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.

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