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

Coppo, M.

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.

MSC:

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

Keywords:

functional language; semantics of types; type-free domain; algorithm to decide semantic equality

Citations:

Zbl 0563.00018; Zbl 0388.68003