# The self-reduction in lambda calculus

- Authors
- Journal
- Theoretical Computer Science 0304-3975
- Publisher
- Elsevier
- Publication Date
- Volume
- 235
- Issue
- 1
- Identifiers
- DOI: 10.1016/s0304-3975(99)00190-5
- Keywords

## Abstract

Abstract In this paper, the authors discuss the internal code for λ terms: ⌈ ⌉:Λ→Λ which is defined by ⌈x⌉≡λe.eU 1 3xe, ⌈PQ⌉≡λe.eU 2 3⌈P⌉⌈Q⌉e, ⌈λx.P⌉ ≡ λe.eU 3 3(λx.⌈P⌉)e, where U i 3 ≡ λx 1x 2x 3.x i (i=1,2,3). The main result is that there exists a self-reductor R such that 1. R ∈ Λ 0 ∩ NF 2. ∀M ∈ Λ 0.M has nf M nf ⇒ R ⌈M⌉ = β ⌈M nf⌉ 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.

## There are no comments yet on this publication. Be the first to share your thoughts.