A.1 The first presentation

The objects and types of our type theoryPlanetmathPlanetmath may be written as terms using the following syntax, which is an extensionPlanetmathPlanetmathPlanetmath of λ-calculus with variables x,x,, primitive constants c,c,, defined constants f,f,, and term forming operationsMathworldPlanetmath


The notation used here means that a term t is either a variable x, or it has the form λx.t where x is a variable and t is a term, or it has the form t(t) where t and t are terms, or it is a primitive constant c, or it is a defined constant f. The syntactic markers ’λ’, ’(’, ’)’, and ’.’ are punctuation for guiding the human eye.

We use t(t1,,tn) as an abbreviation for the repeated application t(t1)(t2)(tn). We may also use infix notation, writing t1t2 for (t1,t2) when 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


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


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

The second kind of defined constant is used to specify a (parameterized) mapping f(x1,,xn,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


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 numbersMathworldPlanetmath. 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 tt between terms t and t is the equivalence relationMathworldPlanetmath generated by the defining equations for constants, the computation rule


and the rules which make it a congruencePlanetmathPlanetmathPlanetmath with respect to application and λ-abstraction:

  • if tt and ss then t(s)t(s), and

  • if tt then (λx.t)(λx.t).

The equality judgment tu:A is then derived by the following single rule:

  • if t:A, u:A, and tu, then tu:A.

Judgmental equality is an equivalence relation.

Title A.1 The first presentationMathworldPlanetmathPlanetmath