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 -calculus with variables , primitive constants , defined constants , and term forming operations
The notation used here means that a term is either a variable , or it has the form where is a variable and is a term, or it has the form where and are terms, or it is a primitive constant , or it is a defined constant . The syntactic markers ’’, ’(’, ’)’, and ’.’ are punctuation for guiding the human eye.
We use as an abbreviation for the repeated application . We may also use infix notation, writing for 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 has a single defining equation
where does not involve . For example, we might introduce the explicit defined constant with defining equation
The second kind of defined constant is used to specify a (parameterized) mapping , where ranges over a type whose elements are generated by zero or more primitive constants. For each such primitive constant there is a defining equation of the form
where may occur in , 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 between terms and is the equivalence relation generated by the defining equations for constants, the computation rule
and the rules which make it a congruence with respect to application and -abstraction:
if and then , and
if then .
The equality judgment is then derived by the following single rule:
if , , and , then .
Judgmental equality is an equivalence relation.
|Title||A.1 The first presentation|