Proof Relevant Corecursive Resolution
Proof Relevant Corecursive Resolution
复制标题
证明相关的核心递归解析
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Andrew Pond
中科院分区：
文献类型：
--
作者：
Peng Fu;Ekaterina Komendantskaya;Tom Schrijvers;Andrew Pond
解决问题是函数式语言中逻辑编程和类型类上下文缩减的基础。归结的终止派生具有明确的归纳意义，而一些非终止的派生可以被共同归纳地理解。周期检测是一种流行的方法，可以捕获此类派生的一小部分。我们证明了循环检测实际上是一种受限形式的协归纳证明，其中形成循环的原子式扮演了协归纳假设的角色。
Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have well-defined inductive meaning, whereas some non-terminating derivations can be understood coinductively. Cycle detection is a popular method to capture a small subset of such derivations. We show that in fact cycle detection is a restricted form of coinductive proof, in which the atomic formula forming the cycle plays the role of coinductive hypothesis.