Mercurial > hg > Papers > 2015 > atton-lola
changeset 12:d62cfdf464fe
Mini fixes
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 19 Apr 2015 17:17:16 +0900 |
| parents | 079a9829d204 |
| children | 7b833cdd68a9 |
| files | cfopm.pdf cfopm.tex |
| diffstat | 2 files changed, 5 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/cfopm.tex Sun Apr 19 12:28:46 2015 +0900 +++ b/cfopm.tex Sun Apr 19 17:17:16 2015 +0900 @@ -113,8 +113,8 @@ \section{Meta computation and Monads} Meta computations in CbC formalized by Monads to prevent chaos by unlimited computations. -Monads are a notion of Category Theory, in programs Monad correspondence of normal/meta computations\ref{Moggi:1991:NCM:116981.116984}. -For example, diverging computation as extended normal computations is represented direct sum of normal values and bottom. +Monads are a notion of Category Theory, in programs Monad correspondence of normal/meta computations\cite{Moggi:1991:NCM:116981.116984}. +For example, diverging computation is represented direct sum of normal values and bottom. We show formalization of programs for using Monads. Programs notated typed lambda calculus constructed values and abstractions. @@ -129,16 +129,16 @@ f x : B \\ \end{eqnarray*} -Type matched abstractions can be composed by operator ';'. +Type matched abstractions can be composed by operator '$\circ$'. Order of composition are commutative. \begin{eqnarray*} f : A \rightarrow B \\ g : B \rightarrow C \\ - f;g : A \rightarrow C \\ + g \circ f : A \rightarrow C \\ \\ h : C \rightarrow D \\ - (f;g);h = f;(g;h) + (h \circ g) \circ f = h \circ (g \circ f) : A \rightarrow D \end{eqnarray*} Abstractions has many arguments notated by abstraction took a argument, and returns a abstraction that argument numbers has decreased(Currying).