λ-Terms as total or partial functions on normal forms
iff when auccessively applied to any number of normal forms it gives a λ-term without normal form
(0<h<ω) iff when successively applied to h-1 arbitrary normal forms it gives a λ-term without normal form, but there exist h normal forms X1,...,Xh such that FX1...Xh possesses normal form
(0≤h>ω) iff when successively applied to h arbitrary normal forms it gives a λ-term which possesses normal form, but there exist h+1 normal forms X1,...,Xh+1 such that FX1...Xh+1 possesses no normal form
iff when successively applied to any number of normal forms it gives a λ-term which possesses normal form.
This classification can be effectively determined only for λ-terms in normal form.
KeywordsNormal Form Terminal Node Reduction Algorithm Current Variable Tree Representation
Unable to display preview. Download preview PDF.
- Böhm,C., The CUCH as a Formal and Description Language, Formal Language Description Languages for Computer Programming, ed.T.B. Steel, North-Holland, Amsterdam, (1966), 179–197.Google Scholar
- Böhm,C., M.Dezani-Ciancaglini, Combinatorial Problems Combinator Equations and Normal Forms, Automata Languages and Programming, ed. J. Loeckx, Lecture Notes in Computer Science, 14, Springer-Verlag, (1974), 185–199.Google Scholar
- Church,A., J.Barkley Rosser, Some properties of λ-conversion, Trans.Amer. Math Soc., 39, (1936), 472–482.Google Scholar
- Curry, H.B., J.R. Hindley, J.P. Seldin, Combinatory Logic, 2, North-Holland, Amsterdam, (1972).Google Scholar
- Knuth, D.E., Examples of Formal Semantics, Symposium on Semantics of Algorithmic Languages, 188, ed. E. Engeler, Springer-Verlag, Berlin, (1970), 212–235.Google Scholar
- Simone, C., Un modello di λ-calcolo fortemente equivalente agli schemi ricorsivi, Calcolo, 1, (1974), 111–125.Google Scholar
- Wadsworth, C.P., Semantics and Pragmatics of λ-calculus, Ph.D. Thesis, Oxford, (1971).Google Scholar
- Welch, P.H., Continuous Semantics and Inside-Outside Reductions, these Proceedings.Google Scholar