Proving the genericity lemma by leftmost reduction is simple

Kuper, J. (1995) Proving the genericity lemma by leftmost reduction is simple. In: Rewriting Techniques and Applications, 5-7 April 1995, Kaiserslautern, Germany.

PDF
Restricted to UT campus only: Request a copy
381Kb

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.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Computer Architecture for Embedded Systems (CAES)
Link to this item:	http://purl.utwente.nl/publications/61924
Official URL:	http://dx.doi.org/10.1007/3-540-59200-8_63
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page