--- a/gears.ind	Mon May 11 21:31:34 2015 +0900
+++ b/gears.ind	Tue May 12 04:07:34 2015 +0900
@@ -1,4 +1,4 @@
--title: Gears: Low level Formal Representation of code and data
+-title: Programming in code and data 
 
 --abstract:
 
@@ -51,6 +51,8 @@
 
 Domain of C is I and codemain of C is O.
 
+<center><img src="fig/codeGear.jpg"></center>
+
 --Meta computation of Gears
 
 Computation of a code is limited in the inputs and the outputs and it makes the compuation of the code predictable, but its data are
@@ -62,110 +64,166 @@
 
 is a meta compuation. $C$ has one to one correcpondence with $C'$.
 
+    μ : T (T O) → T O
+
 Parallel execution or IO handling are represented as a monad in our scheme. 
 
+<center><img src="fig/meta.jpg"></center>
+
 --A cateogy of codes 
 
 Types of code segments and  data segments narually compose a category of function and types. Codes and data are interconnected one by one.
 
-    Object : f, g, h  ...
-    Arrows : a, b, c  ...
+    Object : a, b, c  ...
+    Arrows : f, g, h  ...
 
-An arrow has its domain object and codomain object.
+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
+codomain is an output type b. 
+
+    h : a → b
+    g : b → c
+    f : c → d
 
 There is compositon of arrows,
 
-    a o b
+    f o g : b → d
 
 and it satisfies the compisition law.
 
-    (a o b)  o c = a  o (b  o c )
+    (f o g)  o h = f  o (g  o h )
 
-It also have identity arrow $id f$.
+There is also an identity arrow $id a$ for each object $a$, which satisfies,
 
     a o id (domain a) = a = id (domain a)  o a
 
 --A cateogy of data
 
-Is there any duality in codes and data? Ususall answer is no, since we cannot simply combine data segments and code segments cannot be objects
-of a category. Here we show a trivial extension of data segments which makes data of category from category of function and types.
+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.jpg"></center>
+
+In other words, is there any duality in codes and data? Ususall 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
+which arrows are data. Actually these two categories are dual in the sense of adjunction, that is
+there is a one to one corespondense between their arrows with isomorphism.
+Here we show the duality as an exercise of a category theory.
 
 The problem of data segments compisition 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. 
+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$.
+
+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 wich domain is data $f$.
+$n : codomain a →  domain b $ is a continuation of $f$.
 
-Data category C 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 $b$ is
-a data segment $f$ with continuation $n$,  $a'$ is a intermidiate data segment.
+We introdue access function as follows:
 
-    data(f,n)
-    f : codomain a  → a'
-    n : a'   → domain b
+    data-domain f = a
+    data-codomain   f = b
+    continuation f = n
 
-If $f$ and $g$ has same codomain $b$, equality of $data(f,n)$ and $data(g,m)$ is defined as follows,
+We use data-codomain and data-comain 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 intermidiate data segment.
 
-    data(f,n) = data(g,m) iff b o n = b  o m
+    n : codomain a  → domain b
+    f = {a,b,n}
 
-where $b$ is a codomain of both $data(f,n)$ and $data(g,m)$.
+$f$ is an arrow from $a$ to $b$.
+
+<center><img src="fig/dataGearComposition.jpg"></center>
 
-To make an identity arrow in the Data category, if $a$ is a codomain of $f$, we need a reverse arrow of $a$, $a'$.
+If $f$ and $g$ has same data-domain and data-codomain, an equality of $f$ and $g$ is defined as follows,
 
-    data(f,(codomain f)')
+    f = g if b o continuation f = b  o continuation g
+
+where $b$ is data-codomain of $f$ and $g$.
 
 Compisition of arrows of Data category is defined as follows.
 
-    data(f,n)  ∙ data(g,m)  = data(f,n  o g  o m)
+    {b,c,m}  ∙ {a,b,n}  = {a,c,m o (b o n))}
 
 It is easy to see its composition lows.
 
