Abstract
The Calculus of Constructions is a higher-order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn [2,3], Girard [12], Martin-Löf[14] and Scott [18]. The calculus and its syntactic theory were presented in Coquand's thesis [7], and an implementation by the author was used to mechanically verify a substantial number of proofs demonstrating the power of expression of the formalism [9]. The Calculus of Constructions is proposed as a foundation for the design of programming environments where programs are developed consistently with formal specifications. The current paper shows how to define inductive concepts in the calculus.
A very general induction schema is obtained by postulating all elements of the type of interest to belong to the standard interpretation associated with a predicate map. This is similar to the treatment of D. Park [16], but the power of expression of the formalism permits a very direct treatment, in a language that is formalized enough to be actually implemented on computer. Special instances of the induction schema specialize to Nœtherian induction and Structural induction over any algebraic type. Computational Induction is treated in an axiomatization of Domain Theory in Constructions. It is argued that the resulting principle is more powerful than LCF's [13], since the restriction on admissibility is expressible in the object language.
This research, done during a sabbatical at Carnegie Mellon University, was supported in part by the Office of Naval Research under contract N00014-84-K-0415 and in part by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 5404, monitored by the Office of Naval Research under the same contract. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of DARPA or the U.S. Government.
Download to read the full chapter text
Chapter PDF
References
R. Boyer, J Moore. “A Computational Logic.” Academic Press (1979).
N.G. de Bruijn. “Automath a language for mathematics.” Les Presses de l'Université de Montréal, (1973).
N.G. de Bruijn. “A survey of the project Automath.” (1980) in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds Seldin J. P. and Hindley J. R., Academic Press (1980).
R. Burstall. “Proving Properties of Programs by Structural Induction.” Comp. J. 12 (1969), 41–48.
P. M. Cohn. “Universal Algebra.” Reidel, 1965.
R.L. Constable, N.P. Mendler. “Recursive Definitions in Type Theory.” Private Communication (1985).
Th. Coquand. “Une théorie des constructions.” Thèse de troisième cycle, Université Paris VII, Janvier 85.
Th. Coquand. “An analysis of Girard's paradox.” First IEEE Symposium on Logic in Computer Science, Boston (June 1986), 227–236.
Th. Coquand and G. Huet. “Constructions: A Higher Order Proof System for Mechanizing Mathematics.” EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).
Th. Coquand and G. Huet. “The Calculus of Constructions.” To appear, Information and Control.
Th. Coquand and G. Huet. “Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions.” Logic Colloquium, Orsay (July 85). To appear, North-Holland.
J.Y. Girard. “Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieure.” Thèse d'Etat, Université Paris VII (1972).
M. Gordon, R. Milner and C. Wadsworth. “Edinburgh LCF.” Springer-Verlag LNCS 78 (1979).
P. Martin-Löf. “A theory of types.” Report 71-3, Dept. of Mathematics, University of Stockholm, Feb. 1971, revised (Oct. 1971).
N.P. Mendler. “First and Second-Order Lambda Calculi with Recursive Types.” Technical Report TR 86-764, Dept. of Computer Science, Cornell University (July 1986).
D. Park. “Fixpoint Induction and Proofs of Program Properties.” Machine Intelligence 5, Eds. B. Meltzer & D. Michie, 59–77, Edinburgh University Press.
L. C. Paulson. “Constructing Recursion Operators in Intuitionistic Type Theory.” Tech. Report 57, Computer Laboratory, University of Cambridge (Oct. 1984). To appear, J. of Symbolic Computation.
D. Scott. “Constructive validity.” Symposium on Automatic Demonstration, Springer-Verlag Lecture Notes in Mathematics, 125 (1970).
D. Scott. “Data Types as Lattices.” SIAM Journal of Computing 5 (1976) 522–587.
A. Tarski. “A Lattice-Theoretical Fixpoint Theorem and its Applications.” Pacific J. Math. 5 (1955), 285–309.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huet, G. (1987). Induction principles formalized in the calculus of constructions. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds) TAPSOFT '87. CAAP 1987. Lecture Notes in Computer Science, vol 249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17660-8_62
Download citation
DOI: https://doi.org/10.1007/3-540-17660-8_62
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17660-2
Online ISBN: 978-3-540-47746-4
eBook Packages: Springer Book Archive