Is the only difference between Inductive and CoInductive the well-formedness checks on their uses (in Coq)?

Question

To phrase the question differently: if we were to remove termination-checking and the guardedness condition on uses of inductive and coinductive data types, respectively, would there cease to be a fundamental difference between inductive/coinductive and fix/cofix?

By "fundamental difference" I mean a difference in the core calculus of Coq–not differences in things like syntax and proof search.

This seems to ultimately boil down to a question about the Calculus of Constructions.

Note: I know a theorem prover that skipped termination-checking/guardedness of recursion/corecursion could prove False–so, if it helps, please take this as a question about non-total programming rather than proving.

Answer 1

The termination check for fix and cofix is part of their well-formedness rules. If we ignore that, the other important distinguishing feature of those constructs is in the computation rules.

• fix only reduces if its decreasing argument is a constructor

• cofix only reduces when under a destructor (match or a primitive projection)

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

Those peculiar rules are that way in order to ensure termination. If you do not care about that, and allow fix and cofix to unfold in any context, then they behave identically as a fixpoint combinator:

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