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, A|B, and the
functions from A to B, A->B.
The second stage of understanding includes the dependent
function and dependent product constructors,
which are written
as x:A->B and x:A#B, respectively, in Nuprl
.
The dependent function space is used in AUTOMATH and the
dependent product was suggested by logicians studying the correspondence
between propositions and types; see Scott [Scott 70] and
Howard [Howard 80]. These types will be explained in detail later, but the
intuitive idea is simple. In a dependent function space represented
by x:A->B,
the range type, B, is indexed by the domain type, A.
This is exactly like the
indexed product of a family of sets in set theory,
which is usually written as
(see [Bourbaki 68]). In the
dependent product represented by
x:A#B, the type of the second member of a pair can depend
on the value of the first. This is exactly the indexed disjoint sum of set
theory, which is usually written as
(see [Bourbaki 68]).
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 a is equal to b in type A. A special case of this is a = a in A, written also as a in A. These types embody the propositions--as--types principle discovered by H. B. Curry [Curry, Feys, & Craig 58], W. Howard [Howard 80], N. G. deBruijn [deBruijn 80] and H. Lauchli [Lauchli 70] and used in AUTOMATH [deBruijn 80,Jutting 79] . This principle is also central to P. Martin-Löf 's Intuitionistic type theories [Martin-Löf 82,Martin-Löf 73].
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.