抽象聚焦的可实现性语义的形式化

我们提出了一种配备证明项的抽象聚焦相继式演算：遵循 Zeilberger 工作的传统，逻辑连接词及其引入规则作为系统的参数留待指定，从而将聚焦的同步与异步阶段折叠为宏规则。我们更进一步将用新假设扩展假设上下文的操作也作为参数，这使得我们能够同时涵盖经典与直觉的聚焦相继式演算。随后，我们基于 Munch-Maccagnoni 针对经典聚焦相继式演算的正交性模型，定义了该系统的（证明的）可实现性语义，但此刻运作于上述更高抽象层次。我们在该层次证明了充分性引理（Adequacy Lemma），即若一个项具有类型 A，则其在模型中的指称位于 A 的（集合论）解释中。这揭示了如下事实：当取集合的正交时涉及的全程量化，在语义中反映了 Zeilberger 在异步阶段宏规则中的全程量化。该系统及其语义均在 Coq 中形式化。