\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}}
\newcommand{\fire}[0]{$\lambda_{\operatorname{fire}}$}

\newcommand{\conv}[1]{=_{#1}}
\newcommand{\convb}[0]{\conv{\beta}}
\newcommand{\convbe}[0]{\conv{\beta\eta}}

\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*{Background}

% \subsubsection*{Lambda Calculus}
 \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.
 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.

 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.

\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 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$.

\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] & \convb \operatorname{true} \text{, and}\\
  E[N] & \convb \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 problems in other $\lambda$-theories.

Let us now make some remarks which will be useful in the last section.

Firstly, note that an 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.

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.

$\nabla$

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).

% Two-level logic approach....

% Examples: in the \lc, equivalence of big-step and small-step evaluation.

\section*{Outcomes}

\TODO{\ldots, pro/contro Abella}

\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 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).

 \subsubsection*{The Fireball Calculus}

 \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:
 \begin{itemize}
  \item it is \textit{strongly confluent};
  \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.
 \end{itemize}

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:
\begin{itemize}
 \item it is \textit{not} confluent;
 \item contextual equivalence is not closed under reduction.
 % a term and its strong normal form may not be contextual equivalent (in the usual sense).
 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.

\end{itemize}

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}.

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.

 % 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}
