[Prev][Next][Index][Thread]
intensional type theory , modified realizability
Date: Wed, 27 May 1992 15:46:00 +0200
TRULY INTENSIONAL MODELS OF TYPE THEORY ARISING FROM MODIFIED REALIZABILITY
The definition of what is a model structure for intensional Martin-Loef
Type Theory has been given by John Cartmell in his Thesis (Oxford 1978).
Essentially it is like semantics for extensional type theory with the only
exception that one drops uniqueness constraints and replaces them by the
constraint that Eliminators are preserved by substitution.
There has been described quite a lot of models for extensional type theory
mainly based on the idea of Kleene realizability. The most important
structure in this context is the category of so called realizability sets
which we will refer to by r-Set and the full reflective internally
complete subcategory PER. It seems to be impossible to find truly
intensional models for type theory in this setting as extensionality is
built in almost by definition. (Extensionality for me means that the
terminal object is a generator).
But instead of considering a category of Kleene realizability sets one can
also build a category based on Kreisel's Modified Realizability. Whereas
in Kleene realizability propositions are considered as arbitrary sets of
natural numbers the key idea of modified realizability is to endow any
such set A of natural numbers with a subset B. The set A has to be
thought of as the collection of potential realizers and the subset B as
the collection of ACTUAL REALIZERS.
This intuitive idea can be lifted to realizability sets. Based on the
category r-Set of realizability sets we construct a category mr-Set of so
called "modified realizability sets".
Description of mr-Set:
objects: triples ( X , d(X) , r(X) ) such that
(1) X is a set
(2) d(X) is a subset of X
(objects in d(X) will be called "defined")
(3) ( X , r(X) ) is an r-set , i.e.
r(X) is a relation between natural numbers
and X such that for any x in X there
is a natural number n with n r(X) x
morphisms: a morphism from ( X , d(X) , r(X) ) to ( Y , d(Y) , r(Y) )
is a set-theoretic function f : X -> Y such that
(1) f (x) is in d(Y) provided that x is in d(X)
(i.e. f preserves actual realizers !)
(2) f is a morphism from ( X , r(X) ) to ( Y , r(Y) )
in r-Set
( i.e. there is a natural number n such that for
all x in X and m with m r(X) x:
{n}(m) is defined and {n}(m) r(Y) f(x) ).
More abstractly the category mr-Set can be described as the result of the
Grothendieck construction applied to the fibration of REGULAR MONOs in
r-Set over r-Set . The category r-Set is a full reflective subcategory of
mr-Set by the embedding sending
( X , r(X) ) to ( X , X , r(X) ) .
THEOREM Just as r-Set is locally cartesian closed so is mr-Set.
The category mr-Set is not extensional.
Proof : Obviously, mr-Set has finite limits. The Pi-s are computed as in
r-Set , BUT elements are defined iff they preserve definedness. The
underlying r-set of the terminal object in mr-Set is the terminal object
in r-Set and all elements are defined. Of course, there exist two
different parallel morphisms in mr-Set which coincide on defined elements
and such morphisms cannot be separated by global elements, i.e. morphism
whose source is the terminal object.
As mr-Set is left exact it constitutes a model of extensional type theory.
Nevertheless we can interpret intensional identity typs in a way such that
they do not fulfill the laes of extensional identity types. For this
purpose we consider mr-Set as a model of the ambient logical framework.
For what Martin-Loef calls "constructive set theory" we have to identify a
certain full subcategory of mr-Set.
DEFINITION A small set is an object ( X , d(X) , r(X) ) in
mr-Set such that
(1) n r(X) x1 and n r(X) x2 implies x1 = x2
(2) for some object x in X we have 0 r(X) x .
In the sequel we shall need two distinguished small sets:
Succeed = ( {e , r} , {r} , { ( 0 , e ) , (1 , r ) }) and
Fail = ( {e} , {} , { (0,e) } ) .
Now we shall interpret Martin-Loef's identity types in mr-Set in
such a way that they do not satisfy the laws of extensional identity
types.
If A is a small set and a1, a2 are objects of the underlying set of A then
Id A a1 a2 = Fail if a1 and a2 are different
Id A a a = Succeed .
For any small set A and a in A (not necessarily defined!)
r A a = r .
Finally we give the definition of the elimination operator J .
Given A : Set and a family
C : {a1 , a2 : A} {c : Id A a1 a2} Set and a function
d : {a : A} C a a (r A a)
the function
J A C d : {a1 , a2 : A} {c : Id A a1 a2} C a1 a2 c
is defined as follows
J A C d a a r = d a
J A C d a1 a2 e = the unique object in C a1 a2 e
realized by 0 .
Obviously, J is realizable as one simply performs a decidable case
analysis on the realizer for the lasr argument.
THEOREM The following sequents are NOT valid in this model:
(1) A : Set , x : A , y : A , z : Id A x y |- x = y : A
[ but, of course, theer is a term t such that
A : Set , x : A , y : A , z : Id A x y
|- t : Id Ax y : A ]
(2) A : Set , C : A -> Set , x : A , y : A , z : Id A x y
|- C x = C y
(PUT for A a small set with at least two different objects a and b where
a is assumed to be defined and for C the family [x:A] Id A a x ; then we
have
Id A a a = Succeed, but
Id A a b = Fail
although e : Id A a b .)
(3) The so-called Equality Reflection Lemma (terminology of LuoBs Thesis)
holds
If |- p : Id A t s is valid in the model
then |- t = s : A is valid in the model, too.
(The restriction to the empty context is important, see (1) ! The
interpretation of the empty context contains one defined and no
undefined object ! ).
THEOREM In the model defined above the principle of extensionality
{A,B : Set} {f,g : A->B} ({x:A} Id B (f x) (g x)) -> Id (A->B) f g
is NOT realized !!
Proof : by a continuity argument !!
//** In General Leibniz Equality is different from Martin-Loef Idenity
Types **//
Interpret Prop as small sets and interpret Type(0) as those mr-sets where
the underlying r-set is a per.
Then both Prop and Type(0) are closed under arbitrary internal products.
In Type(0) we can interpret (even extensional) Martin-Loef identity types
as we have mr-sets whose underlying r-set is empty. On the other hand we
can define Leibniz equality employing Prop.
Now let A be a type containing ar least two different defined elements a1
and a2 . Then LE A a1 a2 is in Prop containing no defined element BUT
surely a nondefined element realized by 0. Id A a1 a2 contains not even
an undefined element.
Therefore there cannot exist a morphism from LE A a1 a2 to Id A a1 a2 !!
Thomas Streicher