一个经典术语演算的强双模拟
摘要：$lambdamu$-演算与证明网络的翻译中，$simeq\_sigma$-等价关系捕捉了那些次要细节，这是在直观主义（由Regnier提出）和经典主义（由Laurent提出）情况下。本文的目的是揭示Laurent为Parigot的$lambdamu$-演算提出的$simeq\_sigma$-等价关系背后的强同步关系。这是通过引入一个关系$simeq$来实现的，该关系定义在我们称之为$Lambda M$的$lambdamu$-演算的修订表达式上。我们首先找出Laurent关于$lambdamu$-项上的$simeq\_sigma$-等价关系无法成为强同步关系的原因。受到Laurent的“极化证明网络”的启发，我们区分了项上的乘法和指数规约步骤。其次，我们丰富了$lambdamu$的语法，以便追踪指数运算。这些技术要素为经典情况下的强同步关系铺平了道路。我们引入了一个名为$Lambda M$的演算和一个关系$simeq$，我们证明了它是与$Lambda M$中的规约对称的强同步关系，即两个$simeq$-等价的项具有完全相同的规约语义。这一结果在$lambda$-演算的Regnier的$simeq\_sigma$-等价关系以及$lambdamu$中的Laurent的$simeq\_sigma$-等价关系都不成立。尽管$simeq$是在丰富的语法上定义的，因此并不严格包含在Laurent的$simeq\_sigma$中，但我们展示了它可以被看作是其的一种限制。
作者：Eduardo Bonelli, Delia Kesner and Andr''es Viso
论文ID：2101.05754
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-19