Proving the genericity lemma by leftmost reduction is simple

Jan Kuper; J. Hsiang

doi:10.1007/3-540-59200-8_63

Proving the genericity lemma by leftmost reduction is simple

Jan Kuper, J. Hsiang (Editor)

Research output: Contribution to conference › Paper › peer-review

363 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 language	Undefined
Pages	271-278
Number of pages	8
DOIs	https://doi.org/10.1007/3-540-59200-8_63
Publication status	Published - Apr 1995
Event	Rewriting Techniques and Applications - Kaiserslautern, Germany Duration: 5 Apr 1995 → 7 Apr 1995

Conference

Conference	Rewriting Techniques and Applications
Period	5/04/95 → 7/04/95
Other	5-7 April 1995

Keywords

EWI-11088
IR-61924

Access to Document

10.1007/3-540-59200-8_63

RTA95

Cite this

@conference{b80e79f957d84f299e60dd1827af12bb,

title = "Proving the genericity lemma by leftmost reduction is simple",

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.",

keywords = "EWI-11088, IR-61924",

author = "Jan Kuper and J. Hsiang",

year = "1995",

month = apr,

doi = "10.1007/3-540-59200-8\_63",

language = "Undefined",

pages = "271--278",

note = "Rewriting Techniques and Applications ; Conference date: 05-04-1995 Through 07-04-1995",

}

TY - CONF

T1 - Proving the genericity lemma by leftmost reduction is simple

AU - Kuper, Jan

A2 - Hsiang, J.

PY - 1995/4

Y1 - 1995/4

N2 - 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.

AB - 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.

KW - EWI-11088

KW - IR-61924

U2 - 10.1007/3-540-59200-8_63

DO - 10.1007/3-540-59200-8_63

M3 - Paper

SP - 271

EP - 278

T2 - Rewriting Techniques and Applications

Y2 - 5 April 1995 through 7 April 1995

ER -