Memoryful Geometry of Interaction II: Recursion and Adequacy
Memoryful Geometry of Interaction II: Recursion and Adequacy
复制标题
交互的记忆几何 II：递归和充分性
DOI：
10.1145/2837614.2837672
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Naohiko Hoshino and Ichiro Hasuo
中科院分区：
文献类型：
--
作者：
Koko Muroya;Naohiko Hoshino and Ichiro Hasuo
最近，作者提出了一个一般性的相互作用记忆几何（mGoI）框架。它提供了一个健全的翻译，其实现流传感器（在低级别），其中后者的内部状态（称为记忆）被利用，以适应代数影响的Plotkin和电源的Ammada术语（在高级别）。翻译是合成的，因此是“指称的”，其中转换器是使用巴博萨的共代数分量演算的改编归纳合成的。在本文中，我们扩展了mGoI框架，并提供了一个系统的递归处理-编程语言的一个基本功能，但在我们以前的工作中缺少。具体来说，我们引入了两个新的不动点算子的共代数分量演算。这两种风格遵循GoI中以前关于递归的工作，被称为吉拉德风格和Mackie风格：前者显然展示了一些不错的域理论属性，而后者允许更简单的构造。它们的等价性建立在范畴（或追踪monoidal）抽象层次上，因此在代数效应的选择方面是通用的。我们的主要结果是一个充分性定理，我们的mGoI翻译，对Plotkin和电源的操作语义代数效果。
A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the internal states of the latter (called memories) are exploited for accommodating algebraic effects of Plotkin and Power. The translation is compositional, hence ``denotational,'' where transducers are inductively composed using an adaptation of Barbosa's coalgebraic component calculus. In the current paper we extend the mGoI framework and provide a systematic treatment of recursion---an essential feature of programming languages that was however missing in our previous work. Specifically, we introduce two new fixed-point operators in the coalgebraic component calculus. The two follow the previous work on recursion in GoI and are called Girard style and Mackie style: the former obviously exhibits some nice domain-theoretic properties, while the latter allows simpler construction. Their equivalence is established on the categorical (or, traced monoidal) level of abstraction, and is therefore generic with respect to the choice of algebraic effects. Our main result is an adequacy theorem of our mGoI translation, against Plotkin and Power's operational semantics for algebraic effects.