An analysis of Böhm's theorem (Q1314351): Difference between revisions
From MaRDI portal
Changed an Item |
Changed an Item |
||
Property / describes a project that uses | |||
Property / describes a project that uses: ML / rank | |||
Normal rank |
Revision as of 17:24, 29 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | An analysis of Böhm's theorem |
scientific article |
Statements
An analysis of Böhm's theorem (English)
0 references
28 August 1994
0 references
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''.
0 references
\(\lambda\)-calculus
0 references
separability theorem
0 references