An analysis of Böhm's theorem (Q1314351): Difference between revisions

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
Added link to MaRDI item.
links / mardi / namelinks / mardi / name
 

Revision as of 12:59, 31 January 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
    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
    0 references
    \(\lambda\)-calculus
    0 references
    separability theorem
    0 references