coq - Inductive 和 CoInduction 之间的唯一区别是对其使用的格式良好性检查(在 Coq 中)吗？

Question

换句话来说:如果我们分别删除归纳和共归纳数据类型使用的终止检查和防护条件，那么归纳/共归纳和修复/cofix之间是否不再有根本区别？

我所说的“根本差异”是指 Coq 核心演算的差异，而不是语法和证明搜索等方面的差异。

这似乎最终归结为有关构造微积分的问题。

注意:我知道一个定理证明者跳过了递归/核心递归的终止检查/防护性可以证明False - 所以，如果有帮助，请将此视为关于非总体编程的问题，而不是而不是证明。

Answer 1

fix 和 cofix 的终止检查是其格式良好规则的一部分。如果我们忽略这一点，这些构造的另一个重要区别特征在于计算规则。

• fix 仅当其递减参数是构造函数时才减少

• cofix 仅在析构函数(match 或原始投影)下减少

(* stuck *)
(fix f x {struct x} := body f x)

(* not stuck *)
(fix f x {struct x} := body f x) (S y)
=
body (fix f x := body f x) (S y)


(* stuck *)
(cofix g x := body g x)

(* not stuck *)
match (cofix g x := body g x) with _ => _ end
= match body (cofix g x := body g x) x with _ => _ end

这些特殊的规则是为了确保终止。如果您不关心这一点，并允许 fix 和 cofix 在任何上下文中展开，那么它们的行为与固定点组合器相同:

(fix f x := body f x)
=
(fun x => body (fix f x := body f x) x)

(cofix g x := body g x)
=
(fun x => body (cofix g x := body g x) x)