The self-reduction in lambda calculus

AbstractIn this paper, the authors discuss the internal code for λ terms: ⌈⌉:Λ→Λ which is defined by⌈x⌉≡λe.eU13xe,⌈PQ⌉≡λe.eU23⌈P⌉⌈Q⌉e,⌈λx.P⌉≡λe.eU33(λx.⌈P⌉)e,where Ui3≡λx1x2x3.xi (i=1,2,3). The main result is that there exists a self-reductor R such that 1.R∈Λ0∩NF2.∀M∈Λ0.M has nfMnf⇒R⌈M⌉=β⌈Mnf⌉3.∀M∈Λ0.M has no nf⇒R⌈M⌉ has no nf. In 1992, J. Mogensen defined an internal code in λ-calculus, with which he showed that there exists a self-reductor R which satisfies (2) and (3) above. Later, A. Berarducci and C. Böhm defined another internal code in λ-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. Böhm, and is different from Mogensen's, but it is an alternation of Berarducci and Böhm's. The authors improved the former results and simplified the proof of existence a self-reductor