Affordable Access

Publisher Website

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.

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

Statistics

Seen <100 times
0 Comments

More articles like this

Combinatory weak reduction in lambda calculus

on Theoretical Computer Science Jan 01, 1998

Reduction graphs in the lambda calculus

on Theoretical Computer Science Jan 01, 1984

Needed reduction and spine strategies for the lamb...

on Information and Computation Jan 01, 1987
More articles like this..