# A.1 The first presentation

The objects and types of our type theory may be written as terms using the following syntax, which is an extension of $\lambda$-calculus with variables $x,x^{\prime},\dots$, primitive constants $c,c^{\prime},\dots$, defined constants $f,f^{\prime},\dots$, and term forming operations

 $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 it has the form ${\lambda}x.\,t$ where $x$ is a variable and $t$ is a term, or it has the 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},\dots,t_{n})$ as an abbreviation for the repeated application $t(t_{1})(t_{2})\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 defined constant.

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

 $f(x_{1},\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},\dots,x_{n},x)$, where $x$ ranges over a type whose elements are generated by zero or more primitive constants. For each such primitive constant $c$ there is a defining equation of the form

 $f(x_{1},\dots,x_{n},c(y_{1},\dots,y_{m})):\!\!\equiv t,$

where $f$ may occur in $t$, but only in such a way that it is clear that the equations determine a totally defined function. The paradigm examples of such defined functions are the functions defined by primitive recursion on the natural numbers. We may call this kind of definition of a function a total recursive definition. In computer science and logic this kind of definition of a function on a recursive data type has been called a definition by structural 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.

Title A.1 The first presentation
\metatable