一个大步语义学的元理论
A meta-theory for big-step semantics
摘要：
众所周知，大步语义无法区分卡住和非终止计算。这是一个很强的限制，因为它使得推理涉及无限计算的属性变得非常困难，例如类型可靠性，甚至无法表达。我们表明，这个问题只是显而易见的：卡住和发散计算之间的区别是隐含在任何大步语义，它只需要被发现。为了实现这一目标，我们开发了一个系统的研究大步语义：我们引入了一个抽象的定义是什么一个大步语义，我们定义了一个概念的计算通过形式化的评估算法隐式与任何大步语义，我们展示了如何规范地扩展一个大步语义，以避免卡住和发散计算。在这些概念的基础上，我们描述了一个通用的证明技术，以表明一个谓词是健全的，也就是说，它可以防止卡住计算，相对于一个大步语义。需要检查与谓词和语义相关的三个属性，如果它们成立，则谓词是合理的。扩展的语义对于建立这个元逻辑结果是必不可少的，但是对于用户来说是无关紧要的，用户只需要证明初始大步语义的三个属性。最后，我们通过几个例子说明了该技术，表明它也适用于主题还原不成立的情况下，因此不能使用标准的小步语义技术。
英文摘要：
It is well-known that big-step semantics is not able to distinguish stuck and non-terminating computations. This is a strong limitation as it makes very difficult to reason about properties involving infinite computations, such as type soundness, which cannot even be expressed. We show that this issue is only apparent: the distinction between stuck and diverging computations is implicit in any big-step semantics and it just needs to be uncovered. To achieve this goal, we develop a systematic study of big-step semantics: we introduce an abstract definition of what a big-step semantics is, we define a notion of computation by formalising the evaluation algorithm implicitly associated with any big-step semantics, and we show how to canonically extend a big-step semantics to characterise stuck and diverging computations. Building on these notions, we describe a general proof technique to show that a predicate is sound, that is, it prevents stuck computation, with respect to a big-step semantics. One needs to check three properties relating the predicate and the semantics and, if they hold, the predicate is sound. The extended semantics are essential to establish this meta-logical result, but are of no concerns to the user, who only needs to prove the three properties of the initial big-step semantics. Finally, we illustrate the technique by several examples, showing that it is applicable also in cases where subject reduction does not hold, hence the standard technique for small-step semantics cannot be used.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
