# zbMATH — the first resource for mathematics

Termination tests inside lambda-calculus. (English) Zbl 0358.02025
Automata, languages and programming, 4th Colloq., Turku 1977, Lect. Notes Comput. Sci. 52, 95-110 (1977).
[This article was published in the book announced in Zbl 0349.00016.]
The aim of this paper is to investigate the termination property, i.e., the property to have normal form, of terms of $$\lambda$$-calculus of the shape $$NX_1\dots X_r$$ where $$N,X_1,\dots, X_r$$ are terms in normal form. This is done by characterizing (constructively) a domain $$C(N,r) \in {\mathcal N}^r$$ (where $$r$$ is a positive integer and $${\mathcal N}$$ is the set of terms in normal form) such that for all $$X_1,\dots ,X_r \in C(N,r)$$ the term $$NX_1\dots X_r$$ reduces to a normal form. If we interpret $$N$$ as a function, $$C(N,r)$$ represents a domain onto which $$N$$ is total and, therefore, it is contained in the (semidecidable) domain of total convergence of $$N$$. These two domains coincide if and only if $$C(N,r)={\mathcal N}^r$$. The decidability of this relation has been shown (also constructively) in a previous work by C. Böhm and M. Dezani-Ciancaglini [Lect. Notes Comput. Sci. 37, 96–121 (1975; Zbl 0342.02017)]. The characterization of $$C(N,r)$$ is done by coding some features of $$N$$ and $$X_1,\dots ,X_r$$ by means of lists of integers and comparing them. Further investigations of termination properties of terms have been done (by M. Coppo and M. Dezani-Ciancaglini) by introducing a new functionality theory in which types represent termination properties of terms.
Reviewer: C. Böhm
Show Scanned Page ##### MSC:
 03B40 Combinatory logic and lambda calculus 03B25 Decidability of theories and sets of sentences