Also see Types for supplementary material.

next up previous contents index
Next: Substitution Up: The Rules Previous: The Rules



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

next up previous contents index
Next: Substitution Up: The Rules Previous: The Rules

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995