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
\r
\begin{abstract}\r
- \TODO{...}\r
+ \bohm's theorem is a very important theorem in untyped lambda-calculus: 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 syntactically manipulating lambda-terms. Particularly suited to handle proofs which manipulate lambda-terms is a proof assistant like a Abella, which is co-developed at LIX, Paris. Formalizing \bohm's theorem in Abella would both challenge Abella underlying logic, and assist us proving correct our own different separation algorithm.\r
\end{abstract}\r
\r
\section*{Background}\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
- 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 in it.\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
\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 strenght of Abella is how it treats \textit{binding} in object languages: in fact, object-level binding are represented in Abella using \textit{meta-level abstraction}. 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
+The strength of Abella is how it treats \textit{binding} in object languages: in fact, object-level binding are represented in Abella using \textit{meta-level abstraction}. 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
-$\nabla$\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
-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
+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
-% Two-level logic approach....\r
+\section*{Outcome}\r
\r
-% Examples: in the \lc, equivalence of big-step and small-step evaluation.\r
-\r
-\section*{Outcomes}\r
-\r
-\TODO{\ldots, pro/contro Abella}\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 example. 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.\,i$ ($i$ is an inert), 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 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 Claudio Sacerdoti Coen and Beniamino Accattoli on the observational equality of the \textit{fireball calculus} \fire{} \cite{DBLP:conf/lics/AccattoliC15}. Our goal here is to provide a suitable notion of \textit{bisimulation} in order to characterize syntactically the equivalence of programs (i.e. contextual equivalence).\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
\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
-\end{itemize}\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
-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 \TODO{[??? qui cit. i torinesi]}, and it would be the first (working) separation algorithm in call-by-value. \TODO{We are much done with designing but struggling to prove termination}.\r
+ \end{itemize}\r
\r
-The formalization of \bohm's theorem would provide a good starting point for the formalization of our own algorithm; this would assist us in proving that our separaation algorithm terminates and is correct.\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.\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, which would assist us in proving that the algorithm terminates and is indeed correct.\r
\r
\r
\bibliographystyle{plain}\r
projects / fireball-separation.git / commitdiff