论文标题
大语义的健全条件
Soundness conditions for big-step semantics
论文作者
论文摘要
我们提出了一种通用的证明技术，以证明谓词是声音，也就是说，在大型语义方面可以防止卡住的计算。该结果看起来可能令人惊讶，因为在大型语义上，非终止和卡住计算之间没有差异，因此甚至无法表达健全性。关键想法是定义构造，得出给定的任意大型语义的扩展版本，在该语义上有明确的差异。在元理论中利用了扩展的语义，特别是证明证明技术有效的必要条件。但是，在使用证明技术时，它们仍然透明，因为它仅在原始规则上检查三个条件，正如我们通过几个示例所说明的那样。
We propose a general proof technique to show that a predicate is sound, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising, since in big-step semantics there is no difference between non-terminating and stuck computations, hence soundness cannot even be expressed. The key idea is to define constructions yielding an extended version of a given arbitrary big-step semantics, where the difference is made explicit. The extended semantics are exploited in the meta-theory, notably they are necessary to show that the proof technique works. However, they remain transparent when using the proof technique, since it consists in checking three conditions on the original rules only, as we illustrate by several examples.
