Lexicographic Path Induction
Lexicographic Path Induction
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-Loef's intuitionistic theory of inductive definitions.
The consistency of Heyting arithmetic follows directly, and weak
normalization for Goedel's T follows indirectly; both have been
formalized in a prototypical extension of Twelf.
Paper
A paper is available. TLCA 2009, Brasila, Brazil.
Twelf Sources
Supplementing Section 4.2: The Normalization Procedure for the Logic of Inductive Definitions
Supplementing Section 4.3: Heyting Arithmetic
Supplementing Section 4.4: Weak Normalization of Goedel's T
Installation Instructions
To load the files, you will need a version of Twelf with a prototypical
extension of the termination checker to the LPO ordering. This extension
is a prototype, and still under development. It can be accessed
via
svn co https://cvs.concert.cs.cmu.edu/twelf/branches/twelf-lpo
and compiled using make smlnj. For more information how to install and use Twelf, refer to the Twelf project homepage. Enjoy.
Last modified: Wed Jan 28 17:59:11 CET 2009