diff options
Diffstat (limited to 'tfm.tex')
| -rw-r--r-- | tfm.tex | 99 |
1 files changed, 94 insertions, 5 deletions
@@ -13,6 +13,9 @@ \usepackage{perpage} \usepackage{subcaption} \usepackage{tikz} +\usepackage{amssymb} % arrows +\usepackage{mathpartir} % inference rules + % \usepackage{minted} \usepackage{float} @@ -25,6 +28,7 @@ \hypersetup{pageanchor=false} +\input{defs} \input{ec-defs} \input{front/front-init} @@ -270,6 +274,7 @@ $$\Dec(sk,C) = M$$ That is, a message ($M$) can be encrypted using a public key to obtain a ciphertext ($C$). +(TODO: expand) \section{Proofs by reduction} %% @@ -487,7 +492,7 @@ EasyCrypt supports judgments in some logics derived from Hoare logic: This logic is the most complete and useful when developing game-based reduction proofs, because it allows to encode each game transition as a - judgment. Twe two games are $c_1$ and $c_2$ respectively and the + judgment. Twe two games are $c_1$ and $c_2$ respectively, and the pre/postconditions refer to the probability of the adversary winning the games. @@ -534,18 +539,92 @@ qed. \section{Lambda Calculus} %% -\cite{Church36} +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. +Following is the grammar representing Lambda \textbf{terms} ($\mathcal{T}$), or +well-formed formulas: -\subsection{Extensions} +\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) +\end{bnf} -\subsubsection{Case expressions} +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)$. -\subsubsection{Fixpoints} +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: \subsection{Reduction rules} +Arguably the most important rule in Lambda Calculus is the \textbf{beta + reduction}, or $\beta$-reduction. This rule represents function evaluation, +and can be outlined in the following way: + +\[ + \inferrule* [left=$\beta$-red] + { } + {((\lambda x . \mathcal{T}_1) \: \mathcal{T}_2) \Betared \mathcal{T}_1[x := + \mathcal{T}_2]} +\] + +An application with an abstraction in the left-hand side is called a +\textbf{redex}, short for ``reducible expression'', because it can be +$\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 solution to this problem comes from the intuitive idea that ``the exact +choice of names for bound variables is not really important''. The functions +$(\lambda x . x)$ and $(\lambda y . y)$ behave in the same way and thus should +be considered equal. The \textbf{alpha equivalence} ($\alpha$-equivalence) is +the equivalence relationship that expresses this idea through another rule: the +\textbf{alpha conversion} ($\alpha$-conversion). The basic definition of this +rule is the following: + +\[ + \inferrule* [left=$\alpha$-conv] + {y \notin \mathcal{T}} + {(\lambda x . \mathcal{T}) \Alphared (\lambda y . \mathcal{T}[x := y])} +\] + +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. + +Another equivalence relation over lambda terms is the one defined by the +\textbf{eta conversion} ($\eta$-conversion), and follows by the extensional +equivalence of functions in the calculus: + +\[ + \inferrule* [left=$\eta$-conv] + {x \notin FV(\mathcal{T})} + {(\lambda x . \mathcal{T} \: x) \Etabired \mathcal{T}} +\] + + +In general, we will treat $\alpha$-equivalent and $\eta$-equivalent functions as +interchangeable. + http://adam.chlipala.net/cpdt/html/Equality.html \begin{itemize} @@ -555,6 +634,16 @@ http://adam.chlipala.net/cpdt/html/Equality.html \end{itemize} +\subsection{Extensions} + +\subsubsection{Case expressions} + +\subsubsection{Fixpoints} + + + + + \section{Evaluation Strategies} %% |