# 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
• Lambda Calculus
• Self-Reduction

## 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.

Seen <100 times

# More articles like this

May 1987

## Combinatory weak reduction in lambda calculus

on Theoretical Computer Science Jan 01, 1998

1995

## Parallel Reduction in Resource Lambda-Calculus

Dec 14, 2009
More articles like this..