The self-reduction in lambda calculus
In this paper, the authors discuss the internal code for lambda terms: inverted right perpendicular inverted left perpendicular : Lambda --> Lambda which 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 right perpendicular Q inverted left perpendicular e, inverted right perpendicular lambda x.P inverted left perpendicular = lambda e.eU(3)(3)(lambda x. inverted right perpendicular P inverted left perpendicular)e, where U-i(3) = lambda x(1)x(2)x(3).x(i) (i = 1, 2, 3). The main result is that 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 arrow R inverted right perpendicular M inverted left perpendicular = beta inverted right perpendicular M-nf inverted left perpendicular (3) For All M is an element of Lambda degrees.M has no nf double right arrow R inverted right perpendicular M inverted left perpendicular has no nf. In 1992, J. Mogensen defined an internal code in lambda-calculus, with which 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 lambda-calculus and showed that there exists a self-reductor R, which satisfies (1) and (2) above. The internal code used in this paper was mentioned by 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 results and simplified the proof of existence a selfreductor. (C) 2000 Elsevier Science B.V. All rights reserved.
self-reduction lambda calculus