##
**An ideal model for recursive polymorphic types.**
*(English)*
Zbl 0636.68016

The paper presents a construction of a model for polymorphic recursive types which extend the type system of D. B. MacQueen and R. Sethi [(*) “A higher order polymorphic type system for applicative languages”, Symp. LISP Functional Programming, Pittsburgh, 1982, 243- 252]. Basic intuitions underlying polymorphic types are given, constructions on complete partial orders are summarized and domains introduced. Type expressions are interpreted as certain subsets of the value space. First, an account of modelling of types using weak ideals of the value space according to (*) is presented, then recursive equations are solved by considering the convergence of particular sequences of types.

As far as the converging sequences may be in general neither monotonically increasing or decreasing, a metric structure of types is introduced in order to establish the existence and uniqueness of solutions. Using Banach fixed-point theorem, existence of unique fixed points is established for a class of contractive functions on metric spaces. Various constructions are discussed in connection with contractive functions and the applicability of this result to the metric space of types is shown. The general results obtained are used for defining a semantics of type expressions permitting recursion and universal and existential quantification. A set of type-inference rules is presented, and its soundness is proved.

In the appendix, a variant of the theory, the strong ideals from (*), is considered; analogous results hold true for strong ideals as well, except that certain of the type-inference rules are no longer sound.

As far as the converging sequences may be in general neither monotonically increasing or decreasing, a metric structure of types is introduced in order to establish the existence and uniqueness of solutions. Using Banach fixed-point theorem, existence of unique fixed points is established for a class of contractive functions on metric spaces. Various constructions are discussed in connection with contractive functions and the applicability of this result to the metric space of types is shown. The general results obtained are used for defining a semantics of type expressions permitting recursion and universal and existential quantification. A set of type-inference rules is presented, and its soundness is proved.

In the appendix, a variant of the theory, the strong ideals from (*), is considered; analogous results hold true for strong ideals as well, except that certain of the type-inference rules are no longer sound.

Reviewer: J.Zlatuska

### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

03B40 | Combinatory logic and lambda calculus |

68Q65 | Abstract data types; algebraic specification |

03C99 | Model theory |