Also see Terms, Evaluation, Types, Intensional Types, Sequents, and Extraction for newer supplementary material.

This section is included for technical completeness; the beginning reader
may wish to skip this section on a first reading.
Here we shall consider only briefly the
semantics.
The complete introduction appears in section .
The semantics of
are given in terms of a system of computation
and in terms of criteria for something being a * type*,
for * equality* of types,
for something being a * member* of a given type
and for * equality* between members * in* a given type.

The basic objects of
are called * terms*.
They are built using variables and operators, some of
which bind variables in the usual sense. Each occurrence of a variable
in a term is either free or bound.
Examples of free and bound variables from other contexts are:

- Formulas of predicate logic, where the quantifiers (, )
are the binding operators. In
the two occurrences of
**x**are bound, and the occurrence of**y**is free. - Definite integral notation. In
the occurrence of
**y**is free, the first occurrence of**x**is free, and the other two occurrences are bound. - Function declarations in Pascal. In
`function Q(y:integer):integer;`

function P(x:integer):integer; begin P:=x+y end ;

begin Q:=P(y) end ;`all occurrences of``x`and`y`are bound, but in the declaration of`P``x`is bound and`y`is free.

By a * closed* term we mean a term in which no variables are free.
Central to the definitions of computation in the system is
a procedure for * evaluating* closed terms.
For some terms this procedure will not halt, and for some it will halt
without specifying a result.
When evaluation of a term does specify a result, this value will be
a closed term called a * canonical* term.
Each closed term is either canonical or * noncanonical*, and each canonical
term has itself as value.

Certain closed terms are designated as * types*; we may write ``**T** type''
to mean that **T** is a type.
Types always evaluate to canonical types.
Each type may have associated with it closed terms
which are called its * members*; we may write ``'' to mean
that **t** is a member of **T**.
The members of a type are the (closed) terms that have as values the
canonical members of the type, so it is enough when specifiying the
membership of a type to specify its canonical members.
Also associated with each type is an equivalence relation on its
members called the * equality in* (or * on*) that type;
we write ``'' to mean that **t** and **s** are members of **T**
which satisfy equality in **T**.
Members of a type are equal (in that type) if and only if their values
are equal (in that type).

There is also an equivalence relation **T = S** on types called * type equality*.
Two types are equal if and only if they evaluate to equal types.
Although equal types have the same membership and equality, in
some * un*equal types also have the same membership and equality.

We shall want to have simultaneous substitution of terms, perhaps containing free variables, for free variables. The result of such a substitution is indicated thus:

,where , are variables, and are the terms substituted for them in

What follows describes inductively the type terms in Nuprl
and their
canonical members. We use ` typewriter` font to signify actual
Nuprl
syntax.
The integers are the canonical members of the type ` int`.
There are denumerably many atom constants (written as character strings
enclosed in quotes) which are the canonical members of the type ` atom`.
The type ` void` is empty. The type ` A|B` is a disjoint union
of types

A term of the form ` t(a)` is called an

`\`

The significance of some constructors derives from the representation
of propositions as types, where the
proposition represented by a type is true if and only if the type
is inhabited.
The term ` a<b` is a type if

Types of form ` { A|B}` or

Terms of the form ` A//B` and

is inhabited.
In ` ( x,y):A//B` the

Now consider equality on the types already discussed.
Members of ` int` are equal
(in ` int`) if and only if they have the same value. The same goes for type ` atom`.
Canonical members of ` A|B`,

Now consider the so--called * universes*, ` U k` (

With the type theory in hand we now turn to the Nuprl
proof theory.
The assertions that one tries to prove in the
system are
called * judgements*.
They have the form

,where are distinct variables and and

The criterion for a judgement being * true*
is to be found in the complete introduction to
the semantics.
Here we shall say a judgement

is * almost true* if and only if

*

*
if

That is, a sequent like the one above is almost true
exactly when substituting terms of type (where
and may depend on and for **j<i**) for the
corrseponding free variables in **s** and **S** results in a true
membership relation between **s** and **S**.

It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, the extract term or any hypothesis, then the variable (and the colon following it) may be omitted.

In
it is not possible for the user to enter a complete
sequent directly; the extract term must be omitted.
In fact, a sequent is never displayed with its extract term.
The system has been designed so that upon completion of a proof,
the system automatically provides, or * extracts*, the extract term.
This is because in the standard mode of use
the user tries to prove that a certain type is inhabited without
regard to the identity of any member.
In this mode the user thinks of the type
(that is to be shown inhabited) as a proposition and assumes that it
is merely the truth of this proposition that the user wants to show.
When one does wish to show explicitly that or that ,
one instead shows the type ` ( a = b in A)`
or the type

The system can often extract a term from an incomplete proof
when the extraction is independent of
the extract terms of any unproven claims within the proof body.
Of course, such unproven claims may still
contribute to the truth of the proof's main claim.
For example, it is possible to provide an incomplete proof of
the untrue sequent ` >> 1<1 [ext axiom]`, the extract term ` axiom`
being provided automatically.

Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. In the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.

`
`

Also see Terms, Evaluation, Types, Intensional Types, Sequents, and Extraction for newer supplementary material.

Thu Sep 14 08:45:18 EDT 1995