An analysis of Böhm's theorem (Q1314351)

We analyse an important result of \(\lambda\)-calculus, the separability theorem, first proved by \textit{C. Böhm} [Alcune proprietà delle forme \(\beta\)-\(\eta\)-normali nel \(\lambda\)-\(K\)-calcolo, Pubbl. dell'Ist. Appl. Calcolo N. 696 (Roma, 1968)]. The descriptive formalism used is not the usual meta-language of Mathematics, but an actual programming language of the ML family, more specifically CAML V3.1, developed in Project Formel at INRIA Rocquencourt [\textit{G. Cousineau} and the author, The CAML primer, Rapp. Techn. 122 INRIA (1990)]. This has the advantages of being more rigorous, more constructive and of allowing better understanding by the reader who may interactively execute all definitions and examples. This article is adapted from the notes for a graduate course taught at Université Paris VII. This paper may be considered an implementation of the following suggestion, quoted from Böhm's original paper [loc. cit.]: ``Il metodo di dimostrazione per il teorema 1 e' costruttivo, percio' suggerisce di per se' un algoritmo per la costruzione delle formule''.