Untyped lambda calculus with functionally referable environments
Untyped lambda calculus with functionally referable environments
复制标题
具有功能可引用环境的无类型 lambda 演算
DOI：
10.1145/3457784.3457798
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Kasuga Ryotaro
中科院分区：
文献类型：
--
作者：
Nishizaki Shin-ya;Kasuga Ryotaro
环境是程序执行期间变量和它们的限定值之间的关系，是程序语义中的一个概念。一级环境是一种机制，它允许将环境视为数据，如整数值或布尔值，并可以作为参数传递给函数或作为返回值接收。环境演算是西崎提出的一种形式化计算系统，是一种扩展了一级环境机制的Lambda演算。环境的表述是基于Curien等人的明确替代，他们将环境视为一种替代。环境演算或归约的操作语义基于lambda-sigma演算的归约。在演算中，一级环境有两个构造：一个是将当前环境具体化的标识环境，即将元级环境转换为对象级数据；另一个是环境组成，以反映对象级环境数据，即将对象级环境数据传回元级环境。在本文中，我们提出了一种新的界面，它具有一流的环境，一个功能可引用的环境，而不是环境的组成。如果将对象级环境数据作为函数应用程序的参数提供，则函数反射会将环境带回到元级，并使lambda项在该环境下可计算。使用功能可参照环境，可以将环境组成与功能应用统一。我们定义了具有函数可引用环境的非类型Lambda演算：我们给出了演算的语法及其归约。然后，通过将环境演算转化为记录演算，给出了约简的语义。我们证明了翻译语义的可靠性。最后，我们讨论了评估策略，特别是按价值减少的评估策略。
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.
登录
查看更多内容
DOI：
10.1007/978-3-642-53932-9_23
发表时间：
2013
期刊：
--
影响因子：
--
作者：
S. Nishizaki
通讯作者：
S. Nishizaki
DOI：
10.1023/a:1010010314528
发表时间：
2000
期刊：
Higher-Order and Symbolic Computation
影响因子：
--
作者：
S. Nishizaki
通讯作者：
S. Nishizaki
具有一流延续和环境的非类型化值调用演算
DOI：
10.1142/9789813279674_0008
发表时间：
2018
期刊：
Theory and Practice of Computation
影响因子：
--
作者：
Yuta Aoyagi;S. Nishizaki
通讯作者：
S. Nishizaki
用于按值调用演算的简单类型系统，具有一流的延续和环境
DOI：
10.1201/9780429261350-13
发表时间：
2019
期刊：
Theory and Practice of Computation
影响因子：
--
作者：
S. Nishizaki
通讯作者：
S. Nishizaki
具有一流环境的简单类型 Lambda 演算
DOI：
10.2977/prims/1195164948
发表时间：
1994
影响因子：
1.2
作者：
S. Nishizaki
通讯作者：
S. Nishizaki