Cuts for circular proofs: semantics and cut-elimination
Cuts for circular proofs: semantics and cut-elimination
复制标题
循环证明的剪切：语义和剪切消除
DOI：
10.4230/lipics.csl.2013.248
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
L. Santocanale
中科院分区：
文献类型：
--
作者：
J. Fortier;L. Santocanale
其中一位作者在[Santocanale，FoSSaCS，2002]中介绍了一种循环证明演算，用于研究以下范畴运算的可计算性：有限乘积，有限余积，初始代数，最终余代数。提出的演算[Santocanale，FoSSaCS，2002]是无切割的;即使对于可证明性来说是合理且完整的，它也缺乏证明语义的一个重要属性，即相对完整性预期的分类模型类（在[Santocanale，ITA，2002]中称为多双完全分类）。
在本文中，我们解决了这个问题，增加了切割规则的演算，并相应地修改语法约束，确保可靠的证明。增强的证明系统完全表示了规范模型（一个自由的μ-双完全范畴）的箭头。我们还描述了削减消除过程作为一个模型的计算所产生的上述分类操作。该过程构造了一个无割证明树，可能有无限的分支出一个有限的循环证明与削减。
One of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]).
In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.
Coq 中核心递归函数的归纳和共归纳成分
影响因子：
--
作者：
Bertot Y
通讯作者：
Bertot Y