The insensitivity theorem for nonreducing reflexive types (Q792755)

The paper is concerned to the problem of deciding which are the useful types for typed \(\lambda\)-expression programming languages (ALGOL 68, LISP, etc.). In the first section the authors present the concept of reducing type and their hierarchies of finite and infinite types. In a previous paper by the authors [Lect. Notes Comput. Sci. 85, 38-50 (1980; Zbl 0444.68026)], they showed that the nonreducing types are useless for primitive functions of first order type and for terms having the same meaning if they behave in the same way in any program (fully abstract semantics). This result comes from a more general and stronger syntactic result, obtained in the present paper (Insensitivity Theorem): contexts of finite type and closed with respect to variables of reflexive type are insensitive to differences between terms of nonreducing type. Formally, the theorem is the following: if \(M^ 1\), \(M^ 2\) are two terms of the same nonreducing type, C[] a context for them and \(C[M^ 1]\), \(C[M^ 2]\) are i-closed terms of finite type, then \(val(C[M^ 1])=val(C[M^ 2])\) (val denoting the ''syntactic'' value of a term). A main consequence is that nonreducing types are useless within a fully abstract semantics. The third section illustrates the role played by the concept of reducing type in applicative language modelling. Semantics (defined by models) and full abstraction concepts are introduced and the insensitivity theorem related to a new programming languages design principle. Finally, hints about further researches on this topic are given.