A.1 The first presentation

The objects and types of our type theory may be written as terms usingthe following syntax, which is an extension of $\lambda$-calculus withvariables $x,x^{\prime },\mathrm{\dots }$,primitive constants$c,c^{\prime },\mathrm{\dots }$, defined constants $f,f^{\prime },\mathrm{\dots }$, and term formingoperations

$$t::=x\mid \lambda x.t\mid t(t^{\prime })\mid c\mid f$$

The notation used here means that a term $t$ is either a variable $x$, or ithas the form $\lambda x.t$ where $x$ is a variable and $t$ is a term, or it hasthe form $t(t^{\prime })$ where $t$ and $t^{\prime }$ are terms, or it is a primitive constant$c$, or it is a defined constant $f$. The syntactic markers ’$\lambda$’, ’(’,’)’, and ’.’ are punctuation for guiding the human eye.

We use $t(t_1,\mathrm{\dots },t_n)$ as an abbreviation for the repeated application$t(t_1)(t_2)\mathrm{\dots }(t_n)$. We may also use infix notation, writing $t_1\star t_2$ for $\star (t_1,t_2)$ when $\star$ is a primitive or definedconstant.

Each defined constant has zero, one or more defining equations.There are two kinds of defined constant. An explicitdefined constant $f$ has a single defining equation

$$f(x_1,\mathrm{\dots },x_n):\equiv t,$$

where $t$ does not involve $f$.For example, we might introduce the explicit defined constant $\circ$ with defining equation

$$\circ (x,y)(z):\equiv x(y(z)),$$

and use infix notation $x\circ y$ for $\circ (x,y)$. This of course is just composition of functions.

The second kind of defined constant is used to specify a (parameterized) mapping$f(x_1,\mathrm{\dots },x_n,x)$, where $x$ ranges over a type whose elements are generatedby zero or more primitive constants. For each such primitive constant $c$ thereis a defining equation of the form

$$f(x_1,\mathrm{\dots },x_n,c(y_1,\mathrm{\dots },y_m)):\equiv t,$$

where $f$ may occur in $t$, but only in such a way that it is clear that theequations determine a totally defined function. The paradigm examples of suchdefined functions are the functions defined by primitive recursion on thenatural numbers. We may call this kind of definition of a function a totalrecursive definition.In computer science and logic this kind of definitionof a function on a recursive data type has been called a definition bystructural recursion.

Convertibility$t\downarrow t^{\prime }$ between terms $t$and $t^{\prime }$ is the equivalence relation generated by the defining equations for constants,the computation rule

$$(\lambda x.t)(u):\equiv t[u/x],$$

and the rules which make it a congruence with respect to application and $\lambda$-abstraction:

• if $t\downarrow t^{\prime }$ and $s\downarrow s^{\prime }$ then $t(s)\downarrow t^{\prime }(s^{\prime })$, and

• if $t\downarrow t^{\prime }$ then $(\lambda x.t)\downarrow (\lambda x.t^{\prime })$.

The equality judgment $t\equiv u:A$ is then derived by the following single rule:

• if $t:A$, $u:A$, and $t\downarrow u$, then $t\equiv u:A$.

Judgmental equality is an equivalence relation.