ITU

Lexicographic Path Induction

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Standard

Lexicographic Path Induction. / Schürmann, Carsten; Sarnat, Jeffrey.

In: Lecture Notes in Computer Science, 2009, p. 279.

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Harvard

Schürmann, C & Sarnat, J 2009, 'Lexicographic Path Induction', Lecture Notes in Computer Science, pp. 279. https://doi.org/10.1007/978-3-642-02273-9

APA

Schürmann, C., & Sarnat, J. (2009). Lexicographic Path Induction. Lecture Notes in Computer Science, 279. https://doi.org/10.1007/978-3-642-02273-9

Vancouver

Schürmann C, Sarnat J. Lexicographic Path Induction. Lecture Notes in Computer Science. 2009;279. https://doi.org/10.1007/978-3-642-02273-9

Author

Schürmann, Carsten ; Sarnat, Jeffrey. / Lexicographic Path Induction. In: Lecture Notes in Computer Science. 2009 ; pp. 279.

Bibtex

@inproceedings{d5ea9d20e31311dea523000ea68e967b,
title = "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-L{\"o}f{\textquoteright}s intuitionistic theory of inductive definitions. The consistency of Heyting arithmetic follows directly, and weak normalization for G{\"o}del{\textquoteright}s T follows indirectly; both have been formalized in a prototypical extension of Twelf.",
author = "Carsten Sch{\"u}rmann and Jeffrey Sarnat",
note = "Volumne: 5608/2009; null ; Conference date: 01-07-2009 Through 03-07-2009",
year = "2009",
doi = "10.1007/978-3-642-02273-9",
language = "English",
pages = "279",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer",

}

RIS

TY - GEN

T1 - Lexicographic Path Induction

AU - Schürmann, Carsten

AU - Sarnat, Jeffrey

N1 - Volumne: 5608/2009

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-02273-9

DO - 10.1007/978-3-642-02273-9

M3 - Conference article

SP - 279

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

Y2 - 1 July 2009 through 3 July 2009

ER -

ID: 1036831