| Tyep definitions and lazy evaluation are important concepts for enhancing the expressive power of applicative languages. A first-order applicative system incorporating both these concepts of orthogonal features is studied.; A class of algebraic specifications called firm types is proposed as a type definition method. A semantic model for types, based on Scott's theory of domains, is constructed. It is shown that each firm type corresponds to a complete partially ordered domain of values, including, in general, infinite values.; The primitive functions on a type can be described by sets of equations. The notion of a reduction system is introduced as a self-contained collection of types and functions defined by equations. The correspondence between the operational behavior of functions, based on reductions, and a semantic model based on Scott's approximable maps, is established. The continuity and referential transparency of the operational behavior of functions is demonstrated.; Loose types are introduced as a generalization of firm types, in order to deal with loose structures such as multisets. It is shown that loose types which satisfy certain conditions admit a continuous semantics. |
