\newcommand{\lc}[0]{{$\lambda$-calculus}}\r
\newcommand{\bohm}[0]{{B\"ohm}}\r
\newcommand{\TODO}[1]{\textcolor{red}{\textbf{TODO} #1}}\r
+\newcommand{\fire}[0]{$\lambda_{\operatorname{fire}}$}\r
+\r
+\newcommand{\conv}[1]{=_{#1}}\r
+\newcommand{\convb}[0]{\conv{\beta}}\r
+\newcommand{\convbe}[0]{\conv{\beta\eta}}\r
\r
\usepackage{xcolor}\r
\usepackage{amsmath, amsthm, amssymb}\r
-\usepackage{verbatim}\r
+\usepackage{verbatim, hyperref}\r
\usepackage[normalem]{ulem}\r
\usepackage{cleveref}\r
\r
\r
\maketitle\r
\r
-Segue una presentazione del progetto di ricerca che effettuerei presso il \textit{Laboratoire d'informatique de l'\'Ecole polytechnique} di Parigi, con il supporto economico del programma Marco Polo.\r
+Segue una presentazione del progetto di ricerca che effettuerei presso il \textit{Laboratoire d'informatique de l'\'Ecole polytechnique} di Parigi nel gruppo di ricerca \textit{Parsifal} (\url{https://team.inria.fr/parsifal/}), con il supporto economico del programma Marco Polo.\r
\r
\begin{abstract}\r
- \TODO{...}\r
+ \bohm's theorem is a celebrated theorem in untyped lambda-calculus, and it states that lambda-terms behave differently if they are syntactically different. The proof of this statement is well-known, and consists of a separation algorithm manipulating the syntax of lambda-terms. The proof assistant Abella (co-developed at LIX, Paris) is particularly suited to handle proofs which manipulate lambda-terms. Formalizing \bohm's theorem in Abella would both challenge Abella's underlying logic, and assist us proving correct a much harder separation algorithm for a different calculus that we are studying.\r
\end{abstract}\r
\r
-\section*{Introduction}\r
+\section*{Background}\r
\r
% \subsubsection*{Lambda Calculus}\r
- \textit{Pure lambda calculus} (which we call \lc) was originally conceived by Church, being intended as a general theory of functions which could serve as foundation for mathematics.\r
+ \textit{Pure lambda calculus} (which we call \lc) was originally conceived by Alonzo Church, being intended as a general theory of functions which could serve as foundation for mathematics.\r
Its syntax is based on two basic conceptual operations: $\lambda$-abstraction and application. Since \lc{} can represent computable functions, it is considered an idealized functional programming language, where $\beta$-reduction corresponds to a computational step.\r
\r
- \TODO{In the following, we write $\equiv_\beta$ for equality of the terms up to $\alpha$-conversion (renaming of bound variables) and $\beta$-reduction. $\eta$-convertibility corresponds to extensionality, that means considering equal those functions which give same output on the same inputs.}\r
+ In the following, we say that $M \convb N$ if $M$ and $N$ are $\alpha\beta$-convertible ($\alpha$ being the renaming of bound variables). $\eta$-conversion allows expansion and contraction of the arguments of functions, and corresponds to function extensionality. A term is in \textit{normal form} when no more $\beta$-reductions are viable.\r
\r
\subsubsection*{Separation Theorem}\r
Among the most important results for \lc{} (like fixpoint, Church-Rosser, and normalization theorems) is the \textit{separation theorem} (also known as \bohm's theorem \cite{bohm}).\r
Even though this theorem may seem a basically syntactical property, its importance lays on showing that the syntactical constructions and the reduction rules of \lc{} work well together \cite{DBLP:conf/lics/Saurin05}. In particular, two essential consequences are:\r
\r
\begin{enumerate}\r
- \item any non-trivial model of the \lc{} cannot identify different $\beta\eta$-normal forms;\r
+ \item any non-trivial model of the \lc{} cannot identify $\beta\eta$-different normal forms;\r
\item normal forms can be explored by the only means of computational rules.\r
\end{enumerate}\r
\r
- Intuitively, \bohm's theorem states that when two $\lambda$-terms are syntactically different, then one can put them in the context of a bigger $\lambda$ program s.t. they reduce to two clearly different terms. By \textit{context} (denoted by $E[\,]$) we mean a $\lambda$-term with a hole ($[\,]$ is the hole), such that $E[M]$ is the $\lambda$-term obtained by replacing in $E[\,]$ the holes $[\,]$ with $M$.\r
+ Intuitively, \bohm's theorem states that when two $\lambda$-terms are syntactically different, then one can put them in the context of a bigger $\lambda$ program such that they reduce to two clearly different terms. By \textit{context} (denoted by $E[\,]$) we mean a $\lambda$-term with a hole ($[\,]$ is the hole), such that $E[M]$ is the $\lambda$-term obtained by replacing in $E[\,]$ the hole $[\,]$ with $M$.\r
\r
\begin{theoren}[\bohm{} theorem]\r
Let $M$, $N$ be $\beta\eta$-distinct $\lambda$-terms in normal form; then there exists a context $E[\,]$ such that:\r
\[\begin{array}{ll}\r
- E[M] & \equiv_{\beta} \operatorname{true} \text{, and}\\\r
- E[N] & \equiv_{\beta} \operatorname{false}, \\\r
+ E[M] & \convb \operatorname{true} \text{, and}\\\r
+ E[N] & \convb \operatorname{false}, \\\r
\end{array}\]\r
where $\operatorname{true}:=\lambda x\,y.\,x$ and $\operatorname{false}:=\lambda x\,y.\,y$.\r
\end{theoren}\r
-The proof of this theorem is carried out by induction on so-called \textit{\bohm{} trees} (syntax trees computed from the normal forms), and by means of \textit{\bohm{} transformations}. The technique used in the proof is called ``\bohm-out'', and is a powerful tool that was applied to separation in other $\lambda$-theories.\r
+The proof of this theorem is carried out by induction on so-called \textit{\bohm{} trees} (syntax trees computed from the normal forms), and by means of \textit{\bohm{} transformations}. The technique used in the proof is called ``\bohm-out'', and is a powerful tool that was applied to separation problems in other $\lambda$-theories.\r
\r
-Let's now make some remarks which will be useful in the last section.\r
+Let us now make some remarks which will be useful in the last section.\r
\r
-Firstly, note that easy consequence of the theorem is the following:\r
+Firstly, note that an easy consequence of the theorem is the following:\r
\r
\begin{corollary}\r
Let $M$, $N$ be $\beta\eta$-distinct $\lambda$-terms in normal form; then there exists a context $E[\,]$ such that $E[M]$ has a normal form, and $E[N]$ has no normal form.\r
\r
It is now clear that \bohm's theorem actually states that, in the case of terms with a normal form, observational equivalence coincides with $\beta\eta$-convertibility.\r
\r
-Note that the original proof of \bohm's theorem is \textit{constructive}: it consists of an actual algorithm which, given two $\beta\eta$-distinct $\lambda$-terms, constructs a corresponding discriminating context. Such algorithm was implemented in CAML in \cite{DBLP:journals/tcs/Huet93}, but to my knowledge it was never formalized in a \textit{proof assistant}. A formalization would yield a verified implementation (proven to be correct, and to comply with its specification) of the algorithm; in addition, it would add up to the pile of formalized mathematical knowledge, allowing other researchers to build on top of it.\r
+Note that the original proof of \bohm's theorem is \textit{constructive}: it consists of an actual algorithm which, given two $\beta\eta$-distinct $\lambda$-terms, constructs a corresponding discriminating context. Such algorithm was implemented in CAML in \cite{DBLP:journals/tcs/Huet93}, but to my knowledge it was never formalized in a \textit{proof assistant}.\r
+A formalization would not only yield a verified implementation of the algorithm (which is actually a well-known result and beyond doubt), but mainly:\r
+\begin{enumerate}\r
+ \item probe the proof assistant in which it will be formalized and push it to its limits (see section Outcome);\r
+ \item be a starting point to help us prove correct other separation algorithms which we are currently working on (see section Future Work).\r
+\end{enumerate}\r
+% A formalization would yield a verified implementation (proven to be correct, and to comply with its specification) of the algorithm; in addition, it would add up to the pile of formalized mathematical knowledge, allowing other researchers to build on top of it.\r
\r
\subsubsection*{Abella}\r
-The plan is to formalize \bohm's theorem in Abella. Abella is an interactive theorem prover based on lambda-tree syntax \cite{DBLP:conf/cade/Gacek08}, and it is intended for reasoning about object languages whose syntactic structure is presented through recursive rules.\r
+The plan is to formalize \bohm's theorem in Abella. \textit{Abella} is an interactive theorem prover based on $\lambda$-tree syntax \cite{DBLP:conf/cade/Gacek08}, and it is intended for reasoning about object languages whose syntactic structure is presented through recursive rules.\r
+\r
+The strength of Abella is how it treats \textit{binding} in object languages: in fact, object-level bindings are represented in Abella using \textit{meta-level abstractions}. This makes the encoding of object languages much more straightforward, since usual notions related to binding (such as $\alpha$-equivalence and capture-avoiding substitutions) are already built into the logic and need not be implemented again at the specification level.\r
+\r
+To reason over $\lambda$-tree syntax, Abella uses the $\nabla$ (\textit{nabla}) quantifier, which allows one to move binders from the object-logic to the meta-logic. $\nabla$-bound variables are instantiated with \textit{nominal constants}, and indeed the intuition is that the formula $\nabla x.\,F$ holds iff $F$ holds for whatever $x$, but in a ``generic'' way.\r
\r
-% Two-level logic approach....\r
+As a matter of fact, Abella has been used effectively to formalize proofs in which objects with bindings must be manipulated in a fundamental way: for example, some results in \lc{} (subject reduction, uniqueness of typing, normalizability \`a la Tait) and proof theory (cut-admissibility).\r
\r
-% Examples: in the \lc, equivalence of big-step and small-step evaluation.\r
+\section*{Outcome}\r
\r
-\section*{Outcomes}\r
+As a consequence of Abella's successful handling of binding, and of the syntactic nature of \bohm's theorem, Abella may be particularly well-suited to host its formalization. But this is not completely straightforward: let's see one possible obstacle. One $\nabla$ quantifier handles one binder at the object level, but $\lambda$-terms in strong normal form in \fire{} have the form $\lambda x_1\ldots x_n.\,x_j\,f_1\ldots f_m$ ($f$'s are fireballs), where the normal form begins with $n$ $\lambda$-abstractions. In order to handle iterated binders, it would seem natural for $\nabla$ to quantify over ``vectors'' of variables, but this is not possible at the moment. In the light of this and other technical complications, the formalization of \bohm's theorem won't be trivial, and will hopefully shed some light on possible drawbacks/improvements in Abella's logic; this is also the reason why the hosting research group at LIX, Paris is interested in this project.\r
\r
\section*{Future work}\r
- The computer formalization of \bohm{}'s theorem would be a convenient result on its own\r
+ As we noted, the computer formalization of \bohm{}'s theorem would be a convenient result on its own\r
sake; nevertheless, it poses a solid starting point to provide formal proofs of similar separation results in other $\lambda$-theories and other $\lambda$-calculi. %, for example in extensions of \lc, or according to different evaluation strategies.\r
\r
- For example, the problem of separating $\lambda$-terms popped up inevitably while working with Prof. Claudio Sacerdoti Coen on the observational equality of a calculus in call-by-value called \textit{fireball calculus} \cite{fireball}.\r
+ For example, the problem of separating $\lambda$-terms popped up inevitably while working with Claudio Sacerdoti Coen and Beniamino Accattoli on the observational equality of the \textit{fireball calculus} \fire{} \cite{DBLP:conf/lics/AccattoliC15}. Our goal there is to provide a suitable notion of \textit{bisimulation} in order to characterize syntactically the equivalence of programs (i.e. contextual equivalence).\r
+\r
+ \subsubsection*{The Fireball Calculus}\r
+\r
+ \fire{} is an \textit{open} call-by-value \lc{}. Recall that \textit{call-by-value} is an evaluation strategy for the \lc{} in which - intuitively - functions' arguments are evaluated before the function call. \fire{} is similar to Plotkin's call-by-value \lc{}, which is at the foundation of programming languages (OCaml) and proof assistants (Coq), but \fire{} (as a \textit{weak calculus}, when reductions occur only outside abstractions) is particularly elegant because:\r
+ \begin{itemize}\r
+ \item it is \textit{strongly confluent};\r
+ \item normal forms have a clean syntactic description as \textit{fireballs}: a fireball is either an abstractions (like values in Plotkin), or a variable possibly applied to other fireballs.\r
+ \end{itemize}\r
+\r
+ Strong evaluation may be obtained as usual by iterating the weak one under abstractions. But, mainly because fireballs are not closed under substitutions, the strong calculus has some issues:\r
+ \begin{itemize}\r
+ \item it is \textit{not} confluent;\r
+ \item contextual equivalence is not closed under reduction.\r
+ % a term and its strong normal form may not be contextual equivalent (in the usual sense).\r
+ For example: \[(\lambda y.\,z) \, (x\, x) \to_{\beta} z ,\] but in a context replacing the free variable $x$ with $\lambda x.\, x\, x$, the term on the left diverges, and the one on the right converges.\r
\r
- \TODO{}\r
+ \end{itemize}\r
\r
- \TODO{fireball calculus, and the algorithm we are dessigning}\r
+ Therefore, it is not easy to give a syntactic characterization of contextually equivalent terms. We are working on a separation algorithm which departs non-trivially from \bohm's theorem and other separation algorithms \cite{BOHM1979271}, and it would be the first (working) separation algorithm in call-by-value. After a couple of months of trial and errors, we now understand quite well the problem, and we are done with designing the separation algorithm. It still remains to prove termination, which seems a difficult task.\r
+ In fact, while the \bohm-out technique is ``completely described in less than a page of ML code'' \cite{DBLP:journals/tcs/Huet93}, our algorithm (as of now) consists of more than one-thousand lines of OCaml code; additionally, our procedure relies on the careful repetition of basic trasformations in a certain order, that when altered brings easily to looping and non-termination. Proving termination for such a long algorithm \textit{on paper} is a long and error-prone job, which would profit the support of a proof assistant.\r
\r
- Once done with the formalization, we will adapt the formal proof to the algorithm which we are currently designing for the fireball calculus.\r
-% e si potrebbe estendere la prova al nostro mostro\r
+ The formalization of \bohm's theorem would hence be the first step in formalizing our own separation algorithm, and facilitate us proving that the algorithm terminates and is indeed correct.\r
\r
\r
\bibliographystyle{plain}\r
projects / fireball-separation.git / blobdiff