Skip to main content
PRL Project

The Book

Implementing Mathematics with The Nuprl Proof Development System

See title page for important information about this reference

next up previous contents
Next: Bibliography Up: doc Previous: Mathematics Libraries   Contents

Recursive Definition

For anyone doing mathematics or programming, recursive definition needs no motivation; its expressiveness, elegance and computational efficiency motivate us to include forms of it in the Nuprl logic. Current work on extending the logic involves three type constructors: rec, the inductive type constructor, permitting inductive data types and predicates; inf, the lazy type constructor, permitting infinite objects; and $\sim$, the partial function space constructor, permitting recursively defined partial functions. This chapter gives the extensions to the system necessary for inductive types and for partial function types; for detailed presentations of these two types see [Constable & Mendler 85].

Inductive Types

As an introduction to the rec types, consider the inductive type of integer trees, defined informally as

\begin{displaymath} let\: z\: be\: int \mid (z \char93 z). \end{displaymath}

In the language of rec types this type may be defined as 
     rec(z. int | z#z).
Its elements include
inl 2,
inr <inl 3,inl 5> and
inr <inr <inl 7,inl 11>,inl 13>.
An inductive type may also be parameterized; generalizing the above definition of binary integer trees to general binary trees over a specified type, the example rephrased as

\begin{displaymath} let\: z(x)\: be\: defined\: as\: x \mid (z(x) \char93 z(x));\: consider\: z(int) \end{displaymath}

is denoted 
     rec(z,x. x | z(x)#z(x); int),
and the predicate function dom,
$ dom(x) = \left\{ \begin{array}{ll} true & {\rm if\ \ } f(x)=0 \\ dom(x+1)& {\rm if\ \ } f(x)\not=0 \\ \end{array} \right., %note the . must be there. $
asserting $f$ has a root $\geq x$ is denoted 
     \x. rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); x).
The elim form, rec_ind, is analogous to the list_ind and integer ind forms. If t is of type rec(z. int | z#z) then the following term computes the sum of the values at t's leaves. 
     rec_ind(t;  sum,x.
       decide(x;
         leaf. leaf;
         pair. spread(pair; left_son,right_son.
                 sum(left_son)+sum(right_son))))
The simpler rec($z$.$T$) form is not formally part of the extension since it can be mimicked by rec($z$,$x$. $T$$[$$z$(0)$/$$z$$]$;0), for example, so consider any rec($z$.$T$) term in what follows to be just an abbreviation. Inductive types can also be defined in a mutually recursive fashion, but we will not pursue that possibility here.

Expressiveness and Elegance

The transfinite W-type of well-founded trees, $({\bf W}x\in A)B$, used to represent Brouwer ordinals is inexpressible in the Nuprl logic discussed in the earlier chapters but can be represented in the logic extended by rec types as rec(w. $x$:$A$#($B$->w)). The data type for programs given in chapter 11, 
     d:N#ind(d; x,y.void; void; x,T. Atomic_Stmt | (T#T) |
                                     (expr#T) | expr#T#T),
can be written more elegantly as 
     rec(T. Atomic_Stmt | (T#T) | (expr#T) | expr#T#T).
The list type constructor is now redundant because $A$ list can be expressed as rec(l. NIL | $A$#l).

Details of the Extension

The following modifications will add inductive types to Nuprl.

Computation System Modification

Add terms
rec($z$,$x$.$T$;$a$)
rec_ind($r$; $v$,$u$.$g$)
where $u,v,x$ and $z$ range over variables, $a,g,r$ and $T$ range over terms, and $T$ is restricted as follows:
No instance of $z$ bound by rec may occur in the domain type of a function space, in the argument of a function application or in the principal argument(s) of the remaining elimination forms.12.1
Thus (A#$z$)->B or f(inr $z$) or spread($z$; a,b.a->int) cannot be subexpressions of $T$. When closed, rec terms are canonical and rec_ind terms are noncanonical. These noncanonical terms are redices with principal argument $r$ and contracta
$g[r,\;$\$u$.rec_ind($u$; $v$,$u$.$g$)$/u,\;v]$,
when $r$ is canonical. The rules for binding variables are:
  • In rec($z$,$x$.$T$;$a$)the $z$ and $x$ in front of the dot and any free occurrences of $z$ or $x$ in $T$ become bound.

  • In rec_ind($r$; $v$,$u$.$g$) the $u$ and $v$ in front of the dot and any free occurrences of $u$ or $v$ in $g$ become bound.

Inductive Type Proof Rules

The proof rules will ensure that the following two assertions hold.
rec($x$,$y$.$A$;$b$) type $\Leftrightarrow$
$\exists B,k.\; b \in B$ & $x$:($B$->U$k$)->$y$:$B$->$A$ type



$t \in\; $rec($x$,$y$.$A$;$b$) $\Leftrightarrow$ rec($x$,$y$.$A$;$b$) type
& $t \in A[$\$y$.rec($x$,$y$.$A$;$y$)$,\;b/x,\;y]$
That is, rec($x$,$y$.$A$;$b$) is a type exactly when there is a type $B$ and universe level $k$ such that $b$ is in $B$ and for all $x$ which, when instantiated with a value from $B$, yield a type at universe $k$, and $y$ of type $b$, $A$ (with $x$ and $y$ potentially free) is a type. Also, $t$ is of type rec($x$,$y$.$A$;$b$) exactly when rec($x$,$y$.$A$;$b$) is a type and $t$ is a member of the ``unwinding'' of the recursive type.

Formation

A universe intro rule such as ``» ${\tt U}{i}$ by intro rec'' cannot be phrased easily in the refinement logic style because of the syntactic restriction on $T$ in the extracted term rec($z$,$x$.$T$;$a$). One could give an approximate solution (as was done for set elim), but here we settle for no rule at all, thereby forcing the use of the explicit intro rule. 

1.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » rec($z$,$x$.$T$;$a$) in ${\tt U}{i}$ 				 by intro using $A$

 $z$:$A$->${\tt U}{i}$,$x$:$A$ » $T$ in ${\tt U}{i}$ 

 » $a$ in $A$

Intro 


2.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » rec($z$,$x$.$T$;$a$)				by intro at ${\tt U}{i}$		$[EXT  r]$ 

 » $T[$\$x$.rec($z$,$x$.$T$;$x$)$,\;a/z,\;x]$						$[EXT  r]$

 » rec($z$,$x$.$T$;$a$) in ${\tt U}{i}$


3.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » $r$ in rec($z$,$x$.$T$;$a$)				 by intro at ${\tt U}{i}$

 » $r$ in $T[$\$x$.rec($z$,$x$.$T$;$x$)$,\;a/z,\;x]$

 » rec($z$,$x$.$T$;$a$) in ${\tt U}{i}$


4.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » rec_ind($p$; $h$,$p_1$.$g$) in $G[p/p_2]$

    by intro $[$over $p_2.G]$ using $y$:$A$#rec($z$,$x$.$T$;$y$) new $Z[,p_2]$

 $p_2$:($y$:$A$#$Z$($y$))->($p_2$ in $y$:$A$#rec($z$,$x$.$T$;$y$)),

 $h$:$p_2$:($y$:$A$#$Z$($y$))->$G$,

 $p_1$:$y$:$A$#($T[Z,y/z,x]$)» $g$ in $G[p_1/p_2]$

 » $p$ in $y$:$A$#rec($z$,$x$.$T$;$y$)

Elim 


5.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$,$r$:rec($z$,$x$.$T$;$a$),$H^{\prime}$ » $G$ by elim $r$		$[EXT  t]$ 

 $H$,$r$:$T[$\$x$.rec($z$,$x$.$T$;$x$)$,\;a/z,\;x]$,$H^{\prime}$ » $G$ $[EXT  t]$



6.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$,$r$:rec($z$,$x$.$T$;$a$)» $G$$[$<$a$,$r$>$/$$p$$]$				$[EXT  $rec_ind(<$a$,$r$>;$p,h.g$)$]$

    by elim $r$ over $y$:$A$#rec($z$,$x$.$T$;$y$)SPAN CLASS="MATH">$[$using $p$.$G]$ new $h,Z[,p]$

 $p$:($y$:$A$#$Z$($y$))->($p$ in $y$:$A$#rec($z$,$x$.$T$;$y$)),

 $h$:$p$:($y$:$A$#$Z$($y$))->$G$,

 $p$:$y$:$A$#($T[Z,y/z,x]$) » $G$						$[EXT  g]$ 

 » $a$ in $A$

Computation 


7.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » rec_ind($r$; $h$,$r_1$.$g$)=$t$ in $G$				 by reduce 

 »$g[r,\;$\$r_1$.rec_ind($r_1$;$h$,$r_1$.$g$)$/r_1,\;h]$=$t$ in $G$

Example Proof

The $dom$ predicate defined earlier in the chapter is used here to demonstrate induction. Given the definitions 
     ~<T>== (<T>) -> void
     some <v>:<A>.<P>== <v>:(<A>)#(<P>)
     N== {n:int| ~(n<0)}
     true== (0 in int)
     D(<x>)== rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); <x>)
figure 12.1 sketches the proof of 
     f:N->N, r:D(0) >> some y:N. f(y)=0.
Although D(0) is inhabited only by axiom, evaluating the extracted term produces a root.
Figure 12.1: A Sample Proof Using Recursion
\begin{figure}\hrule \begin{verbatim}1. f:N->N 2. r:D(0) >> some y:N. f(y)=0 i... ...f(y)=0 in N by elim h on <y+1,ax>\end{verbatim} \vspace{2pt} \hrule \end{figure}

Partial Function Types

We handle partial functions by viewing them as total functions over their domains of convergence. To do so we introduce dom terms, which capture the notion of a domain of convergence. Thus, for a partial function application to be sensible one must prove that the domain of convergence predicate is true for the argument, i.e., that the argument is in the domain of convergence of the function. The introduction of dom terms introduces additional proof obligations into the rules for reasoning about partial functions.

As an example, the partial function $\mu$ producing the smallest root $\geq x$ of $f$,

$ \mu(x) = \left\{ \begin{array}{ll} x & {\rm if } f(x)=0 \\ \mu(x+1)& {\rm if } f(x)\not=0 \\ \end{array} \right. $
has a domain of convergence defined by the predicate $\mu'$ as follows.
$ \mu'(x) = \left\{ \begin{array}{ll} {\rm true} & {\rm if } f(x)=0 \\ \mu'(x+1)& {\rm if } f(x)\not=0 \\ \end{array} \right. $
Thus $\mu$ is a total function in $\{x \in {\sl nat} \vert \mu'(x)\} \rightarrow {\sl nat}$.

In our notation the type of partial functions from $A$ to $B$ is $A$$\sim$$B$, the application of partial function f to a is written f[a], recursive functions are expressed as terms of the form fix($f$,$x$.$b$), so function $\mu$ of the preceding example is 

     MU == fix(mu,x. int_eq(f(x); 0; x; mu[x+1])),
and $\mu'$ is dom(MU) , an elim form which turns out to have value 
     \x.rec(mu',x. int_eq(f(x); 0; true; mu(x+1)); MU; x).
The domain predicate is derived later; in general, if $f\in$ $A$$\sim$$B$ then \$x.f$[$x$] $in$ {$x$:$A$|dom($f$)($x$)}->$B$.

As a second example, the ``91'' function,

$ F(x) = \left\{ \begin{array}{ll} x-10 & {\rm if } x>100 \\ F(F(x+11))& {\rm if } x\leq 100\\ \end{array} \right. $
has domain
$ F'(x) = \left\{ \begin{array}{ll} true & {\rm if } x>100 \\ F'(x+11)\; and\; F'(F(x+11))& {\rm if } x\leq 100\\ \end{array} \right. $
In our notation $F$ and $F'$ are 
     91== fix(F,x. less(100; x; x-10; F[F[x+11]])

     \x.rec(F',x.
        less(100; x; true; c:F'(x+11)#F'(F[x+11]); 91; x)
Notice that the rec forms defined in the preceding section must be extended to include the simultaneous definition of the recursive function. The new proof rules for these rec terms are only slight variants of the given rules, so they are not listed here.

Details of the Extension

Computation System Modification

The domain predicate captures a call-by-value order of computation, so the entire computation system must be adjusted slightly to reflect this. In particular, computing the value of a function application (total or partial) dictates that function and argument are normalized before beta reduction, both subterms in pairs are normalized, and for injections into disjoint sums the subterm is normalized. In this extension direct computation rules are not present.

To add $\sim$ types to the logic we add terms

fix($f$,$x$.$b$)
$A$$\sim$$B$
dom($t$)
$t$[$a$]
where $f$ and $x$ range over variables and $a,b,t,A$ and $B$ range over terms. When closed, the first two kinds of terms are canonical, and the last two are noncanonical.

Let $\varphi$ stand for fix($f$,$x$.$b$) henceforth. Each closed term $\varphi$[$a$] is a redex with contractum $b[\varphi,\; a/f,\;x]$, and each closed term dom($\varphi$) is a redex with contractum

\$x$.rec($f'$,$x$. ${\cal E}{}[\![$b$]\!]$;$\varphi$ ;$x$),
where ${\cal E}$ is defined below. The rule for binding variables is as follows.
  • In fix($f$,$x$.$b$), the $f$ and $x$ in front of the dot and any free occurrences of $f$ or $x$ in $b$ become bound.

Domain Predicate

We define ${\cal E}$, a syntactic transformation on terms, as follows.
  • ${\cal E}{}[\![$$f$[$t$]$]\!]$ = ${\cal E}{}[\![$$t$$]\!]$#$f$'($t$), if $f$ had been bound by the the first variable in a surrounding fix term. Recall that $f'$ is the characteristic function for the domain of $f$.

  • ${\cal E}{}[\![$$t$[$a$]$]\!]$ = ${\cal E}{}[\![$$t$$]\!]$# ${\cal E}{}[\![$$a$$]\!]$#dom($t$)($a$) if the first clause does not apply.

  • ${\cal E}{}[\![$$t$($a$)$]\!]$ = ${\cal E}{}[\![$$t$$]\!]$# ${\cal E}{}[\![$$a$$]\!]$

  • ${\cal E}{}[\![$spread($e$; $u$,$v$.$t$)$]\!]$ = ${\cal E}{}[\![$$e$$]\!]$#spread($e$; $u$,$v$. ${\cal E}{}[\![$$t$$]\!]$), and similarly for the other elimination forms.

  • ${\cal E}{}[\![$inl($a$)$]\!]$ = ${\cal E}{}[\![$$a$$]\!]$

  • ${\cal E}{}[\![$<$a$,$b$>$]\!]$ = ${\cal E}{}[\![$$a$$]\!]$# ${\cal E}{}[\![$$b$$]\!]$

  • ${\cal E}{}[\![$$t$$]\!]$ = true, for the remaining terms.
The #'s used here are dependent products and therefore require a left-to-right evaluation order in the predicate.

Partial Function Type Proof Rules

In the following ${\cal E}'$ is just ${\cal E}$ with the first clause of the definition omitted and $\varphi'$ is fix($f$,$x$.$b'$).

Formation 


8.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » $A$$\sim$$B$ in ${\tt U}{i}$ 				 by intro

 » $A$ in ${\tt U}{i}$ 

 » $B$ in ${\tt U}{i}$

Intro 


9.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » $\varphi$ in $A$$\sim$$B$				by intro at ${\tt U}{i}$

 » $A$$\sim$$B$ in ${\tt U}{i}$

 $f$:$A$$\sim$$B$, $x$:$A$ » ${\cal E}'{}[\![$$b$$]\!]$ in ${\tt U}{i}$

 $f$:$A$$\sim$$B$, $x$:$A$, ${\cal E}'{}[\![$$b$$]\!]$ » $b$ in $B$


10.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » $\varphi$ = $\varphi'$ in $A$$\sim$$B$				by intro at ${\tt U}{i}$

 » $\varphi$ in $A$$\sim$$B$

 » $\varphi'$ in $A$$\sim$$B$

 » {$x$:$A$ | dom($\varphi$)($x$)} ={$x$:$A$ | dom($\varphi'$)($x$)}  in ${\tt U}{i}$

 $x$:{$x$:$A$ | dom($\varphi'$)($x$)}» $\varphi$[$x$] = $\varphi'$[$x$]  in $B$


11.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » $g$[$a$] in $B$ by intro using $A$$\sim$$B$

 » $g$ in $A$$\sim$$B$

 » $a$ in {$x$:$A$ | dom($g$)($x$)}


12.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » dom($g$) in $A$->${\tt U}{i}$ 				by intro using $A$$\sim$$B$

 » $g$ in $A$$\sim$$B$

 » $A$$\sim$$B$ in ${\tt U}{i}$

Elim 


13.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$,$g$:$A$$\sim$$B$,$H^{\prime}$ » $G$ by elim $g$ on $a$ new $y$

 $H$,$g$:$A$$\sim$$B$,$H^{\prime}$ » $a$ in {$x$:$A$ | dom($g$)($x$)}

 $H$,$g$:$A$$\sim$$B$,$H^{\prime}$, $y$:$B$; $y$=$g$[$a$] in $B$ » $G$

Computation 


14.$H$,$r$:ind($z$,$x$.$T$;$a$) » $G$$[$$a$$/$$g$$]$ggggggby ind $r$ over $A$ ${\tt U}{i}$ [$EXT$ foobar][$EXT$ foobar]$H$ » $\varphi$[$a$] = $t$ in $B$ by reduce 

 » $b[\varphi,a/\;f,x]$ = $t$ in $B$

General Notes

All universe levels must be strictly positive. Unless otherwise stated the tokens `nil` and `NIL` may be used as identifiers to indicate that no identifier should label the new hypothesis.


Refinement Functions

refine: rule $\rightarrow$ tactic.
This function refines a proof according to a given rule.

refine_using_prl_rule: tok $\rightarrow$ tactic.
This function parses the token as a rule in the context of the given proof. The proof is then refined via this rule.

Rule Constructors

See chapter 8 for a description of the rule constructors.


Rule Destructors

rule_kind: rule $\rightarrow$ tok.
Returns the kind of the rule. Note that at present this is in the internal form of the rule name. There are also predicates of the form is_universe_intro_void that correctly translate from the internal names of rules and the names of the rule constructors (as listed above with ``is_'' prepended). There are also destructors for each of the rules that correspond to the constructor. The names are of the form ``destruct_universe_intro_void''.

Term Destructors

term_kind: term -> tok.
Returns the kind of the term. Possible results are: UNIVERSE, VOID, ANY, ATOM, TOKEN, INT, NATURAL-NUMBER, MINUS, ADDITION, SUBTRACTION, MULTIPLICATION, DIVISION, MODULO, INTEGER-INDUCTION, LIST, NIL, CONS, LIST-INDUCTION, UNION, INL, INR, DECIDE, PRODUCT, PAIR, SPREAD, FUNCTION, LAMBDA, APPLY, QUOTIENT, SET, EQUAL, AXIOM, VAR, BOUND-ID, TERM-OF-THEOREM, ATOMEQ, INTEQ, INTLESS.

There are corresponding predicates such as is_universe_term and corresponding constructors such as make_function_term (which has type tok $\rightarrow$ term $\rightarrow$ term $\rightarrow$ term).

destruct_universe: term $\rightarrow$ int.
The integer is the universe level.

destruct_any: term $\rightarrow$ term.

destruct_token: term $\rightarrow$ tok.

destruct_natural_number: term $\rightarrow$ int.

destruct_minus: term $\rightarrow$ term.

destruct_addition: term $\rightarrow$ (term # term).

The results are the left and right terms.

destruct_subtraction: term $\rightarrow$ (term # term).

destruct_multiplication: term $\rightarrow$ (term # term).

destruct_division: term $\rightarrow$ (term # term).

destruct_modulo: term $\rightarrow$ (term # term).

destruct_integer_induction: term $\rightarrow$ (term # term # term # term).

The results are the value, down term, base term and up term.

destruct_list: term $\rightarrow$ term.
Returns the type of the list.

destruct_cons: term $\rightarrow$ (term # term).
Returns the head and tail.

destruct_list_induction: term $\rightarrow$ (term # term # term).

Returns the value, base term and up term.

destruct_union: term $\rightarrow$ (term # term).

Results in the left and right types.

destruct_inl: term $\rightarrow$ term.

destruct_inr: term $\rightarrow$ term.

destruct_decide: term $\rightarrow$ (term # term # term).

The result is the value, the left term and the right term.

destruct_product: term $\rightarrow$ (tok # term # term).

The result is the bound identifier, the left term and the right term.

destruct_pair: term $\rightarrow$ (term # term).

Returns the left term and the right term.

destruct_spread: term $\rightarrow$ (term # term).

Returns the value and the term.

destruct_function: term $\rightarrow$ (tok # (term # term)).

The result is the bound identifier, the left term and the right term.

destruct_lambda: term $\rightarrow$ (tok # term).

Returns the bound identifier and the term.

destruct_apply: term $\rightarrow$ (term # term).

Returns the function and the argument.

destruct_quotient: term $\rightarrow$ (tok # (tok # (term # term))).

Returns the two bound identifiers, the left type and the right type.

destruct_set: term $\rightarrow$ (tok # (term # term)).

Returns the bound identifier, the left type and the right type.

destruct_var: term $\rightarrow$ tok.

destruct_equal: term $\rightarrow$ ((term list) # term).

Returns a list of the equal terms and the type of the equality.

destruct_less: term $\rightarrow$ (term # term)).

Returns the left term and the right term.

destruct_bound_id: term $\rightarrow$ ((tok list) # term).

Returns a list of the bound identifiers and the type.

destruct_term_of_theorem: term $\rightarrow$ tok.

Returns the name of the theorem.

destruct_atomeq: term $\rightarrow$ (term # (term # (term # term))).

Returns the left term, right term, if term and else term.

destruct_inteq: term $\rightarrow$ (term # (term # (term # term))).

Returns the left term, right term, if term and else term.

destruct_intless: term $\rightarrow$ (term # (term # (term # term))).

Returns the left term, right term, if term and else term.

destruct_tagged: term $\rightarrow$ (int # term).

The integer returned is zero if the tag is *.

For each term type there is a corresponding constructor that is the curried inverse to the destructor given above. For example,

make_inteq_term: term $\rightarrow$ term $\rightarrow$ term $\rightarrow$ term $\rightarrow$ term.


Auto-Tactic

set_auto_tactic: tok $\rightarrow$ void.

Set auto-tactic to be the ML expression represented by the token.

show_auto_tactic: void $\rightarrow$ tok.

Displays the current setting of the auto-tactic.

Miscellaneous Functions

mm: tactic.

Prints a reasonable representation of the proof into the snapshot file without modifying the proof. It is intended to be used as a transfomation tactic.

term_to_tok: term $\rightarrow$ tok.
Converts a term into a token representation.

print_term: term $\rightarrow$ void.
Displays a term.

rule_to_tok: rule $\rightarrow$ tok.

print_rule: rule $\rightarrow$ void.
Displays a representation of a rule.

declaration_to_tok: declaration $\rightarrow$ tok.

print_declaration: declaration $\rightarrow$ void.
Displays a declaration.

main_goal_of_theorem: tok $\rightarrow$ term.

Returns the term which is the conclusion of the top node of the named theorem.

extracted_term_of_theorem: tok $\rightarrow$ term.

Returns the term extracted from the named theorem.

map_on_subterms: (term $\rightarrow$ term) $\rightarrow$ term $\rightarrow$ term.

Replaces each immediate subterm of the term argument by the result of applying the function argument to it.

free_vars: term $\rightarrow$ term list.

remove_illegal_tags: term $\rightarrow$ term.
Takes a term and removes the smallest number of tags needed to make the term have a tagging which is legal with respect to the direct computation rules. (See appendix C for a definition of legal tagging.)

do_computations: term $\rightarrow$ term.

Returns the result of performing the computations indicated by the tags in the argument. (See appendix C for a description of the direct computation rules).

no_extraction_compute: term $\rightarrow$ term.

Computes (in the sense of the direct computation rules) the term as far as possible, without treating term_of terms as redices; these are treated in the same way as variables.

loadt: tok $\rightarrow$ void.

Loads the named file into the ML environment. The name given must be the name, or path name, of the file, with the extension (e.g., ``.ml'') removed; the appropriate version (binary, Lisp or ML source) will be loaded. Note that ML written in files can only mention other ML objects; in particular, Nuprl definitions cannot be instantiated, and the single quote cannot be used to form Nuprl terms.

compilet: tok $\rightarrow$ void.

Compiles the named file, putting the Lisp and binary code files in the same directory as the named file. The argument should be the full path name for the file with the extension removed.

This appendix discusses the differences in the Lambda-prl and Nuprl logics and user interfaces and ways to simulate Lambda-prl constructs in Nuprl.

Differences in the Logic

The Nuprl proof rules naturally extend the Lambda-prl proof rules and as such are organized along roughly the same lines. However, the logic of Nuprl is considerably more powerful than that of Lambda-prl, and the rules are correspondingly more complex. The Nuprl rules are classified into three broad categories: introduction, elimination and equality; the equality rules are further broken down into computation rules and equality rules for each of the term constructors. The introduction and elimination rules are analogous to those in Lambda-prl; the equality rules are a new feature of the Nuprl logic.

The differences between the logic of Lambda-prl and Nuprl can be briefly summarized as follows:

  • Strengthening the type structure.
    The Lambda-prl logic is based on two primitive types, integers and lists of integers. The Nuprl logic extends this to a much richer type structure.
  • Identifying propositions with types.
    In Lambda-prl propositions were specific syntactic entities. In Nuprl propositions are simply certain kinds of types. Demonstrating the truth of a proposition amounts to presenting an object of that type so that a proposition is treated as the type of its justifications.
  • Well-formedness.
    In Lambda-prl well-formedness of propositions was checked by the system. The richness of the Nuprl type structure, however, precludes the possibility of automatically checking whether or not an expression is a type. By the identification of propositions with types this property extends to propositions as well.
  • Explicit treatment of equality and simplification.
    In Lambda-prl equality and simplification were by and large taken care of by the arith rule, which handled simple arithmetic, substitutivity of equality and simplification of terms (such as hd[1,2]=1). The Nuprl logic, however, is sufficiently rich that such a treatment is no longer possible. Consequently there are rules for equality of terms and for computation.
We now discuss the effect of these aspects of the Nuprl logic on the formulation of the rules.

Introduction Rules

For each of the type constructors of the theory there are two introduction rules, one of the form $H$ » $A$ and one of the form $H$ » $a$ in $A$. For instance, we have

\(H\) » \(A\)|\(B\) by intro at \(\mbox{${\tt U}{i}$}\) right
\(H\) » \(A\)
\(H\)» \(B\) in \(\mbox{${\tt U}{i}$}\)
and
\(H\) » inl(\(a\)) in \(A\)|\(B\) by intro at \(\mbox{${\tt U}{i}$}\)
\(H\) » \(a\) in \(A\)
\(H\) » \(B\) in \(\mbox{${\tt U}{i}$}\)
These rules have essentially the same content to the extent that the judgements are completely reflected in the equality types, but the former leaves the inhabiting object, inl($a$), suppressed whereas the latter treats it explicitly. In the first rule the extracted object is inl($a$), while in the latter it is the token axiom. Intuitively, the first of the two is useful when we are regarding $A$|$B$ as the proposition expressing the disjunction of $A$ and $B$; the latter is useful when we are thinking of $A$|$B$ as a data type, in which case the right-hand side above expresses the proposition that inl($a$) is a member of the type $A$|$B$.

Since types, and hence propositions, are those terms which can be shown to inhabit a universe type, this duality extends to the type (proposition) formation rules -- they are simply the introduction rules for the universe types. Note, however, that the rules are organized in such a way that one does not need to construct a type explicitly before showing it to be inhabited. Each rule is sufficient to show not only that a type is inhabited but also that it is in fact a type. In most cases we go to no special trouble to achieve this, but certain rules contain subgoals whose only purpose is to assist in demonstrating that the consequent is a type. For instance, the second subgoal in the rules above exists solely to ensure that $A$|$B$ is a type. That $A$ is a type is ensured by the first subgoal; the second provides the additional information necessary to form the union type.

Elimination Rules

There is also a dual relationship between the elimination rules and an introduction rule for the corresponding elimination form. For instance, the union elimination rule has a goal of the form $H$ » $T$; the extracted code is a term of the form decide($z$;$u.a$;$v.b$). Correspondingly there is an introduction rule with a goal of the form $H$ » decide($e$;$u.a$;$v.b$) in $\mbox{$T[e/z]$}$. This rule states the general conditions under which we may introduce a decide. Notice that any decide introduced by an elimination rule will have a variable in the first argument position. However, the additional generality of the introduction is obtained at a price; it is not possible to produce the subgoals of the rule instance from the goal alone. Two parameters are needed: one to specify the union type, written using $A$|$B$, and one to specify the range type, written using $z.T$. This additional complexity is part of the price of the increased expressiveness of the Nuprl logic.

Equality and Simplification Rules

Another major difference between the Lambda-prl rules and the Nuprl rules is the treatment of equality and simplification. The logic of Lambda-prl is sufficiently simple that all equality reasoning can be lumped into a single rule. Similarly, simplification of terms is handled by a single rule. The two are combined, together with some elementary arithmetic reasoning, into a decision procedure called arith which handles nearly all of the low-level details of Lambda-prl proofs. However, the additional expressiveness of the Nuprl logic prevents such a simple solution. For each term constructor there is a rule of equality, for each elimination form there is a computation rule, and there is a general rule of substitution.

For instance, the equality rule for inl is as follows.

\(H\) » inl(\(a\)) = inl(\(b\)) in \(A\)|\(B\) by intro
\(H\) » \(a\) = \(b\) in \(A\)
\(H\) » \(B\) in \(\mbox{${\tt U}{i}$}\)
For decide there are two equality rules: the basic equality rule for the constructor and a computation rule. The goals are, respectively,
\(H\) » decide(\(e\);\(u.s\);\(v.t\)) = decide(\(e'\);\(u.s'\);\(v.t'\)) in \(T[e/z]\)
and
\(H\) » decide(inl(\(a\));\(u.s\);\(v.t\)) = \(s[a/u]\) in $T[\mbox{\tt inl(\(a\))}/z]$
Equations obtained with these rules can be used by the equality and substitution rules.

Differences in the User Interfaces

The Lambda-prl and Nuprl user interfaces are nearly identical, although there are two noticeable differences.

  • In Nuprl the eval command invokes an interactive evaluation facility, into which one enters terms and bindings to be evaluated. EVAL objects residing in the library may contain def refs. .1 In Lambda-prl the eval command has the form eval ${term}$, and ${term}$ may not contain definition references.

  • In Lambda-prl, identifiers can include the pound sign (``#'') in addition to the alphanumeric characters and the underscore (``_''). In Nuprl, the at sign (``@'') is used instead of the pound sign. Note that users are encouraged not to use at signs in their own identifiers, since the system implementers have reserved them for their own purposes.

Simulating Lambda-prl Constructs in Nuprl

Logical Operators

The logical operators are not part of Nuprl; they can be simulated by using DEF's described in chapter 3. We will use these simulated logical operators below in the examples.

Lists

The hd and tl built-in functions of Lambda-prl do not exist in Nuprl. They can be simulated with the following definitions. 

    hd(<a:list>)==list_ind(<a>; "?"; h,t,v.h)
    tl(<a:list>)==list_ind(<a>; nil; u,v,w.v)
Given these definitions, it is straightforward to prove in Nuprl that hd satisfies 
    >> All A:U1. All L:A list. hd(L) in A => ~(L=nil in A list)
and 
    >> All A:U1. All x:A. All L:A list. hd(x.L)=x in A

Once the two goals above are proved they can be used in other proofs as lemmas. Similar facts for tl are also easy to prove.

Primitive Recursive Functions

Since primitive recursive function objects are not available in Nuprl, they have to be simulated. Consider the primitive recursive function

\begin{displaymath} \begin{array}{lcl} F(0,y) & = & G(y) \\ F(n+1,y) & = & H(n,F(n,y),y) \end{array}\end{displaymath}

Shown below is a DEF that serves as a template for defining such functions. .2 

    (F such that F(0,y)=(<G:base>)(y),
                 F(n+1,y)=(<H:body>)(n,F(n,y),y)
    )
    ==
    \n.(\y.ind(n;
               u,v."?";
               (\_y_.(<G>)(_y_));
               u,v.(\_y_.(<H>)(u)(v(_y_))(_y_))
              )
              (y) 
       )

The DEF above could be used to define an exponentiation DEF in the following way. 

    <y:int>**<n:int>
    ==
    ((F such that F(0,y)=(\z.z)(y),
                  F(n+1,y)=(\a.\b.\c.(b*c))(n,F(n,y),y)
     )(<n>)
    )(<y>)

Extraction Terms

To use the extracted term E from a (complete) theorem T in another theorem, make E a DEF: 

         E==term_of(T).
The evaluation mechanism may be used to evaluate term_ of(T) and to bind its value to a variable.

This appendix gives a more precise description of the direct computation rules than the one given in chapter 8. It should probably be ignored by those who find the previous description adequate, for the details are rather complicated.

The direct computation rules allow one to modify a goal by directing the system to perform certain reduction steps within the conclusion or a hypothesis. The ``direct'' in ``direct computation'' refers to the fact that no well-formedness subgoals are entailed. The present form of these rules, involving ``tagged terms'' as described in chapter 8, was chosen to provide the user with a high degree of control over what reductions are performed. The tagged terms may be somewhat inconvenient at the rule-box level, but it is expected that the vast majority of uses of these rules will be by tactics.

First, we define what it means to compute a term for $n$ steps (for $n$ a nonnegative integer). To do this we define a function $compute_n$ on terms $t$. Roughly speaking, $compute_n(t)$ is the result of doing computation (as described in chapter 5) on $t$ until it can be done no further or until a total of $n$ reductions have been done, whichever comes first. The precise definition is as follows. If $t$ is not a term_of term and not a noncanonical term, or if $n$ is $0$, then $compute_n(t)$ is $t$. If $t$ is term_of($name$) then $compute_n(t)$ is $compute_{n-1} (t')$, where $t'$ is the term extracted from the theorem named $name$. If $t$ is a noncanonical term with one principal argument $e$ then replace $e$ in $t$ by $compute_n (e)$ to obtain $t'$, and let $k$ be the number of replacements of redices by contracta done by $compute_n (e)$. If $n>k$, and $t'$ is a redex, then $compute_n(t)$ is $compute_{n-k-1} (t'')$, where $t''$ is the contractum of $t'$. If t is noncanonical with two principal arguments (e.g., int_eq) then replace the leftmost one, $e$, with $compute_n (e)$ to obtain $t'$, and let $k$ be the number of reductions done by $compute_n (e)$. If $compute_n (e)$ is not a canonical term of the right type then $compute_n(t)$ is $t'$; otherwise, it is $compute_{n-k} (t')$, where $t'$ is treated as having one (the second) principal argument.

Having now defined $compute_n(t)$ we can define what it means to do the computations indicated by a tagging. If $T$ is a term with tags then the computed form of $T$ is obtained by successively replacing subterms of $T$ of the form [[$n$;$t$]] or [[*;$t$]], where $t$ has no tags in it, by $compute_n(t)$ or $compute_{\infty} (t)$, respectively, where $compute_{\infty}$ is defined in the obvious way.

It seems very plausible that one should be able to put tags anywhere in a term. Unfortunately, it has not yet been proved that this would be sound, so there is at present a rather complicated restriction, based on technical considerations, on the set of subterm occurrences that can legally be tagged. Let $T$ be a term and define a relation $\prec$ on subterm occurrences of $T$ by $u \prec v$ if and only if $u$ occurs properly within $v$. A $t \preceq T$ may be tagged if there are $u$ and $v$ with $t \preceq u \preceq v \preceq T$ such that:

  1. $v \prec r \preceq T$ $\Rightarrow$ r is a canonical term, and

  2. $u$ is free in $v$ (i.e., no free variables of $u$ are bound in $v$), and

  3. $t \prec r \preceq u$ $\Rightarrow$
    1. $r$ is a noncanonical term with $t$ occurring within the principal argument of $r$,
    2. $r$ is a spread, decide, less, int_eq, any or atom_eq term, or
    3. $r$ is ind($a$;$m$,$x$.$b$;$c$;$n$,$y$.$d$) such that $x$,$y$ do not occur free in $b$,$d$ respectively, or
    4. $r$ is list_ind($a$;$h$,$t$,$v$.$b$) and $v$ does not occur free in $b$.

For the purposes of the definition above, the notions of canonical and noncanonical are extended in the obvious way to terms with free variables.


Footnotes

... forms.12.1
This will ensure that the definitions of relations $T=T'$ and $t=t'\in\;T$ are sensible. A more liberal (and complex) restriction is given in [Constable & Mendler 85].
... refs. .1
See chapter 7 for more on the eval command.
... functions. .2
The variable _y_ contains underscores because we want a name unlikely to appear in the surrounding text.
next up previous contents
Next: Bibliography Up: Index Previous: Mathematics Libraries   Contents
PRL Home
Introduction
The Nuprl book
Origins of the PRL Project
Goals
Dynamics of the Project
Mathematical Expression in Nuprl
Cross Links to Math & CS Fields
Knowledge Base
Math Library
Publications
Projects
CRASH
Nuprl/FDL System
EventML Software
Seminar
People
Wiki
The Book
Lectures
Other Groups


Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library