An analysis of Böhm's theorem (Q1314351): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: The lambda calculus, its syntax and semantics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A discrimination algorithm inside \(\lambda -\beta\)-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4204131 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5667469 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4175261 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4002456 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: REGULAR SYSTEMS OF EQUATIONS IN λ-CALCULUS / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On sets of solutions to combinator equations / rank | |||
Normal rank |
Latest revision as of 13:03, 22 May 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
0 references