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 ``'' by
T=S if and only if & ;
is transitive and symmetric in t and s;
if and only if & ;
T=T if ;
if T=S & .
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.