diff options
Diffstat (limited to 'tfm.tex')
| -rw-r--r-- | tfm.tex | 244 |
1 files changed, 210 insertions, 34 deletions
@@ -1,10 +1,12 @@ \documentclass[12pt,a4paper,parskip=full]{scrreprt} -\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc +%\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc \usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry} % \usepackage[spanish]{babel} -\usepackage{fontspec} \usepackage{url} +\usepackage{lmodern} +\usepackage{fontspec} \setmonofont{DejaVu Sans Mono} +\usepackage{url} \usepackage{graphicx} \usepackage{cite} \usepackage{amsmath} \usepackage{mathtools} \usepackage{listings} \usepackage{syntax} % \usepackage[compact,small]{titlesec} @@ -16,7 +18,7 @@ \usepackage{amssymb} % arrows \usepackage{mathpartir} % inference rules -% \usepackage{minted} +\usepackage{minted} \usepackage{float} \floatstyle{boxed} @@ -543,23 +545,24 @@ The \textbf{Lambda Calculus} \cite{Church36} is a formal system developed by Alonzo Church in the decade of 1930 as part of his research on the foundations of mathematics and computation (it was later proven to be equivalent to the Turing Machine). In its essence, the Lambda Calculus is a simple term rewriting -system that represents computation through the application of functions. +system that represents computation through the \textbf{application of + functions}. -Following is the grammar representing Lambda \textbf{terms} ($\mathcal{T}$), or -well-formed formulas: +Following is the grammar representing \textbf{lambda terms} ($\mathcal{T}$), +also called ``well-formed formulas'': \begin{bnf}[caption=Lambda Calculus, label={lst:lambda}]{} $\mathcal{T} ::= x$ variable | $(\lambda x . \mathcal{T})$ abstraction | $(\mathcal{T}_1 \: \mathcal{T}_2)$ application - $x ::= v_1, v_2, v_3, ...$ (infinite variables) + $x ::= v_1, v_2, v_3, ...$ (infinite variables available) \end{bnf} Intuitively, the \textbf{abstraction} rule represents function creation: take an -existing term ($\mathcal{T}$) and parameterize it with an argument ($x$). The -variable $x$ \textbf{binds} every instance of the same variable on the body, -which we say are \textbf{bound} instances. The \textbf{application} represents -function evaluation ($\mathcal{T}_1$) with an actual argument ($\mathcal{T}_2)$. +existing term ($\mathcal{T}$) and parameterize it with an argument ($x$). The +variable $x$ binds every instance of the same variable on the body, which we say +are \textbf{bound} instances. The \textbf{application} rule represents function +evaluation ($\mathcal{T}_1$) with an actual argument ($\mathcal{T}_2)$. Seen as a term rewriting system, the Lambda Calculus has some reduction rules that can be applied over terms in order to perform the computation: @@ -584,13 +587,13 @@ $\beta$-reduced following the rule. The semantics of the rule match with the intuition of function application: the result is the body of the function with the formal parameter replaced by the actual argument. -The syntax $\mathcal{T}_1[x := \mathcal{T}_2]$ replaces $x$ by $\mathcal{T}_2$ -in the body of $\mathcal{T}_1$, but we have to be careful in its definition, -because the ``obvious/naïve'' substitution process can lead to unexpected -results. For example, $(\lambda x . y)[y := x]$ would $\beta$-reduce to -$(\lambda x . x)$, which is not the expected result: the new $x$ in the body has -been \textbf{captured} by the argument and the function behavior is now -different. +The \textbf{substitution operation} $\mathcal{T}_1[x := \mathcal{T}_2]$ replaces +$x$ by $\mathcal{T}_2$ in the body of $\mathcal{T}_1$, but we have to be careful +in its definition, because the ``obvious/naïve'' substitution process can lead +to unexpected results. For example, $(\lambda x . y)[y := x]$ would +$\beta$-reduce to $(\lambda x . x)$, which is not the expected result: the new +$x$ in the body has been \textbf{captured} by the argument and the function +behavior is now different. The solution to this problem comes from the intuitive idea that ``the exact choice of names for bound variables is not really important''. The functions @@ -609,7 +612,7 @@ rule is the following: So, to correctly apply a $\beta$-reduction, we will do \textbf{capture-avoiding substitutions}: if there is the danger of capturing variables during a substitution, we will first apply $\alpha$-conversions to change the problematic -variables by fresh ones. +variables by fresh ones. Another equivalence relation over lambda terms is the one defined by the \textbf{eta conversion} ($\eta$-conversion), and follows by the extensional @@ -625,23 +628,96 @@ equivalence of functions in the calculus: In general, we will treat $\alpha$-equivalent and $\eta$-equivalent functions as interchangeable. -http://adam.chlipala.net/cpdt/html/Equality.html -\begin{itemize} -\item Alpha reduction -\item Beta reduction -\item ... -\end{itemize} +\subsection{Types} + +Until now, we have been discussing the \textbf{untyped} Lambda Calculus, where +there are no restrictions to the kind of terms we can build. Every formula +resulting from the grammar (\ref{lst:lambda}) is a valid term. There are +alternative interpretations of the Lambda Calculus, the \textbf{Typed Lambda + Calculi}, which give \textbf{typing rules} to construct ``well-typed terms'' +(terms that have a \textbf{type} associated to it). The point is being unable to +construct terms that ``make no sense'', like the ones that encode logical +paradoxes or whose evaluation does not finish. + +As previously seen, EasyCrypt uses a statically typed expression language that +in turn is represented internally as a typed Lambda Calculus. (TODO: put in +context) \subsection{Extensions} -\subsubsection{Case expressions} +Until there we have seen the ``basic'', or ``pure'' Lambda Calculus, where the +only data primitive is the function. Being turing complete, it is all that is +needed to express all the possible computations, but there are extensions that +make it more suitable to be manipulated by human beings. + +One of the most typical is having natural numbers as primitive terms, that is +way more convenient that representing them as \textbf{church numerals}: + +$$0 \Longleftrightarrow (\lambda f . (\lambda x . x))$$ +$$1 \Longleftrightarrow (\lambda f . (\lambda x . (f \: x)))$$ +$$2 \Longleftrightarrow (\lambda f . (\lambda x . (f \: (f \: x))))$$ +$$...$$ + +As with the natural numbers, any data structure can be encoded in basic Lambda +Calculus \cite{Mogensen00}, but the representation is complex and the terms can +rapidly become very difficult to handle. This is why the first major extension +comes in: \textbf{algebraic data types}. + +\subsubsection{Algebraic Data Types} + +If we want to be able to extend the Lambda Calculus to encode structured data, +we will want to have some way to build new data, instead of extending the +language with every data type we can imagine (naturals, booleans, +etc.). \textbf{Algebraic data types} (ADT's) offer a powerful way to compose +existing terms into more complex ones\footnote{Although ADT's are a + type-theoretical concept, as we are concerned with the untyped version of the + Lambda Calculus, we will be only interested in how it allows us to build new + \textbf{terms}, not \textbf{types}. }. The composition can be made in two +different ways: + +\paragraph{Product types} + +If we have some terms $T_1, T_2, ..., T_n$, we can produce a new term +that is the ordered \textit{grouping} of them: $T = (T_1, T_2, ..., T_n)$. The +resulting structure is often called an \textbf{n-tuple}. + +\paragraph{Sum types} + +If we have some terms $T_1, T_2, ..., T_n$, we can produce a new term that can +be \textbf{disjoint union} of them: +$T = C_1(T_1) \: | \: C_2(T_2) \: | \: ... \: | \: C_n(T_n)$. It consists of a +series of \textbf{variants}, one for every previous term, each tagged by a +unique \textbf{constructor} ($C_1-C_n$). A sum type will take the form of one +(and only one) of the variants, and the constructor is used to in runtime to +know which of the variants it actually is. + + + +As a special interesting case, it is often useful not to parameterize a variant +(sum type) and just have the constructor as one of the values. This can be done +naturally by parameterizing it over the empty product type $()$, also called +\textbf{unit}. + +While the \subsubsection{Fixpoints} +There's also the problem of recursion: as the lambda +functions are anonymous, they can't simply refer to themselves. As with the +church numerals, there are ways to \cite{PeytonJones87} +--- + +http://adam.chlipala.net/cpdt/html/Equality.html + +\begin{itemize} +\item Alpha reduction +\item Beta reduction +\item ... +\end{itemize} @@ -651,6 +727,10 @@ http://adam.chlipala.net/cpdt/html/Equality.html +\section{Normal forms} + + + \section{Abstract Machines} %% (TODO: basic intro, motivation, function application implementations @@ -683,16 +763,110 @@ http://adam.chlipala.net/cpdt/html/Equality.html \chapter{KRIVINE MACHINE} %%%%%%%%%% -\cite{Krivine07} -\cite{Douence07} - - - -\section{Not compiled} %% +To begin our study of the implementation of abstract machines, we will start +with the Krivine Machine. It is a relatively simple and well-known model that +will help us see the steps that we need to take in order to implement a real +abstract machine. We will be using the OCaml language from now on (not only in +this section but also in the next ones). +The Krivine Machine \cite{Krivine07} is an implementation of the weak-head +call-by-name reduction strategy for pure lambda terms. What that means is that: +\begin{itemize} +\item The Krivine Machine reduces pure (untyped) terms in the Lambda Calculus +\item The reduction strategy it implements is call-by-name, reducing first the + leftmost outermost term in the formula +\item It stops reducing whenever the formula is in weak-head normal form, that + is: + \begin{itemize} + \item does not reduce abstractions: $(\lambda x . \mathcal{T})$ + \item does not reduce applications of non-abstractions: $(x \: \mathcal{T})$ + \end{itemize} +\end{itemize} -\section{Compiled} %% +The first thing we need to have is an encoding of the language we will be +reducing, in this case the Lambda Calculus. We will define a module, +\textbf{Lambda}, containing the data structure and basic operations over it: + +\begin{code} + \begin{minted}[fontsize=\footnotesize]{ocaml} +type symbol = string * int +let show_symbol (s, _) = s + +module Lambda = struct + type t = Var of symbol | App of t * t | Abs of symbol * t + let rec show = match m with + | Var x -> show_symbol x + | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")" + | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")" +end + \end{minted} +\end{code} + +(From now on, the auxiliar (e.g., pretty-printing) functions will be ommited for +brevity.) + +Now we have a representation of the pure Lambda Calculus. As the Krivine Machine +usually works with expressions in \textbf{de Bruijn} notation\footnote{ The de + Bruijn's notation gets rid of variable names by replacing them by the number + of ``lambdas'' between it and the lambda that is binding the variable. For + example, $(\lambda x . (\lambda y . (x \: y)))$ will be written in de Bruijn + notation as $(\lambda . (\lambda . (1 \: 0)))$}, we'll need to write an +algorithm to do the conversion. To be sure we do not accidentally build terms +mixing the two notatios, we'll create another module, \textbf{DBILambda}, with a +different data type to represent them: + +\begin{code} + \begin{minted}[fontsize=\scriptsize]{ocaml} +let rec find_idx_exn x = function + | [] -> raise Not_found + | (y::ys) -> if x = y then 0 else 1 + find_idx_exn x ys + +module DBILambda = struct + type dbi_symbol = int * symbol + type t = Var of dbi_symbol | App of t * t | Abs of symbol * t + + let dbi dbis x = (find_idx_exn x dbis, x) + + let of_lambda = + let rec of_lambda dbis = function + | Lambda.Var x -> let (n, x) = dbi dbis x in Var (n, x) + | Lambda.App (m1, m2) -> App (of_lambda dbis m1, of_lambda dbis m2) + | Lambda.Abs (x, m) -> Abs (x, of_lambda (x :: dbis) m) + in of_lambda [] +end + \end{minted} +\end{code} + +The new variables areThe function <<of_lambda>> accepts traditional lambda terms (Lambda.t) and +returns its representation as a term using de Bruijn notation (DBILambda.t). Now +we are ready to implement the actual reduction. + +The Krivine Machine has a state consisting on the code it is evaluating +(\textbf{C}), an environmentThe typical description of the Krivine Machine \cite{Douence07} is given by the +following set of rules: + +\begin{center} +\line(1,0){250} +\end{center} +\begin{table}[H] +\centering +\begin{tabular}{lllll} +$(M N, S, E)$ & \rightsquigarrow & $(M, (S,(N,E)), E)$ \\ \\ +$(\lambda M, (S,N), E)$ & \rightsquigarrow & $(M, S, (E,N))$ \\ \\ +$(i+1, S, (E,N))$ & \rightsquigarrow & $(i, S, E)$ \\ \\ +$(0, S, (E_1,(M,E_2)))$ & \rightsquigarrow & $(M, S, E_2)$ +\end{tabular} +\end{table} +\begin{center} +\line(1,0){250} +\end{center} + +\section{With power} %% + + + +%\section{Compiled} %% @@ -757,10 +931,12 @@ http://adam.chlipala.net/cpdt/html/Equality.html \section{Krivine Machine source code} %% +\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml} - +\newpage \section{ZAM source code} %% +%\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml} \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} |