对称相互作用组合子的观测等价性和完全抽象性
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
摘要：
对称交互作用组合子是拉丰交互作用组合子的一个同样有表现力的变体。它们是确定性计算的图重写模型。我们定义了两个观测等价的概念，类似于范式和头范式等价的微积分。然后，我们证明了一个完整的抽象结果的两个等价。这是通过将网解释为康托空间的某些子集（称为大厦）来获得的，这些子集在代数演算理论中扮演着与Boehm树相同的角色。
英文摘要：
The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graph-rewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambda-calculus. Then, we prove a full abstraction result for each of the two equivalences. This is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambda-calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
