marco polo/statement.tex

   1 \documentclass[10pt]{article}\r
   2 \r
   3 \title{B\"ohm's Theorem in Abella}\r
   4 \author{Andrea Condoluci}\r
   5 \date{June 30, 2017}\r
   6 \r
   7 \newcommand{\lc}[0]{{$\lambda$-calculus}}\r
   8 \newcommand{\bohm}[0]{{B\"ohm}}\r
   9 \newcommand{\TODO}[1]{\textcolor{red}{\textbf{TODO} #1}}\r
  10 \newcommand{\fire}[0]{$\lambda_{\operatorname{fire}}$}\r
  11 \r
  12 \newcommand{\conv}[1]{=_{#1}}\r
  13 \newcommand{\convb}[0]{\conv{\beta}}\r
  14 \newcommand{\convbe}[0]{\conv{\beta\eta}}\r
  15 \r
  16 \usepackage{xcolor}\r
  17 \usepackage{amsmath, amsthm, amssymb}\r
  18 \usepackage{verbatim}\r
  19 \usepackage[normalem]{ulem}\r
  20 \usepackage{cleveref}\r
  21 \r
  22 \theoremstyle{definition}\r
  23 \newtheorem{theorem}{Theorem}\r
  24 \newtheorem*{theoren}{Theorem}\r
  25 \newtheorem{lemma}[theorem]{Lemma}\r
  26 % \newtheorem{corollary}[theorem]{Corollary}\r
  27 \newtheorem*{corollary}{Corollary}\r
  28 \newtheorem*{notation}{Notation}\r
  29 \newtheorem*{definition}{Definition}\r
  30 \newtheorem{fact}[theorem]{Fact}\r
  31 \r
  32 \r
  33 \begin{document}\r
  34 \r
  35 \maketitle\r
  36 \r
  37 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
  38 \r
  39 \begin{abstract}\r
  40  \TODO{...}\r
  41 \end{abstract}\r
  42 \r
  43 \section*{Background}\r
  44 \r
  45 % \subsubsection*{Lambda Calculus}\r
  46  \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
  47  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
  48 \r
  49  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
  50 \r
  51 \subsubsection*{Separation Theorem}\r
  52  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
  53 \r
  54  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
  55 \r
  56  \begin{enumerate}\r
  57   \item any non-trivial model of the \lc{} cannot identify different $\beta\eta$-normal forms;\r
  58   \item normal forms can be explored by the only means of computational rules.\r
  59  \end{enumerate}\r
  60 \r
  61  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
  62 \r
  63 \begin{theoren}[\bohm{} theorem]\r
  64  Let $M$, $N$ be $\beta\eta$-distinct $\lambda$-terms in normal form; then there exists a context $E[\,]$ such that:\r
  65  \[\begin{array}{ll}\r
  66   E[M] & \convb \operatorname{true} \text{, and}\\\r
  67   E[N] & \convb \operatorname{false}, \\\r
  68  \end{array}\]\r
  69  where $\operatorname{true}:=\lambda x\,y.\,x$ and $\operatorname{false}:=\lambda x\,y.\,y$.\r
  70 \end{theoren}\r
  71 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
  72 \r
  73 Let us now make some remarks which will be useful in the last section.\r
  74 \r
  75 Firstly, note that an easy consequence of the theorem is the following:\r
  76 \r
  77 \begin{corollary}\r
  78  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
  79 \end{corollary}\r
  80 \r
  81 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
  82 \r
  83 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
  84 \r
  85 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
  86 \r
  87 \subsubsection*{Abella}\r
  88 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
  89 \r
  90 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
  91 \r
  92 $\nabla$\r
  93 \r
  94 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
  95 \r
  96 % Two-level logic approach....\r
  97 \r
  98 % Examples: in the \lc, equivalence of big-step and small-step evaluation.\r
  99 \r
 100 \section*{Outcomes}\r
 101 \r
 102 \TODO{\ldots, pro/contro Abella}\r
 103 \r
 104 \section*{Future work}\r
 105  The computer formalization of \bohm{}'s theorem would be a convenient result on its own\r
 106  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
 107 \r
 108  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
 109 \r
 110  \subsubsection*{The Fireball Calculus}\r
 111 \r
 112  \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
 113  \begin{itemize}\r
 114   \item it is \textit{strongly confluent};\r
 115   \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
 116  \end{itemize}\r
 117 \r
 118 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
 119 \begin{itemize}\r
 120  \item it is \textit{not} confluent;\r
 121  \item contextual equivalence is not closed under reduction.\r
 122  % a term and its strong normal form may not be contextual equivalent (in the usual sense).\r
 123  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
 124 \r
 125 \end{itemize}\r
 126 \r
 127 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
 128 \r
 129 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
 130 \r
 131  % Once done with the formalization, we will adapt the formal proof to the algorithm which we are currently designing for the fireball calculus.\r
 132 % e si potrebbe estendere la prova al nostro mostro\r
 133 \r
 134 \r
 135 \bibliographystyle{plain}\r
 136 \bibliography{statement}\r
 137 \r
 138 \end{document}\r