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 \r
  11 \usepackage{xcolor}\r
  12 \usepackage{amsmath, amsthm, amssymb}\r
  13 \usepackage{verbatim}\r
  14 \usepackage[normalem]{ulem}\r
  15 \usepackage{cleveref}\r
  16 \r
  17 \theoremstyle{definition}\r
  18 \newtheorem{theorem}{Theorem}\r
  19 \newtheorem*{theoren}{Theorem}\r
  20 \newtheorem{lemma}[theorem]{Lemma}\r
  21 % \newtheorem{corollary}[theorem]{Corollary}\r
  22 \newtheorem*{corollary}{Corollary}\r
  23 \newtheorem*{notation}{Notation}\r
  24 \newtheorem*{definition}{Definition}\r
  25 \newtheorem{fact}[theorem]{Fact}\r
  26 \r
  27 \r
  28 \begin{document}\r
  29 \r
  30 \maketitle\r
  31 \r
  32 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
  33 \r
  34 \begin{abstract}\r
  35  \TODO{...}\r
  36 \end{abstract}\r
  37 \r
  38 \section*{Introduction}\r
  39 \r
  40 % \subsubsection*{Lambda Calculus}\r
  41  \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
  42  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
  43 \r
  44  \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
  45 \r
  46 \subsubsection*{Separation Theorem}\r
  47  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
  48 \r
  49  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
  50 \r
  51  \begin{enumerate}\r
  52   \item any non-trivial model of the \lc{} cannot identify different $\beta\eta$-normal forms;\r
  53   \item normal forms can be explored by the only means of computational rules.\r
  54  \end{enumerate}\r
  55 \r
  56  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
  57 \r
  58 \begin{theoren}[\bohm{} theorem]\r
  59  Let $M$, $N$ be $\beta\eta$-distinct $\lambda$-terms in normal form; then there exists a context $E[\,]$ such that:\r
  60  \[\begin{array}{ll}\r
  61   E[M] & \equiv_{\beta} \operatorname{true} \text{, and}\\\r
  62   E[N] & \equiv_{\beta} \operatorname{false}, \\\r
  63  \end{array}\]\r
  64  where $\operatorname{true}:=\lambda x\,y.\,x$ and $\operatorname{false}:=\lambda x\,y.\,y$.\r
  65 \end{theoren}\r
  66 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
  67 \r
  68 Let's now make some remarks which will be useful in the last section.\r
  69 \r
  70 Firstly, note that easy consequence of the theorem is the following:\r
  71 \r
  72 \begin{corollary}\r
  73  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
  74 \end{corollary}\r
  75 \r
  76 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
  77 \r
  78 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
  79 \r
  80 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
  81 \r
  82 \subsubsection*{Abella}\r
  83 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
  84 \r
  85 % Two-level logic approach....\r
  86 \r
  87 % Examples: in the \lc, equivalence of big-step and small-step evaluation.\r
  88 \r
  89 \section*{Outcomes}\r
  90 \r
  91 \section*{Future work}\r
  92  The computer formalization of \bohm{}'s theorem would be a convenient result on its own\r
  93  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
  94 \r
  95  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
  96 \r
  97  \TODO{}\r
  98 \r
  99  \TODO{fireball calculus, and the algorithm we are dessigning}\r
 100 \r
 101  Once done with the formalization, we will adapt the formal proof to the algorithm which we are currently designing for the fireball calculus.\r
 102 % e si potrebbe estendere la prova al nostro mostro\r
 103 \r
 104 \r
 105 \bibliographystyle{plain}\r
 106 \bibliography{statement}\r
 107 \r
 108 \end{document}\r