The self-reduction in lambda calculus

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.