coq - Inductive 和 CoInductive 之间的唯一区别是对它们的使用（在 Coq 中）进行格式良好的检查吗？

Question

换种说法：如果我们要分别删除终止检查和使用归纳和共归纳数据类型的保护条件，那么归纳/共归纳和修复/共定之间是否会不再存在根本区别？

我所说的“根本差异”是指 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)