LAMBDA(BETA') - A LAMBDA-CALCULUS WITH A GENERALIZED BETA-REDUCTION RULE

Authors
OBEROI S
Citation
S. Oberoi, LAMBDA(BETA') - A LAMBDA-CALCULUS WITH A GENERALIZED BETA-REDUCTION RULE, Information processing letters, 54(1), 1995, pp. 45-53
Citations number
5
Categorie Soggetti
Information Science & Library Science","Computer Science Information Systems
Journal title
Information processing letters → ACNP
ISSN journal
00200190
Volume
54
Issue
1
Year of publication
1995
Pages
45 - 53
Database
ISI
SICI code
0020-0190(1995)54:1<45:L-ALWA>2.0.ZU;2-X
Abstract
The classical notion of beta-reduction in the lambda-calculus has an a rbitrary syntactically-imposed sequentiality. A new notion of reductio n beta' is defined which is a generalization of beta-reduction. This n otion of reduction is shown to satisfy the Church-Rosser property as w ell as some other fundamental properties, leading to the conclusion th at this generalized notion of beta'-reduction can be used in place of beta-reduction without sacrificing any of the fundamental properties.