The
semantics is a variation on that given by Martin-Löf
for
his type theory [Martin-Löf 82]. There are three stages in the semantic specification:
the
computation system,
the type system and
the so--called judgement forms. Here
is how we shall proceed.
We shall specify a computation system consisting of terms,
divided
into canonical and
noncanonical , and a procedure for
evaluating
terms which for a given term t returns at most one canonical term,
called the value of t.
In
whether a term is canonical depends only on the
outermost form of the term, and there are terms which
have no value.
We shall write 
to mean that s has value t.
Next we shall specify a system of types. A type is a term T (of the
computation system) with which is associated a transitive, symmetric
relation, 
, which respects evaluation in t and s;
that is, if T is a type and 
and 
, then 
if and only if 
.
We shall sometimes say ``T type'' to mean that T is a type.
We say t is a member of T, or 
, if 
.
Note that 
is an equivalence relation (in t and s)
when restricted to members of T.
Actually, 
is a three--place relation on terms which respects evaluation
in all three places. We also use a transitive, symmetric relation on
terms, T=S, called type equality,
which 
respects in T; that is,
if T=S then 
if and only if 
.
The relation T=S respects evaluation in T and S,
and T is a type if and only if T=T.
The restriction of T=S to types is an equivalence relation.
For our purposes, then, a type system for a given
computation system
consists of a two--place relation T=S and a three--place relation 
on terms such that
T=S is transitive and symmetric;We define ``T type'' and ``
T=S if and only if&
;
is transitive and symmetric in t and s;
if and only if
&
;
T=T if;
if T=S &
.
'' by
T type if and only if T=T;
if and only if
.
Finally, so--called judgements will be explained. This requires
consideration of terms with free variables
because substitution of closed
terms for free variables is central to judgements as presented
here.
In the description of semantics given so far
``term'' has meant a closed term, i.e., a term with no free variables.
There is only one form of judgement in
,
:
,
,
:
>> S [ext s],
which in the case that n is 0 means 
.
The explanation of the cases in which n is not 0 must wait.