Conservativeness of Λ over λσ-calculus

Λ is a unique functional programming language which has the facility of the encapsulated assignment, without losing referential transparency. The let-construct in Λ can be considered as an environment, which has a close relationship to substitution in λσ-calculus. This paper discusses the relationship between these two calculi; we first define a slightly modified version of Λ-calculus which adopts de Bruijn's index notation. We then define an injective map from λσ-calculus to Λ, and show that the Beta-reduction and the σ-reductions in λσ-calculus correspond to the β-reduction and let-reductions in Λ-calculus, respectively. Finally, we prove that, as equality theories, Λ is conservative over the λσ-calculus.

Authors and Affiliations

1. Research Institute of Electrical Communication, Tohoku University, 980, Sendai, Japan

   Masahiko Sato & Yukiyoshi Kameyama

Reprints and permissions

© 1994 Springer-Verlag Berlin Heidelberg

Policies and ethics