Mercurial > hg > Papers > 2015 > kono-lola
changeset 5:32ec7f73f166
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 12 May 2015 11:44:50 +0900 |
| parents | 8d0f97fd8af3 |
| children | 197b27b2fd8b |
| files | gears.ind lola2015.tex |
| diffstat | 2 files changed, 62 insertions(+), 102 deletions(-) [+] |
line wrap: on
line diff
--- a/gears.ind Tue May 12 10:44:14 2015 +0900 +++ b/gears.ind Tue May 12 11:44:50 2015 +0900 @@ -12,7 +12,7 @@ --Reliable computation and predictability Various software are used in real world. Each of them have to work in a reliable way. A piece of device contains -millions of lines of code. These programs are written in C, Haskell and so on. +millions of lines of code. These programs are written in C, Haskell\cite{haskell} and so on. To assure its reliability, the computation of a function should be predictable. The correctness of the prediction should be assured by measurements, model checking or proofs. @@ -35,76 +35,62 @@ Actually we implement our Gears language in LLVM\cite{LLVM}, but we can think both code and data are System F\cite{Girard:1989:PT:64805} term. As usual, Types are defined starting from type variables X,Y,Z and is generated by two operations: - 1. if U and V are types, then U → V is a type. - 2. if V i a type, and X a type variable, then ΠX.V is a type. - + 2. if V i a type, and X a type variable, + then ΠX.V is a type. Terms are constructed by six schemes - - 1. variable: $x^T, y^T, z^T,...$ of type $T$, - 2. application: $tu$ of type $V$, where $t$ is of type $U→V$ and $u$ is of type $U$, - 3. λ-abstraction: $λx^U.v$ of type $U→V$, where $x^U$ is a variable of type $U$ and $v$ is of type $V$, - 4. universal abstraction: if $v$ is a term type V, then we can form $ΛX.v$ of type $ΠX.V$, so long as the variable $X$ is not free in the type of a free variable of $v$. - 5. universal application: if $t$ is a term of type $ΠX.V$ and $U$ is a type, then %tU$ is a term of type $V[U/X]$. - + 1. variable: x, y, z,... of type T, + 2. application: t u of type V, where t is of type + U→V and u is of type U, + 3. λ-abstraction: λx.v of type U→V, + where x is a variable of type U and v is of type V, + 4. universal abstraction: if v is a term type V, then + we can form ΛX.v of type ΠX.V, so long as the + variable X is not free in the type of a free variable of v. + 5. universal application: if t is a term of type ΠX.V + and U is a type, then tU is a term of type V[U/X]. and usual conversions, - 1. (λx.v)u 〜> v[u/x] 2. (ΛX.v)U 〜> v[U/X] - -What we need here is that a term has a type, a function has type $U → V$. -Code segments f of type $I → O$, accepts data segments of type $I$ and generates data segments of type $O$. - +What we need here is that a term has a type, a function has type \verb+U → V+. +Code segments f of type \verb+I → O+, accepts data segments of type \verb+I+ and generates data segments of type \verb+O+. f : I → O - Domain of C is I and codomain of C is O. Gears system only allows calling another code at the bottom of the code, that is all codes have tail call form. Normal function call is not prohibited, but it should be closed in a code. -<center><img src="fig/codeGear.svg"></center> +<center><img src="fig/codeGear.pdf"></center> --Meta computation of Gears Computation of a code is limited in the inputs and the outputs and it makes the computation of the code predictable, but its data are usually connected to other data. The code has its continuation also. These connections are out of the scope of the code. We think these connections are made by a meta computation, such as monads\cite{Moggi:1989:CLM:77350.77353}. A monad is a data structure with monad laws and -after an execution of a code, monads join code is called to handle meta data structure. With monad $T$, - +after an execution of a code, monads join code is called to handle meta data structure. With monad \verb+T\verb+, C' : I → T O - -is a meta computation. $C$ has one to one correspondence with $C'$. - +is a meta computation. \verb+C+ has one to one correspondence with \verb+C'+. μ : T (T O) → T O Parallel execution or IO handling are represented as a monad in our scheme. Monads are only allows to use at the bottom of a code in our system. -<center><img src="fig/meta.svg"></center> +<center><img src="fig/meta.pdf"></center> --A category of codes Types of code segments and data segments naturally compose a category of function and types. Codes and data are interconnected one by one. - Object : a, b, c ... Arrows : f, g, h ... - -An arrow has its domain object and codomain object. In this case, Object is a type of data and arrows are function $h$ with type $a → b$, which domain is an input type a and +An arrow has its domain object and codomain object. In this case, Object is a type of data and arrows are function \verb+h+ with type \verb+a → b+, which domain is an input type a and codomain is an output type b. - h : a → b g : b → c f : c → d - There is composition of arrows, - f o g : b → d - and it satisfies the composition law. - (f o g) o h = f o (g o h ) - -There is also an identity arrow $id a$ for each object $a$, which satisfies, - +There is also an identity arrow \verb+id a+ for each object \verb+a+, which satisfies, a o id (domain a) = a = id (domain a) o a --A category of data @@ -112,7 +98,7 @@ A code generate an output type and it becomes an input type of next code. It is similar to a code is in between an input type and an output type. Is is possible to think data is an arrow between codes? -<center><img src="fig/dataGear.svg"></center> +<center><img src="fig/dataGear.pdf"></center> In other words, is there any duality in codes and data? Usual answer is no, since we cannot simply combine data segments, but introducing continuation, it is possible to create a category which objects are functions and @@ -121,69 +107,59 @@ Here we show the duality as an exercise of a category theory. The problem of data segments composition is that it forgets about later computation. We can simply store it as a continuation in the -data segment. Data segments now have a continuation, which is a code segment. It is a part of meta computation. We have a data $f$, -which is a codomain of a code $a$ and is a domain of code $b$. A continuation of $f$ will called before the execution of code $b$. +data segment. Data segments now have a continuation, which is a code segment. It is a part of meta computation. We have a data \verb+f+, +which is a codomain of a code \verb+a+ and is a domain of code \verb+b+. A continuation of \verb+f+ will called before the execution of code \verb+b+. -Now an data arrow $f$ is a triplet ${a,b,n}$, $a$ is a code which codomain is data $f$ and $b$ is a code which domain is data $f$. -$n : codomain a → domain b $ is a continuation of $f$. +Now an data arrow \verb+f+ is a triplet \verb+{a,b,n}+, \verb+a+ is a code which codomain is data \verb+f+ and \verb+b+ is a code which domain is data \verb+f+. +\verb+n : codomain a → domain b + is a continuation of \verb+f+. We introduce access function as follows: - data-domain f = a - data-codomain f = b + data-codomain f = b continuation f = n We use data-codomain and data-codomain for new Data Category C, which is constructed from a category C. -Objects of Data category C are arrows of category C. An arrow of Data category C from $a$ to $c$ is -a data segment $f$ with continuation $n$, $b'$ is a intermediate data segment. - +Objects of Data category C are arrows of category C. An arrow of Data category C from \verb+a+ to \verb+c+ is +a data segment \verb+f+ with continuation \verb+n+, \verb+b'+ is a intermediate data segment. n : codomain a → domain b f = {a,b,n} -$f$ is an arrow from $a$ to $b$. +\verb+f+ is an arrow from \verb+a+ to \verb+b+. -<center><img src="fig/dataGearComposition.svg"></center> +<center><img src="fig/dataGearComposition.pdf"></center> -If $f$ and $g$ has same data-domain and data-codomain, an equality of $f$ and $g$ is defined as follows, - +If \verb+f+ and \verb+g+ has same data-domain and data-codomain, an equality of \verb+f+ and \verb+g+ is defined as follows, f = g if b o continuation f = b o continuation g - -where $b$ is data-codomain of $f$ and $g$. +where \verb+b+ is data-codomain of \verb+f+ and \verb+g+. Composition of arrows of Data category is defined as follows. - - {b,c,m} ∙ {a,b,n} = {a,c,m o (b o n))} - + {b,c,m} + {a,b,n} = {a,c,m o (b o n))} It is easy to see its composition lows. - - {c,d,l} ∙ ( {b,c,m} ∙ {a,b,n} ) = ({c,d,l} ∙ {b,c,m} ) ∙ {a,b,n} - + {c,d,l} + ( {b,c,m} + {a,b,n} ) = + ({c,d,l} + {b,c,m} ) + {a,b,n} because - d o ( l o ( m o (b o n))) = d o (( l o m ) o (b o n) ) . - -To make an identity arrow in the Data category, if $a$ is a codomain of $f$, we need a reverse arrow of $a$, $a'$. -So every arrows $a$ in C have to have a reverse arrow $a'$, where - +To make an identity arrow in the Data category, if \verb+a+ is a codomain of \verb+f+, we need a reverse arrow of \verb+a+, \verb+a'+. +So every arrows \verb+a+ in C have to have a reverse arrow \verb+a'+, where a o a' = id (codomain a) - -Then an identity data segment of $a$ in Data Category C is - +Then an identity data segment of \verb+a+ in Data Category C is {a,a,a'} - -<center><img src="fig/IdDataGear.svg"></center> +<center><img src="fig/IdDataGear.pdf"></center> -To check $data(f,a')$ is an identity, +To check \verb+{a,a,a'}+ is an identity, + {b,b,b'} + {a,b,n} = {a,b,b' o (b o n)} = {a,b,n} +Right identity law holds the same way. - {b,b,b'} ∙ {a,b,n} = {a,b,b' o (b o n)} = {a,b,n} - -Right identity law holds the same way. +If we use + continuation f = continuation g +as a definition of arrow equality, we need + a' o a = id (domain a) --A trivial duality of code and data -<center><img src="fig/Duality.svg"></center> +<center><img src="fig/Duality.pdf"></center> Data category is a data segment with continuation, which is one step behind, so there is a trivial one to one correspondence. @@ -191,49 +167,32 @@ Data segments in a Data category C is an object of original category C, so it has an identity arrow, which is an object of Data Category C . Actually, we have a map F, - F : Obj C → Obj (Data Category C) F a = id a - As a reverse, Functor U : (DataCategory C) C is defined as follows : - U d = codomain d U {a,b,n} = b o n - -where $d$ is an object of Data Category C, and ${a,b,n}$ is an arrow from $a$ to $b$, with continuation $n$. -Identity law and distribution law of $U$ is easyly checked as - +where \verb+d+ is an object of Data Category C, and \verb+{a,b,n}+ is an arrow from \verb+a+ to \verb+b+, with continuation \verb+n+. +Identity law and distribution law of \verb+U+ is easyly checked as U {a,a,a'} = a o a' = id (codomain a) - -We need a mapping $η$, which will be a natural transformation. - +We need a mapping \verb+η+, which will be a natural transformation. η : Obj C → U ( F a ) η a = id a - -We can define a solution $*$ of universal mapping problem for $F, U, η$ for - +We can define a solution \verb+*+ of universal mapping problem for \verb+F, U, η+ for f : a → U {a,b,n}. - -it is an allow from $F a$ to $b$, - +it is an allow from \verb+F a+ to \verb+b+, * f = {a,b,b' o f} - To see this is a solution, - U ( *f ) o (η a) = (b o (b' o f) ) o id a = f - -is directly checked and $*f$ is unique, that is - - if there is an arrow g $U g o (η a) = f$ then $g = *f$. - +is directly checked and \verb+*f+ is unique, that is + if there is an arrow g U g o (η a) = f then g = *f. This is also trivial as - - b o continuation g = ( b o b' ) o ( b o continuation g) = - b o (b' o ( b o continuation g) ) = - b o (b ' o f) = - b o continuation ( *f ) - -which implies $g = *f$. Q.E.D. + b o continuation g = + ( b o b' ) o ( b o continuation g) = + b o (b' o ( b o continuation g) ) = + b o (b ' o f) = + b o continuation ( *f ) +which implies \verb+g = *f+. Q.E.D. --Comparison