...Logic,
is version ``nu'' of our Proof  Refinement Logics. Earlier versions were ``micro'' and ``lambda'' [ Staff 83].
...space.
In the discussion which follows we will use typewriter font to signify actual Nuprl text and mathematical font for metavariables.
...[#ML##1#].
This is one result of a joint Cornell/Edinburgh study of programming logics and automated reasoning begun in 1981-82 and continuing with joint studies of type theory and polymorphism.
...type.''
Actually 97#97 reads as ``A is a type in universe 98#98.'' We discuss universes later.
...expression.
In full Nuprl the distinction between types and other objects is dropped.
...devices.
In Nuprl the goal 117#117 would be expressed initially as 118#118. A rule of introduction would then create the context 119#119.
...true.
A better term to use here might be the token ``yes'', which can be thought of as a summary of the proof. The term axiom suggests that the facts are somehow basic or atomic, but in fact they may require considerable work to prove.
...h.
In chapter 12 we introduce a concept of partial function that will allow us to define 346#346 such that 347#347 using an unbounded search. The search is guaranteed to terminate because of the information about f.
...semantics.
Section gif, page gif.
...inhabited.
Recall that the term (a = b in A) is a type whenever 416#416 and 417#417 and is inhabited just when 418#418. As a special case the term (a in A), which is shorthand for (a = a in A), is a type and is inhabited just when 419#419.
...windows
The windows are part of Nuprl and are not part of the window mechanism that may come with the machine on which Nuprl is implemented.
...system.
Other commands needed for proving theorems, evaluating terms, etc., will be discussed in later chapters.
...number.
The keyword scroll can be abbreviated by scr.
...follows.
The keyword create can be abbreviated by cr.
...name.
The keyword view can be abbreviated by v.
...#afterthm#2189>.
The new window is dependent on the first window, so the first window cannot be deleted until the text editor window is closed. The first window can, however, be moved off the screen by using the window--moving commands. Thus windows can be temporarily hidden.
...turnstile,
The notation >> is used instead of the more usual turnstile  437#437 since the former is available on most terminals.
...clicked.
Actually one can select the endpoints in either order.
....
One must not be in mouse mode while doing this.
...are
Other type constructors are being actively investigated. Some of these will be discussed in chapter 12.
...assumptions.''
Although >> must be present in every theorem, the system does not generate it because we want to allow the possibility of stating theorems with hypotheses, theorems such as x in int >> x+1 in int.
...void,
This is not a mathematical fact but a fact about Nuprl , so we would not expect to be able to prove in Nuprl a theorem of the form ``if A is an atomic type, then A = atom or A = void''.
....
The notation 461#461 is used in general discussion about the logic of Nuprl , whereas the notation Ui is used in discussing text used by Nuprl .
...proofs.
The proofs we are referring to in this discussion are not formal Nuprl proofs but abstract proofs.
...explicitly.
Every object can be constructed in two ways, either explicitly as in the example above or implicitly. Every proof builds an object implicitly. We will see in chapter 4 how to prove implicitly that the integers are an object in 468#468.
...#cldefs#2462>
It is important to enclose the right side of the definition in parentheses to guarantee proper precedence and scope. Also, it is important not to include a carriage return in the definition. The carriage return will sometimes be read as a bad character when parsing the right side, but it will not be visible on the screen.
...not.
We will see other definitions later which will take account of the structure of A.
...``or''.
The usual sign for classical or is 498#498, which abbreviates the Latin vel, meaning or. We have chosen not to use the word ``or'' at all among the logical operators because it has so many meanings in natural language.
...definition.
If the symbol < is being used in a definition to mean ``less than'' then it must be preceded by a backslash; otherwise, the system will try to interpret it as the start of a new parameter.
...definition:
The space after the ``514#514'' in the definition is to prevent the parser from thinking that the following < is being quoted.
...of
The definitions of the logical connectives, which were presented in the preceding chapter, are used here.
...mouse.
In general, any action involving the cursor and SEL key can also can be done using the mouse pointer and a left--click.
...type
Recall that we think of the proof tree as lying on its side.
....
It might seem natural to be more general and say that P and Q belong to any 549#549 whatsoever. This is something that we will be able to do in Nuprl

shortly, but we do not want to discuss such matters at this point.
...them.
Soon the system will allow the user to suppress the display of any hypotheses he is not interested in.
...evaluate
Evaluation in Nuprl will be discussed in the next chapter.
...term
A closed term is a term containing no free variables.
...redex.
This corresponds to head  reductions, normal --order evaluation or call --by--name parameter passing semantics.
...strategy.
One might complain that for certain terms this strategy would cause more work than necessary to be performed. For instance, consider the term (587#587 x.(x+x))(t), where t is very expensive to evaluate. Under the strategy described above, the value of t would be computed twice. As the language we are dealing with is functional we know that this is unnecessary, and under the actual implementation of the evaluator it would in fact be evaluated only once. In general, for any substitution 588#588 in the rules above, 589#589 will be evaluated at most once and will be evaluated only if there is a free occurrence of x in t.
...term.
The evaluator will try to reduce this term and in doing so will run until something intervenes, such as exhausting available memory.
...proof.
A tactic may fail to produce any proof at all, but it will not produce an invalid proof.
...}
If the cursor is within an edit window COMMAND must be pressed to get the `` P>'' prompt.
...objects.
Note: This has not been fully implemented.
...below.
Note that if the command window is hidden from view, one can enter mouse mode unwittingly. If this happens it will appear as though is not responding to any input except for the arrow keys.
...relation:
A note for experienced 638#638 users: no backslashes are required in this def.
...return.
Carriage returns are significant only as delimiters.
...text.
Unlike, for example, the Unix program nroff does not strip off backslashes when evaluating macros. They are stripped off only when text is actually parsed.
...T.
There is a similarity between a type and Bishop's notion of set. Bishop [Bishop 67] says that to give a set, one gives a way to construct its members and gives an equivalence relation, called the equality on that set, on the members.
...variables.
An identifier is any string of letters, digits, underscores or at--signs that starts with a letter. The only identifiers which cannot be used for variables are term_of and those which serve as operator names, such as int or spread.
...x:A.
In the formation of these as members of 766#766, B must be 767#767--functional in x:A.
...constructor.
modulo the difference between A#B and x:A#B, etc.
...(x:A#B).
If the reader finds this a bit difficult to follow, perhaps it would help to consider first the case in which x is not free in B and z is not free in T and then the more general cases afterward.
...integers.
This is defined by primitive recursion with 0 as the base case and an induction step for each direction out (positive and negative). Of course, in a higher--order system such as

, where functions can take functions as arguments and have functions as values, one can define by primitive recursion functions in int->int which are not primitive recursive.
...true.
If we were to give a similar semantic account of the judgements of [Martin-Löf 82], the plainest difference between the truth conditions for those judgements and judgements would be that the truth of the former requires type--functionality of each assumption in all its variables.
...inhabited.
Recall that the term (a = b in A) is a type whenever 886#886 and 887#887 and is inhabited just when 888#888. As a special case, the term (a in A) is a type and is inhabited just when 889#889.
...system.
It turns out that these predicates will hold only for closed terms.
...theorem.
This rule introduces very strong interproof dependencies. A proof using this rule depends not only on C but also on the way C is proved.
...variable.
The system actually uses sequences of asterisks rather than Greek letters.
...operators
The notation for the logical ``or'' is or and for ``and'' is &.
...is
This is a specialization of the LCF [Gordon, Milner, & Wadsworth 79] concept of tactic in that both goal and event are taken as partial proofs.
...substitution,
This is usually how substitution takes place throughout the Nuprl system.
...subgoal.
For example, doing intro's on a universally quantified formula generates as many subgoals of this form as there are quantified variables.
...nontrivial.
Proving that a type of the form t in T is well-formed, for instance, requires proving that t is a member of T, and this can be a Nuprl \ statement that a program meets its specifications.
...principle.
This principle states that any function mapping a finite set into a smaller finite set must map some pair of elements in the domain to the same element in the codomain.
...forms.
This will ensure that the definitions of relations 2041#2041 and 2042#2042 are sensible. A more liberal (and complex) restriction is given in [Constable & Mendler 85].
...refs.
See chapter 7 for more on the eval command.
...functions.
The variable _y_ contains underscores because we want a name unlikely to appear in the surrounding text.

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