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.
Cite
CITATION STYLE
Kuper, J. (1995). Proving the genericity lemma by leftmost reduction is simple. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 914, pp. 271–278). Springer Verlag. https://doi.org/10.1007/3-540-59200-8_63
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
