Naive Computational Type Theory
by Robert L. Constable
Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen (eds.), pp. 213-259
The basic concepts of type theory are fundamental to computer science, logic and mathematics. Indeed, the language of type theory connects these regions of science. It plays a role in computing and information science akin to that of set theory in pure mathematics.
There are many excellent accounts of the basic ideas of type theory, especially at the interface of computer science and logic -- specifically, in the literature of programming languages, semantics, formal methods and automated reasoning. Most of these are very technical, dense with formulas, inference rules, and computation rules. Here we follow the example of the mathematician Paul Halmos, who in 1960 wrote a 104-page book called Naive Set Theory intended to make the subject accessible to practicing mathematicians. His book served many generations well.
This article follows the spirit of Halmos' book and introduces type theory without recourse to precise axioms and inference rules, and with a minimum of formalism. I start by paraphrasing the preface to Halmos' book. The sections of this article follow his chapters closely.
Every computer scientist agrees that every computer scientist must know some type theory; the disagreement begins in trying to decide how much is some. This article contains my partial answer to that question. The purpose of the article is to tell the beginning student of advanced computer science the basic type theoretic facts of life, and to do so with a minimum of philosophical discourse and logical formalism. The point throughout is that of a prospective computer scientist eager to study programming languages, or database systems, or computational complexity theory, or distributed systems or information discovery.
In type theory, "naive" and "formal" are contrasting words. The present treatment might best be described as informal type theory from a naive point of view. The concepts are very general and very abstract; therefore they may take some getting used to. It is a mathematical truism, however, that the more generally a theorem applies, the less deep it is. The student's task in learning type theory is to steep himself or herself in unfamiliar but essentially shallow generalities until they become so familiar that they can be used with almost no conscious effort.
Type theory has been well exposited in articles by N. G. de Bruijn and the Automath group; the writings of Per Martin-Lof, the originator of many of the basic ideas; the writings of Jean-Yves Girard, another originator; the writings of the Coq group, the Cornell group, and the Gothenberg group; and the writings of others who have collectively expanded and applied type theory.
What is new in this account is treatment of classes and computational complexity theory along lines that seem very natural. This approach to complexity theory raises many new questions.
Table of Contents
Section 1: Types And Equality
Section 2: Subtypes And Set Types
Section 3: Pairs
Section 4: Union And Intersection
Section 5: Functions And Relations
Section 6: Universes, Powers And Openness
Section 7: Families
Section 8: Lists And Numbers
Section 9: Logic And The Peano Axioms
Section 10: Structures, Records And Classes
Section 11: The Axiom Of Choice
Section 12: Computational Complexity
|2/11/03||Title was changed from "Naive Type Theory" to "Naive Computational Type Theory" per Bob. Now the title is the same as that of the former version published in Proof and System-Reliability (see 11/1/02 note below).|
|11/5/02||Typo corrected in Section 1, "Types and equality," under "Equality."
The first formula had read incorrectly:
� � � x=y mod(m) iff (x-y)=k [etc.]
It has now been corrected to:
� � � x=y mod(k) iff (x-y)=k [etc.]
|11/1/02||"Naive Type Theory" is a revised version of R. Constable, "Naive Computational Type Theory," in H. Schwichtenberg & R. Steinbrueggen, eds., Proof and System-Reliability, NATO Science Series III, pp. 213-260, Kluwer Academic Publishers, 2002.|
bibTex ref: Con02