Strong Normalizability of the Simply-Typed Lambda Calculus with Environment Extraction from Function Closures

DOI

10.2991/978-94-6463-684-0_3How to use a DOI?

Keywords

typed lambda calculus; function closure; environment; strong normalizability

Abstract

A function closure is a construct that encapsulates the body of a function, along with the bindings of free variables to their corresponding values in the scope of the function. Environment extraction refers to the process of retrieving these bindings from a function closure. A lambda calculus with environment extraction is a computational framework designed to facilitate this process.

The simple type system, a basic type theory, is based atomic types and function types. The lambda calculus equipped with a simple type system, commonly known as the simply typed lambda calculus, exhibits the property of strong normalization. Strong normalization ensures that, regardless of the order of reductions, the reduction sequence always terminates in a finite number of steps, yielding an irreducible normal form. In this study, we extend the simply typed lambda calculus by integrating the mechanism of environment extraction. We establish that the strong normalization property is preserved in this extended framework. The proof proceeds as follows: first, we define the λX calculus, which incorporates environment extraction. Then, we introduce the λrp calculus, which uses records and pairs. We define translation rules between the λX calculus and the λrp calculus, and prove their soundness. We then assign types to both calculi and verify type preservation. In addition, we formalize the notion of term length in the λX calculus. Finally, we prove the strong normalization of the λrp calculus and use this result to establish the strong normalization of the λX calculus.

Copyright

© 2025 The Author(s)

Open Access

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

TY  - CONF
AU  - Kosuke Kaneshita
AU  - Shinya Nishizaki
PY  - 2025
DA  - 2025/04/30
TI  - Strong Normalizability of the Simply-Typed Lambda Calculus with Environment Extraction from Function Closures
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2024)
PB  - Atlantis Press
SP  - 20
EP  - 36
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6463-684-0_3
DO  - 10.2991/978-94-6463-684-0_3
ID  - Kaneshita2025
ER  -