Definitional equality of recursive function definition by "infinite unfolding"

Question

The context is checking definitional equality in dependent type theory implementations.

Consider in Coq

Fixpoint predd(a: nat): nat := 
  match a with
  | O => O
  | S b => predd(b)
  end.

Fixpoint preddd(a: nat): nat := 
  match a with
  | O => O
  | S b => match b with | O => O | S c => preddd(c) end
  end.


Fixpoint predd2(a: nat): nat := 
  match a with
  | O => O
  | S b => preddd(b)
  end.

So predd is a function that recursively call itself and return O eventually. it is popositionaly equal to _ => O

preddd is the predd unfold once inside.

predd2 is just predd but calls preddd inside.

predd2 and preddd is not definitionaly equal in Coq. But can we have another definitional equality for recursive functions?

I have an idea of definitional equality of recursive functions, such that if the infinite unfolding of recursive definition is equal, then the two value is equal. such "infinite unfolding" seems can be made precise by requiring the finite unfoldings of values always have a similarity relation.

So, is there a sound definition of "definitional equality of recursive functions by infinite expansions"?

Can this be constructively implemented?

Answer 1

Your predd2 is not a fixpoint; you could replace the Fixpoint by Definition. And the fact that they are not convertible is due to the lack of eta-conversion for inductive types in Coq.

The reason for this is that we want the conversion to be decidable, and it's already hard to decide beta-eta-conversion in the simply typed case (see Deciding equivalence with sums and the empty type by Gabriel Scherer).

---

You can more or less check that "a is convertible to b" by using the following notation:

Notation "n ~ m" := (eq_refl : n = m) (at level 70, no associativity).

(It has the expected behaviour on +:

Check fun n => 0 + n ~ n.
Fail Check fun n => n + 0 ~ n.

)

And you can check that there is no eta-conversion for booleans, for natural numbers, or even for the unit type:

Fail Check fun x : bool => if x then tt else tt ~ tt.
Fail Check fun x : nat => match x with | 0 => tt | S _ => tt end ~ tt.
Fail Check fun x : unit => match x with tt => tt end ~ tt.

(Those are specific cases of the eta conversion for those inductive types, but since they already fail, it still shows that the full eta conversion can't be included in the conversion)

Now, going back to your specific example (with the names changed). I use the names:

• $f_i$ for the recursive function that returns $0$ immediately if its argument $n$ is between $0$ and $i-1$, and otherwise recursively calls its self on $n-i$. $f_1$ is your predd and $f_2$ is your preddd.

• $\text{eta}\_\text{fun}\_f_i$ is the eta-expansion (as a function) of $f_i$.

• $\text{eta}\_\text{fun}\_\text{eta}\_\text{nat}\_f_i$ is the result of eta-expanding the body (with the eta-expansion of natural numbers) of $\text{eta}\_\text{fun}\_f_i$.

• $g_i$ is the function that returns $0$ immediately if its argument $n$ is $0$, and otherwise returns $f_i(n-1)$.

We have $g_1\equiv \text{eta}\_f_1 \not \equiv \text{eta}\_\text{fun}\_\text{eta}\_\text{nat}\_f_2 \equiv f_1$, which shows that the problem is indeed the lack of eta-conversion for natural numbers.

We have $g_1\equiv \text{eta}\_f_1 \not \equiv \text{eta}\_\text{fun}\_\text{eta}\_\text{nat}\_f_2 \not\equiv f_1$. The first $\not\equiv$ is still due to the same reason. I think the second one is more about unfolding of fixpoints.

Here is a Coq script that supports what I said above:

Fixpoint f1 n := (* predd *)
  match n with
  | O => O
  | S n' => f1 n'
  end
.

Definition eta_fun_f1 n :=
  f1 n
.

Definition eta_fun_eta_nat_f1 n :=
  match n with
  | 0 => f1 0
  | S n' => f1 (S n')
  end
.

Definition g1 n :=
  match n with
  | 0 => 0
  | S n' => f1 n'
  end
.

Check f1 ~ eta_fun_f1.
Fail Check eta_fun_f1 ~ eta_fun_eta_nat_f1.
Check eta_fun_eta_nat_f1 ~ g1.

Fixpoint f2 n := (* preddd *)
  match n with
  | 0 => 0
  | S n' =>
    match n' with
    | 0 => 0
    | S n'' => f2 n''
    end
  end
.

Definition eta_fun_f2 n :=
  f2 n
.

Definition eta_fun_eta_nat_f2 n :=
  match n with
  | 0 => f2 0
  | S n' => f2 (S n')
  end
.

Definition g2 n := (* predd2 *)
  match n with
  | 0 => 0
  | S n' => f2 n'
  end
.

Check f2 ~ eta_fun_f2.
Fail Check eta_fun_f2 ~ eta_fun_eta_nat_f2.
Fail Check eta_fun_eta_nat_f2 ~ g2.