Abstract
Programming languages theory is full of problems that reduce to proving the consistency of a logic, such as the normalization of typed lambda-calculi, the decidability of equality in type theory, equivalence testing of traces in security, etc. Although the principle of transfinite induction is routinely employed by logicians in proving such theorems, it is rarely used by programming languages researchers, who often prefer alternatives such as proofs by logical relations and model theoretic constructions. In this paper we harness the well-foundedness of the lexicographic path ordering to derive an induction principle that combines the comfort of structural induction with the expressive strength of transfinite induction. Using lexicographic path induction, we give a consistency proof of Martin-Löf’s intuitionistic theory of inductive definitions. The consistency of Heyting arithmetic follows directly, and weak normalization for Gödel’s T follows indirectly; both have been formalized in a prototypical extension of Twelf.
This work was in part supported by grant CCR-0325808 of the National Science Foundation and NABITT grant 2106-07-0019 of the Danish Strategic Research Council.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Tahhan Bittar, E.: Strong normalization proofs for cut-elimination in Gentzen’s sequent calculi. In: Proceedings of the Symposium: Algebra and Computer Science. Helena Rasiowa in memoriam, vol. 46, pp. 179–225. Banach Center Publications (1999)
Brotherston, J.: Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh (November 2006)
Buchholz, W.: Proof-theoretic analysis of termination proofs. Ann. Pure Appl. Logic 75(1-2), 57–65 (1995)
Dershowitz, N., Okada, M.: Proof-theoretic techniques for term rewriting theory. In: LICS, pp. 104–111. IEEE Computer Society Press, Los Alamitos (1988)
Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Studia Logica 60(1), 107–118 (1998)
Dybjer, P.: Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In: Logical Frameworks, pp. 280–306. Cambridge University Press, Cambridge (1991)
Gentzen, G.: New version of the consistency proof for elementary number theory. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 252–286. North-Holland Publishing Co., Amsterdam (1969)
Gacek, A., Miller, D., Nadathur, G.: Combining generic judgments with recursive definitions. In: Pfenning, F. (ed.) Proceedings of LICS 2008, pp. 33–44. IEEE Computer Society, Los Alamitos (2008)
Howard, W.A.: Assignment of ordinals to terms for primitive recursive functions of finite type. In: Kino, A., Myhill, J., Vesley, R.E. (eds.) Intuitionism and Proof Theory, pp. 443–458. North-Holland, Amsterdam (1970)
Kamin, S., Levy, J.-J.: Attemps for generalising the recursive path orderings. Unpublished lecture notes (1980)
Martin-Löf, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium. North-Holland, Amsterdam (1971)
McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science 232(1-2), 91–119 (2000)
Georg Moser, I.L.: Why ordinals are good for you. In: ESSLLI 2003 - Course Material II. Collegium Logicum, vol. 6, pp. 1–65. The Kurt Gödel Society (2004)
Momigliano, A., Tiu, A.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 293–308. Springer, Heidelberg (2004)
Pfenning, F.: Structural cut elimination. In: Kozen, D. (ed.) Proceedings of the Tenth Annual Symposium on Logic in Computer Science, San Diego, California, pp. 156–166. IEEE Computer Society Press, Los Alamitos (1995)
Paulin-Mohring, C.: Inductive Definitions in the System Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993); LIP research report 92-49
Schütte, K.: Proof Theory. Springer, Heidelberg (1977)
Schürmann, C., Sarnat, J.: Structural logical relations. In: Pfenning, F. (ed.) Proceedings of LICS 2008, pp. 69–80. IEEE Computer Society Press, Los Alamitos (2008)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (2000)
Urban, C.: Strong normalisation for a Gentzen-like cut-elimination procedure. In: Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications, Krakow, Poland, May 2001, pp. 415–442 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sarnat, J., Schürmann, C. (2009). Lexicographic Path Induction. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)