Proving the genericity lemma by leftmost reduction is simple

Jan Kuper, J. Hsiang (Editor)

    Research output: Contribution to conferencePaper

    47 Downloads (Pure)

    Abstract

    The Genericity Lemma is one of the most important motivations to take in the untyped lambda calculus the notion of solvability as a formal representation of the informal notion of undefinedness. We generalise solvability towards typed lambda calculi, and we call this generalisation: usability. We then prove the Genericity Lemma for un-usable terms. The technique of the proof is based on leftmost reduction, which strongly simplifies the standard proof.
    Original languageUndefined
    Pages271-278
    Number of pages8
    DOIs
    Publication statusPublished - Apr 1995

    Keywords

    • EWI-11088
    • IR-61924

    Cite this

    @conference{b80e79f957d84f299e60dd1827af12bb,
    title = "Proving the genericity lemma by leftmost reduction is simple",
    abstract = "The Genericity Lemma is one of the most important motivations to take in the untyped lambda calculus the notion of solvability as a formal representation of the informal notion of undefinedness. We generalise solvability towards typed lambda calculi, and we call this generalisation: usability. We then prove the Genericity Lemma for un-usable terms. The technique of the proof is based on leftmost reduction, which strongly simplifies the standard proof.",
    keywords = "EWI-11088, IR-61924",
    author = "Jan Kuper and J. Hsiang",
    year = "1995",
    month = "4",
    doi = "10.1007/3-540-59200-8_63",
    language = "Undefined",
    pages = "271--278",

    }

    Proving the genericity lemma by leftmost reduction is simple. / Kuper, Jan; Hsiang, J. (Editor).

    1995. 271-278.

    Research output: Contribution to conferencePaper

    TY - CONF

    T1 - Proving the genericity lemma by leftmost reduction is simple

    AU - Kuper, Jan

    A2 - Hsiang, J.

    PY - 1995/4

    Y1 - 1995/4

    N2 - The Genericity Lemma is one of the most important motivations to take in the untyped lambda calculus the notion of solvability as a formal representation of the informal notion of undefinedness. We generalise solvability towards typed lambda calculi, and we call this generalisation: usability. We then prove the Genericity Lemma for un-usable terms. The technique of the proof is based on leftmost reduction, which strongly simplifies the standard proof.

    AB - The Genericity Lemma is one of the most important motivations to take in the untyped lambda calculus the notion of solvability as a formal representation of the informal notion of undefinedness. We generalise solvability towards typed lambda calculi, and we call this generalisation: usability. We then prove the Genericity Lemma for un-usable terms. The technique of the proof is based on leftmost reduction, which strongly simplifies the standard proof.

    KW - EWI-11088

    KW - IR-61924

    U2 - 10.1007/3-540-59200-8_63

    DO - 10.1007/3-540-59200-8_63

    M3 - Paper

    SP - 271

    EP - 278

    ER -