\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
- \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
+ \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*{Background}\r
\subsubsection*{Abella}\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 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 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
\r
\section*{Outcome}\r
\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
+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
As we noted, the computer formalization of \bohm{}'s theorem would be a convenient result on its own\r
\end{itemize}\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 \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
+ 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
- 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
+ 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 / commitdiff