Lexicographic Path Induction

Carsten Schürmann, Jeffrey Sarnat

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review

    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.
    OriginalsprogEngelsk
    BogserieLecture Notes in Computer Science
    Sider (fra-til)279
    Antal sider293
    ISSN0302-9743
    DOI
    StatusUdgivet - 2009
    BegivenhedTyped Lambda Calculi and Applications - Brasilia, Brasilien
    Varighed: 1 jul. 20093 jul. 2009

    Konference

    KonferenceTyped Lambda Calculi and Applications
    Land/OmrådeBrasilien
    ByBrasilia
    Periode01/07/200903/07/2009

    Emneord

    • Programming languages theory
    • Consistency proof
    • Transfinite induction
    • Lexicographic path ordering
    • Martin-Löf's intuitionistic theory

    Citationsformater