AI 中文总结
该研究对比了slmu、lmmt、Xs三种经典逻辑演算的CBN、CBV归约及策略，定义了演算间的映射与解释，明确了不同演算间归约概念的对应关系及编码的局限性。
AI 中文摘要
我们为对称lmu（slmu）、lmmt及带隐式替换的X（Xs）演算定义了按名调用（CBN）、按值调用（CBV）归约及归约策略。通过定义从slmu到lmmt的单一解释，该解释尊重正规归约，且slmu中的CBN、CBV归约对应lmmt中的同类归约，我们确立了这些概念间的紧密关联；对于策略，我们将证明类似但较弱的结果。我们还定义了从lmmt到Xs的单一映射，表明其同样尊重上述三种归约概念。随后，我们研究Xs到lmmt的自然编码，发现仅完全归约得到尊重，而归约步骤是对替换建模所必需的，因此无法尊重CBN和CBV策略。最后，我们结合上述工作，定义从slmu到Xs的解释，证明其尊重CBN和CBV归约。该结果表明Xs与lmmt是相似但不同的演算，且slmu的特性使其任何编码都无法完全尊重上述策略。
英文摘要
We define call-by-name and call-by-value reduction and reduction strategies for the calculi slmu (symmetric lmu), lmmt, and Xs (X with implicit substitution). We establish a strong relation between these notions through defining a single interpretation from slmu to lmmt that respects normal reduction, as well as the call-by-name and call-by-value reduction in slmu within the their counterpart in lmmt; for the strategies, we will show similar, but weaker results. We also define a single mapping from lmmt to Xs, and show that this also respects all three notions. We then continue with studying the natural encoding of Xs into lmmt, and show that only full reduction is respected, but that reduction steps are needed to model substitution, so the CBN and CBV strategies cannot be respected. We conclude with studying the combination of our efforts and define an interpretation of slmu into Xs, and show that CBN and CBV reduction are respected. This result underlines that Xs and lmmt are similar, but different calculi, and that the nature of slmu makes that any encoding into either can never fully respect the strategies.
