From f226d96900b53bd05be3370f08d93f4c4cfa39f9 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 29 Jun 2017 22:26:13 +0200 Subject: [PATCH] Added Andrea's research proposal for Marco Polo grant --- marco polo/statement.bib | 88 +++++++++++++++++++++++++++++++ marco polo/statement.tex | 108 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 196 insertions(+) create mode 100644 marco polo/statement.bib create mode 100644 marco polo/statement.tex diff --git a/marco polo/statement.bib b/marco polo/statement.bib new file mode 100644 index 0000000..cff4869 --- /dev/null +++ b/marco polo/statement.bib @@ -0,0 +1,88 @@ +@article{bohm, + author = "Corrado B{\"o}hm", + title = "{Alcune} {Propriet{\`a}} delle {Forme} $\beta\eta$-normali nel + $\lambda${K}-calcolo. ({Italian})", + journal = "Pubblicazioni dell'IAC", + volume = "696:119", + year = "1968" +} + +@article{DBLP:journals/tcs/Huet93, + author = {G{\'{e}}rard P. Huet}, + title = {An {Analysis} of {B}{\"{o}}hm's {T}heorem}, + journal = {Theor. Comput. Sci.}, + volume = {121}, + number = {1{\&}2}, + pages = {145--167}, + year = {1993}, + url = {https://doi.org/10.1016/0304-3975(93)90087-A}, + doi = {10.1016/0304-3975(93)90087-A}, + timestamp = {Sun, 28 May 2017 13:20:07 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/Huet93}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@phdthesis{morris, + author = {J.-H. Morris}, + title = {Lambda-calculus models of programming languages}, + school = {M.I.T.}, + year = 1968, +} + +@inproceedings{DBLP:conf/lics/Saurin05, + author = {Alexis Saurin}, + title = {Separation with Streams in the lambda{\(\mathrm{\mu}\)}-calculus}, + booktitle = {20th {IEEE} Symposium on Logic in Computer Science {(LICS} 2005), + 26-29 June 2005, Chicago, IL, USA, Proceedings}, + pages = {356--365}, + year = {2005}, + crossref = {DBLP:conf/lics/2005}, + url = {https://doi.org/10.1109/LICS.2005.48}, + doi = {10.1109/LICS.2005.48}, + timestamp = {Thu, 25 May 2017 00:42:40 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/Saurin05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} +@proceedings{DBLP:conf/lics/2005, + title = {20th {IEEE} Symposium on Logic in Computer Science {(LICS} 2005), + 26-29 June 2005, Chicago, IL, USA, Proceedings}, + publisher = {{IEEE} Computer Society}, + year = {2005}, + url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10087}, + isbn = {0-7695-2266-1}, + timestamp = {Fri, 21 Nov 2014 14:08:56 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/2005}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{DBLP:conf/cade/Gacek08, + author = {Andrew Gacek}, + title = {{The} {Abella} {Interactive} {Theorem} {Prover} ({System} {Description})}, + booktitle = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008, + Sydney, Australia, August 12-15, 2008, Proceedings}, + pages = {154--161}, + year = {2008}, + crossref = {DBLP:conf/cade/2008}, + url = {https://doi.org/10.1007/978-3-540-71070-7_13}, + doi = {10.1007/978-3-540-71070-7_13}, + timestamp = {Tue, 13 Jun 2017 10:37:55 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/Gacek08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} +@proceedings{DBLP:conf/cade/2008, + editor = {Alessandro Armando and + Peter Baumgartner and + Gilles Dowek}, + title = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008, + Sydney, Australia, August 12-15, 2008, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {5195}, + publisher = {Springer}, + year = {2008}, + url = {https://doi.org/10.1007/978-3-540-71070-7}, + doi = {10.1007/978-3-540-71070-7}, + isbn = {978-3-540-71069-1}, + timestamp = {Tue, 13 Jun 2017 10:37:55 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/2008}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} diff --git a/marco polo/statement.tex b/marco polo/statement.tex new file mode 100644 index 0000000..24fef61 --- /dev/null +++ b/marco polo/statement.tex @@ -0,0 +1,108 @@ +\documentclass[10pt]{article} + +\title{B\"ohm's Theorem in Abella} +\author{Andrea Condoluci} +\date{June 30, 2017} + +\newcommand{\lc}[0]{{$\lambda$-calculus}} +\newcommand{\bohm}[0]{{B\"ohm}} +\newcommand{\TODO}[1]{\textcolor{red}{\textbf{TODO} #1}} + +\usepackage{xcolor} +\usepackage{amsmath, amsthm, amssymb} +\usepackage{verbatim} +\usepackage[normalem]{ulem} +\usepackage{cleveref} + +\theoremstyle{definition} +\newtheorem{theorem}{Theorem} +\newtheorem*{theoren}{Theorem} +\newtheorem{lemma}[theorem]{Lemma} +% \newtheorem{corollary}[theorem]{Corollary} +\newtheorem*{corollary}{Corollary} +\newtheorem*{notation}{Notation} +\newtheorem*{definition}{Definition} +\newtheorem{fact}[theorem]{Fact} + + +\begin{document} + +\maketitle + +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. + +\begin{abstract} + \TODO{...} +\end{abstract} + +\section*{Introduction} + +% \subsubsection*{Lambda Calculus} + \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. + 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. + + \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.} + +\subsubsection*{Separation Theorem} + 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}). + + 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: + + \begin{enumerate} + \item any non-trivial model of the \lc{} cannot identify different $\beta\eta$-normal forms; + \item normal forms can be explored by the only means of computational rules. + \end{enumerate} + + 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$. + +\begin{theoren}[\bohm{} theorem] + Let $M$, $N$ be $\beta\eta$-distinct $\lambda$-terms in normal form; then there exists a context $E[\,]$ such that: + \[\begin{array}{ll} + E[M] & \equiv_{\beta} \operatorname{true} \text{, and}\\ + E[N] & \equiv_{\beta} \operatorname{false}, \\ + \end{array}\] + where $\operatorname{true}:=\lambda x\,y.\,x$ and $\operatorname{false}:=\lambda x\,y.\,y$. +\end{theoren} +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. + +Let's now make some remarks which will be useful in the last section. + +Firstly, note that easy consequence of the theorem is the following: + +\begin{corollary} + 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. +\end{corollary} + +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. + +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. + +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. + +\subsubsection*{Abella} +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. + +% Two-level logic approach.... + +% Examples: in the \lc, equivalence of big-step and small-step evaluation. + +\section*{Outcomes} + +\section*{Future work} + The computer formalization of \bohm{}'s theorem would be a convenient result on its own + 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. + + 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}. + + \TODO{} + + \TODO{fireball calculus, and the algorithm we are dessigning} + + Once done with the formalization, we will adapt the formal proof to the algorithm which we are currently designing for the fireball calculus. +% e si potrebbe estendere la prova al nostro mostro + + +\bibliographystyle{plain} +\bibliography{statement} + +\end{document} -- 2.39.2