First-class Environments in Categorical Combinators
First-class Environments in Categorical Combinators
复制标题
分类组合器中的一流环境
DOI：
10.1142/9789813234079_0003
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
S. Nishizaki
中科院分区：
文献类型：
--
作者：
Hiroki Joko;S. Nishizaki
范畴组合逻辑CCLβηSP是由Pierre-Louis Curien提出的基于范畴闭范畴的组合逻辑。组合逻辑被用于lambda演算的建模，并给出了一个抽象机的设计，分类抽象机（CAM）。第一类环境是编程语言中的一种机制，它使我们能够操纵环境，即变量到绑定值的映射。我们对一类环境下的lambda演算进行了多年的研究，本文刻画了一类环境存在于范畴组合逻辑中，给出了一类环境下的简单类型lambda演算到范畴组合逻辑的翻译.我们表明，翻译尊重打字和减少。
The categorical combinatory logic CCLβηSP is a combinatory logic motivated by the cartesian closed category, proposed by Pierre-Louis Curien. The combinatory logic is used for modeling of the lambda calculus and gives a design of an abstract machine, the Categorical Abstract Machine (CAM). The first-class environment is a mechanism in programming languages which enables us to manipulate an environment, that is, a mapping of variables to bound values. We have studied the lambda calculus with first-class environments for several years.In this paper, we depict that the first-class environment indwells in the categorical combinatory logic, giving the translation of the simply-typed lambda calculus with first-class environments into the categorical combinatory logic. We show the translation respects the typing and the reduction.