A completeness theorem for recursively defined types. (English) Zbl 0585.68047

Automata, languages and programming, 12th Colloq., Nafplion/Greece 1985, Lect. Notes Comput. Sci. 194, 120-129 (1985).
Summary: [For the entire collection see Zbl 0563.00018.]
In this paper the notion of recursively defined type for a functional language is studied. The semantics of types (which are interpreted as subsets of a type-free domain following R. Milner [J. Comput. Syst. Sci. 17, 348-375 (1978; Zbl 0388.68003)]) is built by successive approximations. Using the properties of our construction, an algorithm to decide semantic equality between (recursively defined) types is given. Moreover a system of formal rules to assign types to terms, which is complete with respect to the above semantics, is introduced. A recursive subsystem is complete for terms in normal form.


68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
03B40 Combinatory logic and lambda calculus