3
$\begingroup$

In Coq, there are two restrictions on fixpoints to retain normalization:

  1. Recursive calls can only be done on structurally smaller arguments, enforced by a guard condition during type checking; and
  2. Reduction occurs only when applied to a constructor in the recursive argument position (also called guarded recursion, apparently).

Evidently, without #1 you could prove an inconsistency and break normalization, e.g. fix f (n: nat) (A: Type): A := f (S n) A, while without #2 you could unfold a fixpoint indefinitely (reducing under lambdas and such). Does removing only #2 also break consistency, or merely normalization? I'm wondering if you could have a consistent type theory with an equality rule like

$$ \Gamma, f: A \vdash e: A \\ \rule{19em}{1px}. \\ \Gamma \vdash (\mathrm{fix} \: f : A := e) \equiv e[f/(\mathrm{fix} \: f : A := e)] : A $$

$\endgroup$

1 Answer 1

5
$\begingroup$

This is consistent.

First, this equality holds propositionally by eta-expansion of the constructor. Thus, if your type theory had equality reflection, it would also hold definitionally. Since Extensional Type Theory is consistent, this rule also is.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.