0
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Why is predd is propositionally equal to fun _ => 0? (Try proving it.) $\endgroup$ – Andrej Bauer Feb 13 at 14:04
  • $\begingroup$ @AndrejBauer sorry I means assuming function extensionality $\endgroup$ – molikto Feb 13 at 15:38
  • $\begingroup$ @AndrejBauer also see my comment below cstheory.stackexchange.com/questions/42371/… for some clearance.... $\endgroup$ – molikto Feb 13 at 15:47
  • $\begingroup$ Do you expect "definitional equality" to be checked by an algorithm? Is that what you mean when you say "constructively implemented"? What would it mean to implement "non-constructively"? $\endgroup$ – Andrej Bauer Feb 13 at 18:34
  • $\begingroup$ @AndrejBauer I am using "definitional equality" and judgmental equality" as the same thing now, so maybe I should say judgemental equality, but yes, I expect it be checked with an algorithm $\endgroup$ – molikto Feb 14 at 1:23
2
$\begingroup$

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.
$\endgroup$
  • $\begingroup$ Sorry it is kind of misleading mentioning _ => O which has nothing to do with the question. the question is if preddd and predd2 can be made definitionally equal by changing how definationaly equal is defined. it is actually quite like this question cstheory.stackexchange.com/questions/42333/… but I am lacking the background to fomulate the question that way initially. also the question aforementioned is in the context of untyped lambda calculus, which is not strongly normalizing $\endgroup$ – molikto Feb 13 at 15:42
  • $\begingroup$ @molikto I edited. Is it clearer? $\endgroup$ – xavierm02 Feb 14 at 15:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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