-    data(f,n)  ∙ ( data(g,m)   ∙ data(g,m)  ) =  (data(f,n)  ∙  data(g,m) )  ∙ data(g,m)  
+    {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
+
+    a  o a' =  id (codmain a)
+
+Then an identity data segment  of $a$ in Data Categoy C is
+
+    {a,a,a'}
+
+<center><img src="fig/IdDataGear.jpg"></center>
 
 To check $data(f,a')$ is an identity,
 
-    data(f,(codomain f)') ∙ data(g,n) = data(g,n)
-
-it is true if and only if
+    {b,b,b'}  ∙  {a,b,n} = {a,b,b' o (b o n)} = {a,b,n}
 
-    codmain f  o ( (codmain f)'  o g )  o n = g  o n
-
-since $(codmain f)'$ is a reverse of $codomain f$, it holds. Right identity law holds the same way. 
+Right identity law holds the same way. 
 
 
 --A trivial duality of code and data
 
+<center><img src="fig/Duality.jpg"></center>
+
+
 Data category is a data segment with continuation, which is one step behind, so there is a trivial one to one corespondence. 
-It is also easy to show C and Data category C  is an adjuntion pair.
-
-Data segments in a Data category has an arrow in an original category C, so its corespondence is trivial. Acturally, we have a map F,
+It is also easy to show C and Data category C  is an adjuntion pair. We show it using a universal mapping problem.
 
-    F : Obj C → Obj (DataCategory C)
-    F f =  data(f, id f)
+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 . Acturally, we have a map F,
 
-It has identity continuation, behave as a data segemtn with no continuation. Functor U : (DataCategory C) C is defined as follows
+    F : Obj C → Obj (Data Category C)
+    F a =  id a
 
-    U f = codomain f
-    U data(f,n) =  b o n
+As a reverse, Functor U : (DataCategory C) C is defined as follows :
+
+    U d = codomain d
+    U {a,b,n}  =  b o n
 
-wehre $b$ is a codomain of $data(f,n)$.
-Object $f$ in Data Category C  is an allow of C and it has a codomain. Arrow $data(f,n)$ in Data Category C has
-original arrow $f$ and continuation $n$.
+wehre $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 easily checked as
+
+    U {a,a,a'}  =  a o a' = id (codmain a)
 
-With a mapping transformation $η$,
+We need a mapping $η$, which will be a natural transformation. 
+
+    η : Obj C → U ( F a )
+    η a = id a
 
-    η : Obj C → Arrow C
-    η f = id f
+We can define a solution $*$ of universal mapping problem for $F, U, η$ for
 
-We can define a solution of universal mapping problem, 
+    f : a → U {a,b,n}.
+
+it is an allow from $F a$ to $b$,
 
-    * f =   b'  o f
+    * f =   {a,b,b'  o f}
 
-and
+To see this is a solution, 
 
-    U ( *f )  o (η a) = f
+    U ( *f )  o (η a) =  (b  o (b'  o f) )  o id a = f
 
 is directry checke and $*f$ is unique, that is 
 
     if there is an arrow g $U g  o (η a) = f$ then $g = *f$.
 
-This is also trivial.
+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.
+
 
 --Comparison
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lola2015.tex	Tue May 12 04:07:34 2015 +0900
@@ -0,0 +1,34 @@
+\documentclass[envcountsame]{llncs}
+\usepackage[dvipdfmx]{graphicx}
+\usepackage{llncsdoc}
+\usepackage{url}
+\usepackage{listings}
+
+
+\bibliographystyle{plain} % for bibliography
+%\title{The implementation of recursive type syntax on GCC-4.6 for CbC}
+\title{Recursive type syntax in Continuation based C}
+\titlerunning{title running}
+\toctitle{toc title}
+%\subtitle{sub title}
+\author{Shinji Kono\inst{1} Nobuyasu Oshiro\inst{2}}
+\authorrunning{authorrunning}
+\institute{University of the Ryukyus}
+\email{}
+
+\begin{document}
+\maketitle
+\input common
+
+\begin{abstract}
+\input{abstract}
+\end{abstract}
+
+%\pagenumbering{arabic}
+
+\input{0}	% sections
+
+\bibliography{ref}
+\nocite{r4rs,CompilingWithContinuation,kono08f}
+
+\end{document}