The self-reduction in lambda calculus

Citation
Fm. Song et al., The self-reduction in lambda calculus, THEOR COMP, 235(1), 2000, pp. 171-181
Citations number
6
Language
INGLESE
art.tipo
Article
Categorie Soggetti
Computer Science & Engineering
Journal title
THEORETICAL COMPUTER SCIENCE
ISSN journal
0304-3975 → ACNP
Volume
235
Issue
1
Year of publication
2000
Pages
171 - 181
Database
ISI
SICI code
0304-3975(20000317)235:1<171:TSILC>2.0.ZU;2-S
Abstract
In this paper, the authors discuss the internal code for lambda terms: inve rted right perpendicular inverted left perpendicular : Lambda --> Lambda wh ich is defined by inverted right perpendicular x inverted left perpendicular = lambda e.eU(1) (3)xe, inverted right perpendicular PQ inverted left perpendicular = lambda e.eU(2 )(3) inverted right perpendicular P inverted left perpendicular inverted ri ght perpendicular Q inverted left perpendicular e, inverted right perpendicular lambda x.P inverted left perpendicular = lambd a e.eU(3)(3)(lambda x. inverted right perpendicular P inverted left perpend icular)e, where U-i(3) = lambda x(1)x(2)x(3).x(i) (i = 1, 2, 3). The main result is t hat there exists a self-reductor R such that (1) R is an element of Lambda degrees boolean AND NF (2) For All M is an element of Lambda degrees.M has nf M-nf double right ar row R inverted right perpendicular M inverted left perpendicular = beta inv erted right perpendicular M-nf inverted left perpendicular (3) For All M is an element of Lambda degrees.M has no nf double right arro w R inverted right perpendicular M inverted left perpendicular has no nf. In 1992, J. Mogensen defined an internal code in lambda-calculus, with whic h he showed that there exists a self-reductor R which satisfies (2) and (3) above. Later, A. Berarducci and C. Bohm defined another internal code in l ambda-calculus and showed that there exists a self-reductor R, which satisf ies (1) and (2) above. The internal code used in this paper was mentioned b y A. Berarducci and C, Bohm, and is different from Mogensen's, but it is an alternation of Berarducci and Bohm's. The authors improved the former resu lts and simplified the proof of existence a selfreductor. (C) 2000 Elsevier Science B.V. All rights reserved.