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

Question

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

\n

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

\n

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

\n

注意：我知道一个定理证明者跳过了递归/核心递归的终止检查/防护可以证明False\xe2\x80\x93so，如果有帮助，请将其视为有关非完全编程的问题而不是证明。

\n

Answer 1

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

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

• cofixmatch仅在析构函数（或原始投影）下减少

(* 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)