焦点下计算的对偶性
The duality of computation under focus
摘要：
我们回顾了抽象机（按名称或按值调用）之间的密切关系，演算（扩展与Felleisen的C）和微积分，重新介绍的方式Curien-Herbelin的语法工具包表示的对偶计算。我们使用这个工具包提供一个术语语言的LK（与合取，析取，否定）的介绍，并转录削减消除（非融合）重写。这里的一个关键口号，可能是第一次出现在印刷品上，是交换割消规则是显式的替代传播规则。然后，我们描述了焦点证明搜索纪律（在经典的设置），并缩小语言和重写规则的合流演算（第二作者的焦点系统L的变体）。然后，我们定义了一个游戏的模式和counterpatterns，导致我们的一个完全集中的finitary语法的经典逻辑的合成演示，提供了一个商（集中）的证明，抽象出的顺序分解的负连接词。
英文摘要：
We review the close relationship between abstract machines for (call-by-name or call-by-value) lambda-calculi (extended with Felleisen's C) and sequent calculus, reintroducing on the way Curien-Herbelin's syntactic kit expressing the duality of computation. We use this kit to provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and to transcribe cut elimination as (non confluent) rewriting. A key slogan here, which may appear here in print for the first time, is that commutative cut elimination rules are explicit substitution propagation rules. We then describe the focalised proof search discipline (in the classical setting), and narrow down the language and the rewriting rules to a confluent calculus (a variant of the second author's focalising system L). We then define a game of patterns and counterpatterns, leading us to a fully focalised finitary syntax for a synthetic presentation of classical logic, that provides a quotient on (focalised) proofs, abstracting out the order of decomposition of negative connectives.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
