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

03B40 Combinatory logic and lambda calculus
03B25 Decidability of theories and sets of sentences