对称交互组合子中的观察等价与完全抽象
计算机科学中的逻辑
2015-07-01 v3 离散数学
摘要
对称交互组合子是Lafont交互组合子的一种具有同等表达能力的变体。它们是一种确定性计算的图重写模型。我们为其定义了两种观察等价的概念，类似于λ演算中的范式等价和头范式等价。然后，我们证明了这两种等价各自对应的完全抽象结果。这是通过将网解释为康托尔空间的某些子集（称为edifices）来实现的，这些子集在λ演算理论中扮演着与Boehm树类似的角色。
引用
@article{arxiv.0906.0380,
title = {Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators},
author = {Damiano Mazza},
journal= {arXiv preprint arXiv:0906.0380},
year = {2015}
}