next up previous contents index
Next: Components of the Up: Overview Previous: Motivations

The Nuprl Logical Language

  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. gif 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.

next up previous contents index
Next: Components of the Up: Overview Previous: Motivations

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