[Prev][Next][Index][Thread]
new model for second order lambda calculus and other type theories
This note is to announce a new model construction for the
Girard-Reynolds second order lambda calculus. The interpretation of
the ForAll-type in this model is different from the usual one.
Types are interpreted as inverse limits TT of co-chains
T_0 <--p_0-- T_1 <--p_1-- ...
of finite topological T_0-spaces such that the mappings p_i are continuous
and onto. The morphisms from TT to TT' are sequences (f_i) of maps f_i \in
[T_i --> T'_i]. Here [T_0 --> T'_0] is the set of all continuous maps from
T_0 into T'_0 and for i > 0, [T_i --> T'_i] is the set of those continuous
maps f: T_i --> T'_i such that f~f and [f]~ \in [T_{i-1} --> T'_{i-1}] where
f~g iff
(forall y, z \in T_i) [if p_i(y) = p_i(z) then p'_i(f(y)) = p'_i(g(z))]
and [f]~ is the equivalence class of f under this relation. The space
of all morphisms from TT to TT' is thus again an inverse limit of a
co-chain of finite T_0-spaces. Moreover, its i-th approximation
depends only on the first i+1 approximations of TT and TT', which
means that it is rank preserving.
For each such constructor F a space \Pi F can be constructed such that
its i-th approximation contains i-tuples of elements of the first i+1
approximations of F(TT) for certain spaces TT. Moreover, a mapping
Apply is defined such that for t \in \Pi F Apply(t,TT) \in F(TT). This
is used to give meaning to the ForAll-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_0-spaces, it follows that \Pi X.X is empty. If
one requires that the lowest set of any co-chain is the one-point
space, then \Pi X.X is not empty.
In case that only co-chains with cardinality of T_i being not greater
than i are considered, a slight modification of the construction
yields a model of the Calculus of Construction in which kinds are
interpreted as special rank- ordered sets. Note to this end that each
space TT as well as the collection of all such spaces is rank-ordered.
Moreover, the collection of all rank-ordered sets is closed under the
different types of dependent sums and products used in the Calculus of
Construction.
==============================================================
Prof. Dr. Dieter Spreen
Theoretische Informatik
Universitaet Siegen
D-57068 Siegen
Germany
Tel.: +49 (0)271 740 3165
+49 (0)271 740 2300 (secretary)
Fax.: +49 (0)271 740 2532
email: spreen@informatik.uni-siegen.de
==============================================================