Proving the genericity lemma by leftmost reduction is simple

Jan Kuper, J. Hsiang (Editor)

    Research output: Contribution to conferencePaper

    110 Downloads (Pure)


    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
    Number of pages8
    Publication statusPublished - Apr 1995


    • EWI-11088
    • IR-61924

    Cite this