Untyped lambda calculus with functionally referable environments
| Autor: | Shin-ya Nishizaki, Ryotaro Kasuga |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Soundness
Functional programming Semantics (computer science) Programming language Computer science Substitution (algebra) Function application computer.software_genre Operational semantics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Explicit substitution TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Lambda calculus computer computer.programming_language |
| Zdroj: | ICSCA |
| DOI: | 10.1145/3457784.3457798 |
| Popis: | The environment is the relationship between variables and their bound values during program execution and is a notion in program semantics. A first-class environment is a mechanism that allows the environment to be treated like data, such as integer values or Boolean values, and can be passed to a function as an argument or received as a return value. The environment calculus is a formal computational system proposed by Nishizaki and is a lambda calculus that extends the first-class environment mechanism. The formulation of the environment was based on explicit substitution by Curien et al., who viewed the environment as a substitution. The operational semantics of the environmental calculus, or the reduction, is based on the reduction of the lambda-sigma calculus. In the calculus, there are two constructs for first-class environments: one is the identity environment to reify the current environment, that is, to transfer a meta-level environment to object-level data; the other is the environment composition to reflect the object-level environment data, that is, to transfer object-level environment data back to a meta-level environment. In this paper, instead of the environment composition, we propose a new interface with a first-class environment, a functionally referable environment. If object-level environment data is given as an argument for a function application, the functional reflection brings the environment back to the meta-level and makes the lambda term evaluable under that environment. Using the functionally referable environment, one can unify the environment composition with the function application. We define the untyped lambda calculus with functionally referable environments: we give the syntax of the calculus and its reduction. Then we provide the semantics for the reduction using a translation of the environment calculus into the record calculus. We prove the soundness of the translation semantics. Finally, we discuss the evaluation strategy, especially the call-by-value reduction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|