A New Model Construction for Higher Type Systems
by
Dieter Spreen
Universität--GH Siegen

We present a model for the Girard-Reynolds second order lambda calculus which is not based on Scott domains. In this model types are interpreted as inverse limits [T\vec] of co-chains T₀ <-- ^p₀ T₁ <-- ^p₁ ... of finite topological T₀-spaces such that the mappings p_i are continuous and onto. The morphisms from [T\vec] to [(T')\vec] are sequences (f_i)_{i >= 0} of maps f_i in [T_i --> T'_']. Here [T₀ --> T'₀] is the set of all continuous maps from T₀ into T'₀ and for i > 0, [T_i --> T'_i] is the set of those continuous maps f : T_i --> T'_i such that f \approx f and [f] _\approx in [T_i-1 --> T'_i-1] where \approx is the partial equivalence relation defined by

f \approx g iff ( for ally, z in Ti) [pi(y) = pi(z) implies pi'(f(y)) = pi'(g(z))]

and [f] _\approx is the equivalence class of f under this relation. The spaces of all morphisms from [T\vec] to [(T')\vec] is thus again an inverse limit of a co-chain of finite T₀-spaces. Moreover, its i^th approximation depends only on the first i+1 approximations of [T\vec] and [(T')\vec], which means that it is rank preserving.

For each such constructor F a space \prodF can be constructed such that its i^th approximation contains i-tuples of elements of the first i+1 approximations of F([T\vec]) for certain spaces [T\vec]. Moreover, a mapping Apply is defined such that for t in \prodF Apply(t, [T\vec]) in F([T\vec]). This is used to give meaning to the \Pi-type of second order lambda calculus.

Just as in the case of the function space dependent sums and products can be defined by taking them componentwise. In the same way one obtains power spaces. Thus, the model extends to a model of more powerful type systems.

Since the empty set can also be obtained as an inverse limit of a co-chain of finite T₀-spaces, it follows that \prodX ·X = \emptyset. If one requires that the lowest set of any co-chain is the one-point space, then \prodX ·X =/= \emptyset. In case that only co-chains with | T_i | <= i are considered, then a slight modification of the construction yields a model of the Calculus of Construction.

Date received: April 12, 1996

Copyright © 1996 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # caaf-79.