--- /dev/null
+@article{bohm,\r
+ author = "Corrado B{\"o}hm",\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
+ year = "1968"\r
+}\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
+ journal = {Theor. Comput. Sci.},\r
+ volume = {121},\r
+ number = {1{\&}2},\r
+ pages = {145--167},\r
+ year = {1993},\r
+ url = {https://doi.org/10.1016/0304-3975(93)90087-A},\r
+ doi = {10.1016/0304-3975(93)90087-A},\r
+ timestamp = {Sun, 28 May 2017 13:20:07 +0200},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/Huet93},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
+\r
+@phdthesis{morris,\r
+ author = {J.-H. Morris},\r
+ title = {Lambda-calculus models of programming languages},\r
+ school = {M.I.T.},\r
+ year = 1968,\r
+}\r
+\r
+@inproceedings{DBLP:conf/lics/Saurin05,\r
+ author = {Alexis Saurin},\r
+ title = {Separation with Streams in the lambda{\(\mathrm{\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
+ year = {2005},\r
+ crossref = {DBLP:conf/lics/2005},\r
+ url = {https://doi.org/10.1109/LICS.2005.48},\r
+ doi = {10.1109/LICS.2005.48},\r
+ timestamp = {Thu, 25 May 2017 00:42:40 +0200},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/Saurin05},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
+@proceedings{DBLP:conf/lics/2005,\r
+ title = {20th {IEEE} Symposium on Logic in Computer Science {(LICS} 2005),\r
+ 26-29 June 2005, Chicago, IL, USA, Proceedings},\r
+ publisher = {{IEEE} Computer Society},\r
+ year = {2005},\r
+ url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10087},\r
+ isbn = {0-7695-2266-1},\r
+ timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/2005},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
+\r
+@inproceedings{DBLP:conf/cade/Gacek08,\r
+ author = {Andrew Gacek},\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
+ year = {2008},\r
+ crossref = {DBLP:conf/cade/2008},\r
+ url = {https://doi.org/10.1007/978-3-540-71070-7_13},\r
+ doi = {10.1007/978-3-540-71070-7_13},\r
+ timestamp = {Tue, 13 Jun 2017 10:37:55 +0200},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/Gacek08},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
+@proceedings{DBLP:conf/cade/2008,\r
+ editor = {Alessandro Armando and\r
+ Peter Baumgartner and\r
+ Gilles Dowek},\r
+ title = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008,\r
+ Sydney, Australia, August 12-15, 2008, Proceedings},\r
+ series = {Lecture Notes in Computer Science},\r
+ volume = {5195},\r
+ publisher = {Springer},\r
+ year = {2008},\r
+ url = {https://doi.org/10.1007/978-3-540-71070-7},\r
+ doi = {10.1007/978-3-540-71070-7},\r
+ isbn = {978-3-540-71069-1},\r
+ timestamp = {Tue, 13 Jun 2017 10:37:55 +0200},\r
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/2008},\r
+ bibsource = {dblp computer science bibliography, http://dblp.org}\r
+}\r
--- /dev/null
+\documentclass[10pt]{article}\r
+\r
+\title{B\"ohm's Theorem in Abella}\r
+\author{Andrea Condoluci}\r
+\date{June 30, 2017}\r
+\r
+\newcommand{\lc}[0]{{$\lambda$-calculus}}\r
+\newcommand{\bohm}[0]{{B\"ohm}}\r
+\newcommand{\TODO}[1]{\textcolor{red}{\textbf{TODO} #1}}\r
+\r
+\usepackage{xcolor}\r
+\usepackage{amsmath, amsthm, amssymb}\r
+\usepackage{verbatim}\r
+\usepackage[normalem]{ulem}\r
+\usepackage{cleveref}\r
+\r
+\theoremstyle{definition}\r
+\newtheorem{theorem}{Theorem}\r
+\newtheorem*{theoren}{Theorem}\r
+\newtheorem{lemma}[theorem]{Lemma}\r
+% \newtheorem{corollary}[theorem]{Corollary}\r
+\newtheorem*{corollary}{Corollary}\r
+\newtheorem*{notation}{Notation}\r
+\newtheorem*{definition}{Definition}\r
+\newtheorem{fact}[theorem]{Fact}\r
+\r
+\r
+\begin{document}\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
+\r
+\begin{abstract}\r
+ \TODO{...}\r
+\end{abstract}\r
+\r
+\section*{Introduction}\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
+ 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
+\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
+\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 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
+\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
+ \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
+\r
+Let's 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
+\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
+\end{corollary}\r
+\r
+This last formulation of \bohm's theorem is clearly related to the \textit{observational} or \textit{contextual equivalence} \cite{morris}, which was born at the times of the \bohm's theorem. Two terms are said to be \textit{observationally equivalent} if, when put in the same context, either they both converge to a normal form, or they both diverge. Intuitively, terms are observationally equivalent if they behave in the same way, when ``observed'' from the outside.\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
+\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
+\r
+% Two-level logic approach....\r
+\r
+% Examples: in the \lc, equivalence of big-step and small-step evaluation.\r
+\r
+\section*{Outcomes}\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
+\r
+ \TODO{}\r
+\r
+ \TODO{fireball calculus, and the algorithm we are dessigning}\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
+\r
+\r
+\bibliographystyle{plain}\r
+\bibliography{statement}\r
+\r
+\end{document}\r
projects / fireball-separation.git / commitdiff