Computing with recursive types

Abstract

A study is made of the complete adequacy for a λ-calculus with simple recursive types. The set of types is built using the standard domain-theoretic constructors, namely, function space, sum, cartesian and strict product, and lifting. The recursive types allow the author to solve arbitrary (systems of mutually) recursive domain equations. Thus, he can define in this calculus types of integers, Booleans, lists and streams over these, and so on. The author can also define numerals, Boolean constants, simple arithmetic functions, fixed-point operators at all types, and typed versions of pure untyped terms. A precise description is given of the author's calculus, as well as some examples illustrating its expressiveness. A complete adequacy result for the lattice semantics is presented. The problem of designing a completely adequate evaluator for the CPO semantics is also examined.