Terms

The informal language we used in Naive Type Theory does not reveal any pattern to the notation. We see forms like $x\mapsto b$, f(a),   $A \rightarrow B$, $\forall x\!:\!A.B$, U_i consisting of infix operators, parenthesized arguments, prefix operators, subscripts, etc. We would like a regular pattern to the terms that is a basis for analyzing and manipulating them. A Lisp-like syntax, $(f \ a_1 \ldots a_n)$ might be adequate, but does not provide the flexibility we want for dealing with binding structure; Lisp only allows $(lambda (x_1 \ldots x_n) \,b)$ for binding. So the term structure in Nuprl has the form

$op(\bar{v}_1 . t_1; \ldots; \bar{v}_n . t_n)$

where op is an operator name, $\bar{v}_i$ is a list of binding variables governing the subterm t_i which is then scope. Every occurrence of a variable from $\bar{v}_i$ in t_i is called bound. The t_i are subterms.

For display purposes, if $\bar{v}_i$ is empty, we do not show it, and if n=0 we drop the parentheses. Here is a list of all the Nuprl terms we need

term display form                  

Syntactic variety comes from the display forms, written in the right column. These are like L^ATEXprint macros, but they are also used for input as well.

Syntactic Theory

To understand how to compute with terms, we first need a complete account of certain aspects of the syntax. The main idea we need is the notion of substitution of a term s for occurrences of a variable x in a term t, written

t[s/x].

We need a very precise definition of this concept. To get it we require the definition of $\alpha$-equality and renaming of bound variables. We want an account that is mathematically rigorous, yet transparently clear to users. To illustrate how this is accomplished, I refer to the working material by W. Aitken A Formal Introduction to the Lambda Calculus [2]. This theory is easy to express in Naive Type Theory. Here are some highlights. Definition The $\lambda$terms are the following inductively defined class.

terms

$$x, y, z, \ldots$$

Induction Principle

The induction principle corresponding to this class is given by

$$f, a, b \lambda$$

$$\frac{P(v) \mbox{for} v \mbox{a variable} {P(f) \& P(a)\Rig... ...ightarrow P(\lambda(x.b))}}{\forall t:\lambda\mbox{term.} P(t)}$$

Inductive Definitions

Objects can be defined inductively over the class of $\lambda$terms using the same induction principle. Here is the definition of the set of free variables, FV(t), of a term t.

$$\{v\}$$

Based on the syntactic theory, we can define exactly the kind of substitution we want. The interesting feature is that it must rename bound variables to avoid capture and rename them in a minimal way, i. e.  rename as few variables as possible. For example, in

$$\lambda(x. \lambda(y. ap(z; x)))$$

if we substitute x for z, then we must rename the bound occurrences of x, but we do not want to rename them to y, because this will cause y to be renamed in the scope of x.

Aitken gives a precise definition of all this. He uses the concept t[s/x]t' defined as:

Definition We say that t' is a substitution of s for x in t, written    t[s/x]t',

iff

Theorem: $\forall t, s:$LTerm. $\forall x:$Var. $\exists t':$LTerm

$$t[s/x]t' \&$$

From a (constructive) proof of this $\forall\exists$ formula, we can extract a function to compute t' from t and s.