Böhm's theorem

Böhm's separation theorem, or simply Böhm's theorem, is one of fundamental theorems of the λ-calculus, proved by Corrado Böhm in 1968.

It expresses the fact that two syntactically distinct programs (βη-distinct normalising terms) are observationally distinct (they produce different values when both fed with some well-chosen arguments), see  .

An important consequence is that two η-distinct β-normal terms (two “results”) correspond to different denotations (“meanings”) in any consistent model.

The proof of the theorem is striking because it consists in separating any η-distinct β-normal λ-terms:

• internally: the terms are separated inside the dynamics of the λ-calculus, hence this separation must be mirrored by any (consistent) model,
• constructively: the evidence of this separation is constructed by the proof, using what has been later called the Böhm-out technique.

The theorem

Let $\Lambda _{N}$ be the set of all β-normal λ-terms.

Given a λ-term $M$, we denote by ${\overline {M}}$ a closure of $M$, i.e. ${\overline {M}}=\lambda x_{1}\dots \lambda x_{n}.M$ where $x_{1},\dots ,x_{n}$ is an enumeration of the free variables of $M$.

Theorem  (Böhm 1968)

Let $M,N\in \Lambda _{N}$ be β-normal λ-terms. Then either $M=_{\eta }N$, or there are λ-terms $P_{1},\dots ,P_{n}$ such that

$${\overline {M}}P_{1}\dots P_{n}\rightarrow _{\beta }^{*}{\mathsf {true}}\quad {\text{and}}\quad {\overline {N}}P_{1}\dots P_{n}\rightarrow _{\beta }^{*}{\mathsf {false}}.$$

Usually one takes ${\mathsf {true}}=\lambda x.\lambda y.x$ and ${\mathsf {false}}=\lambda x.\lambda y.y$, but they can be replaced with any other λ-terms $Q_{M}$ and $Q_{N}$:

$${\overline {M}}P_{1}\dots P_{n}Q_{M}Q_{N}\rightarrow _{\beta }^{*}Q_{M}\quad {\text{and}}\quad {\overline {N}}P_{1}\dots P_{n}Q_{M}Q_{N}\rightarrow _{\beta }^{*}Q_{N}.$$

A proof sketch is given by Guerrini et al. (2009). The full proof is presented in Barendregt (1984, ch. 10). Its constructive fashion is taken seriously by Huet (1993), who presents a CaML code proving the theorem. A simpler proof can be found in Joly (2000, ch. 10).

Corollary 

If a model equates βη-distinct normal λ-terms, then it equates all λ-terms.

Böhm theorems in other calculi

Typed versions of Böhm's theorem have been established by Joly (2000, ch. 2) and Došen and Petrić (2001).

A Böhm theorem for the Λμ-calculus (a variant of the λμ-calculus) is designed by Saurin (2012), while the traditional λμ-calculus does not enjoy the separation property.

A Böhm theorem for differential interaction nets is designed by Mazza and Pagani (2007).

References

The theorem was originally proved in:

• C. Böhm (1968), “Alcune proprietà delle forme β-η-normali nel λ-$K$-calcolo”, Pubblicazioni dell'Istituto per le applicazioni del calcolo no. 696, URL: https://www.ens-lyon.fr/LIP/REWRITING/TYPES_AND_L_CALCULUS/bohm696.pdf.

A presentation of the theorem is given in:

• S. Guerrini, A. Piperno and M. Dezani-Ciancaglini (2009), “Böhm's Theorem”, in E. Gelenbe and J.-P. Kahane (ed.), Fundamental Concepts in Computer Science, DOI: 10.1142/9781848162914_0001, URL: https://www.worldscientific.com/doi/suppl/10.1142/p596/suppl_file/p596_chap01.pdf.

Other cited references:

• H. P. Barendregt (1984), The Lambda Calculus. Its Syntax and Semantics.
• G. Huet (1993), “An analysis of Böhm's theorem”, Theoretical Computer Science vol. 121 no. 1-2, DOI: 10.1016/0304-3975(93)90087-A.
• K. Došen and Z. Petrić (2001), “The Typed Böhm Theorem”, in J.-J. Lévy (ed.), Böhm's theorem: applications to Computer Science Theory, Electronic Notes in Theoretical Computer Science, DOI: 10.1016/S1571-0661(04)00168-9.
• T. Joly (2000), Codages, séparabilité et représentation de fonctions en λ-calcul simplement typé et dans d'autres systèmes de types, PhD thesis, Université Paris 7.
• D. Mazza and M. Pagani (2007), “The separation theorem for differential interaction nets”, in Proceedings of the 14th international conference on Logic for programming, artificial intelligence and reasoning (LPAR'07), DOI: 10.5555/1779419.1779448.
• A. Saurin (2012), “Böhm theorem and Böhm trees for the Λμ-calculus”, Theoretical Computer Science vol. 435, DOI: 10.1016/j.tcs.2012.02.027.