@article{bohm,\r
author = "Corrado B{\"o}hm",\r
- title = "{Alcune} {Propriet{\`a}} delle {Forme} $\beta\eta$-normali nel\r
+ title = "Alcune propriet{\`a} delle Forme $\beta\eta$-normali nel\r
$\lambda${K}-calcolo. ({Italian})",\r
journal = "Pubblicazioni dell'IAC",\r
volume = "696:119",\r
\r
@article{DBLP:journals/tcs/Huet93,\r
author = {G{\'{e}}rard P. Huet},\r
- title = {An {Analysis} of {B}{\"{o}}hm's {T}heorem},\r
+ title = {An Analysis of {B}{\"{o}}hm's theorem},\r
journal = {Theor. Comput. Sci.},\r
volume = {121},\r
number = {1{\&}2},\r
\r
@inproceedings{DBLP:conf/lics/Saurin05,\r
author = {Alexis Saurin},\r
- title = {Separation with Streams in the lambda{\(\mathrm{\mu}\)}-calculus},\r
+ title = {Separation with Streams in the $\lambda\mu$-calculus},\r
booktitle = {20th {IEEE} Symposium on Logic in Computer Science {(LICS} 2005),\r
26-29 June 2005, Chicago, IL, USA, Proceedings},\r
pages = {356--365},\r
\r
@inproceedings{DBLP:conf/cade/Gacek08,\r
author = {Andrew Gacek},\r
- title = {{The} {Abella} {Interactive} {Theorem} {Prover} ({System} {Description})},\r
+ title = {The Abella Interactive Theorem Prover ({System} Description)},\r
booktitle = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008,\r
Sydney, Australia, August 12-15, 2008, Proceedings},\r
pages = {154--161},\r
biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/2008},\r
bibsource = {dblp computer science bibliography, http://dblp.org}\r
}\r
+\r
+@inproceedings{DBLP:conf/lics/AccattoliC15,\r
+ author = {Beniamino Accattoli and\r
+ Claudio Sacerdoti Coen},\r
+ title = {On the Relative Usefulness of Fireballs},\r
+ booktitle = {30th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}\r
+ 2015, Kyoto, Japan, July 6-10, 2015},\r
+ pages = {141--155},\r
+ year = {2015},\r
+ crossref = {DBLP:conf/lics/2015},\r
+ url = {https://doi.org/10.1109/LICS.2015.23},\r
+ doi = {10.1109/LICS.2015.23},\r
+ timestamp = {Thu, 15 Jun 2017 21:41:13 +0200},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/AccattoliC15},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
+@proceedings{DBLP:conf/lics/2015,\r
+ title = {30th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}\r
+ 2015, Kyoto, Japan, July 6-10, 2015},\r
+ publisher = {{IEEE} Computer Society},\r
+ year = {2015},\r
+ url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7174833},\r
+ isbn = {978-1-4799-8875-4},\r
+ timestamp = {Wed, 25 May 2016 10:19:57 +0200},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/2015},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
\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
\TODO{...}\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 in it.\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
\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
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
\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. 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
+\r
+$\nabla$\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
\r
% Two-level logic approach....\r
\r
\r
\section*{Outcomes}\r
\r
+\TODO{\ldots, pro/contro Abella}\r
+\r
\section*{Future work}\r
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 here 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
+\end{itemize}\r
\r
- \TODO{}\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
\r
- \TODO{fireball calculus, and the algorithm we are dessigning}\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
\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
+ % 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
\r
\r
projects / fireball-separation.git / commitdiff