In this report we present an elementary and general proof of the GenericityLemma, which says (in the untyped lambda calculus): Suppose M is an unsolvable term, and let N be a normal form. If FM = N, then for each term X we have FX = N. The informal meaning of this lemma is that if a term M is meaningless (undefined), and if a context containing M is convertible to a well-defined answer, then M did not have any influence on the computation of this answer and so M may be replaced by any term. In fact, 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. In this report we prove the Genericity Lemma for a more general situation than just untyped lambda calculus. Therefore, we first generalize the notion of solvability towards typed lambda calculi. We call this generalization usability, and we show that the Genericity Lemma holds for un-usable terms. We prove the lemma by concentrating on the leftmost reduction of FM. This strongly simplifies the proofs that are known from the literature.
展开▼
