Proving the genericity lemma by leftmost reduction is simple

Jan Kuper, J. Hsiang (Editor)

    Research output: Contribution to conferencePaperpeer-review

    322 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
    EventRewriting Techniques and Applications - Kaiserslautern, Germany
    Duration: 5 Apr 19957 Apr 1995

    Conference

    ConferenceRewriting Techniques and Applications
    Period5/04/957/04/95
    Other5-7 April 1995

    Keywords

    • EWI-11088
    • IR-61924

    Cite this