An algorithm to add two integers can be expressed in Nuprl
as
. In general, if is an
expression such as or in
the variable **x**, then
is the function of one argument which on input **a** computes the
value , where stands for the expression
**b** with each occurrence of **x** replaced by **a**.
Application of the function is expressed by
; for example, .
We speak of as the * abstraction * of with
respect to **x**. This notation is essentially the same as Church's
lambda notation, which is systematized in the * lambda calculus* [Church 51].
The form is a visual approximation
to of the lambda calculus. Our notation is also very close
to that used in ML [Gordon, Milner, & Wadsworth 79] except that type information about
the variable can be included in the ML form.
This marks a significant departure from
the Algol--like
languages as well, for in these languages
the type information is given with the parameters of
a function.
For example, one would write
in the heading of an Algol function
definition to show that the function maps integers to integers.

In Nuprl
, as in the work of H.B. Curry [Curry, Feys, & Craig 58,Curry, Hindley, & Seldin 72], a type discipline
is imposed on algorithms to describe their properties. Thus, when we say that
is a function from integers to integers, we are saying that
when an integer **n** is supplied as an argument to this algorithm, then
**n+1** will denote a specific integer value. In general, meaning is given to
a function term by saying that it has type
for some
type **A** called the * domain* and some type **B** called the * range*. The type
denotes
functions which on input **a** from **A** produce a value in
**B**. The fact that the functions always return a value is sometimes
emphasized by calling them * total
functions*.

The type structure hierarchy of
resembles that of
* Principia Mathematica*, the ancestor of all type theories.
The hierarchy manifests itself in an unbounded cumulative hierarchy of
universes, , , ...,
where by cumulative hierarchy we mean that is in and
that every element of is also an element of .
Universes are themselves types,
The concept of a universe in this role, to organize the hierarchy
of types, is suggested in [Artin, Grothendieck, & Verdier 72] and was used by
Martin-Löf
[Martin-Löf 73].
This is a means of achieving a * predicative* type structure as
opposed to an * impredicative* one as in Girard [Girard 71] or
Reynolds [Reynolds 83].
and
every type occurs in a universe. In fact, **A** is a type
if and only if it belongs to a universe.
Conversely
all the elements of a universe are types.

It is pedagogically helpful to think of the other
types in five
stages of decreasing familiarity. The most familiar types and type
constructors are similar to those found in typed programming languages
such as Algol 68, ML or Pascal. These include the atomic types ` int`,
` atom`
and ` void` along with the three basic constructors :
cartesian product, disjoint union and function space.
If **A** and **B** are types,
then so is their cartesian product, ` A#B`, their disjoint union,

The second stage of understanding includes the dependent

function and dependent product constructors,
which are written
as ` x:A->B` and

The third stage of understanding includes the quotient and set types
introduced in [Constable 85]. The set type is written
` x:A|B
`
and allows
to express the notions of constructive set and of
partial function. The quotient type allows
to capture the
idea of equivalence class used extensively in algebra to build new
objects.

The fourth stage includes propositions considered as types.
The atomic types of this form are written ` a = b in A` and express
the
proposition that

The fifth stage includes the recursive types and the type of partial

functions as presented by Constable and N. P. Mendler [Constable & Mendler 85]. These are discussed in chapter 12, but they have not been completely implemented so we do not use them in examples taken directly from the computer screen. These are the only concepts in this book not taken directly from the 1984 version of the system.

The logical language is interesting on its own. It is built around tested logical notions from H. Curry, A. Church, N. deBruijn, B. Russell, D. Scott, E. Bishop, P. Martin-Löf and ourselves among others and as such forms part of a well--known and thoroughly studied tradition in logic and philosophy. However, this tradition has not until now entered the realm of usable formal systems and automated reasoning in the same way as the first--order predicate calculus. Thus the design and construction of this logic is a major part of , and becoming familiar with it will be a major step for our readers. We recommend in addition to this account the forthcoming book of B. Nordström, K. Petersson and J. Smith, the paper ``Constructive Validity'' [Scott 70], the paper ``Constructive Mathematics and Computer Programming'' [Martin-Löf 82] and ``Constructive Mathematics as a Programming Logic'' [Constable 85]. An extensive guide to the literature appears in the references. We hope that this account will be sufficient to allow readers to use the system, which in the end may be its own best tutor.

Thu Sep 14 08:45:18 EDT 1995