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

<p>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).</p>

<hr>

<p>You can more or less check that "<code>a</code> is convertible to <code>b</code>" by using the following notation:</p>

<pre><code>Notation "n ~ m" := (eq_refl : n = m) (at level 70, no associativity).
</code></pre>

<p>(It has the expected behaviour on <code>+</code>:</p>

<pre><code>Check fun n =&gt; 0 + n ~ n.
Fail Check fun n =&gt; n + 0 ~ n.
</code></pre>

<p>)</p>

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

<pre><code>Fail Check fun x : bool =&gt; if x then tt else tt ~ tt.
Fail Check fun x : nat =&gt; match x with | 0 =&gt; tt | S _ =&gt; tt end ~ tt.
Fail Check fun x : unit =&gt; match x with tt =&gt; tt end ~ tt.
</code></pre>

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

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

<ul>
<li><p><span class="math-container">$f_i$</span> for the recursive function that returns <span class="math-container">$0$</span> immediately if its argument <span class="math-container">$n$</span> is between <span class="math-container">$0$</span> and <span class="math-container">$i-1$</span>, and otherwise recursively calls its self on <span class="math-container">$n-i$</span>. <span class="math-container">$f_1$</span> is your <code>predd</code> and <span class="math-container">$f_2$</span> is your <code>preddd</code>.</p></li>
<li><p><span class="math-container">$\text{eta}\_\text{fun}\_f_i$</span> is the eta-expansion (as a function) of <span class="math-container">$f_i$</span>.</p></li>
<li><p><span class="math-container">$\text{eta}\_\text{fun}\_\text{eta}\_\text{nat}\_f_i$</span> is the result of eta-expanding the body (with the eta-expansion of natural numbers) of <span class="math-container">$\text{eta}\_\text{fun}\_f_i$</span>.</p></li>
<li><p><span class="math-container">$g_i$</span> is the function that returns <span class="math-container">$0$</span> immediately if its argument <span class="math-container">$n$</span> is <span class="math-container">$0$</span>, and otherwise returns <span class="math-container">$f_i(n-1)$</span>.</p></li>
</ul>

<p>We have <span class="math-container">$g_1\equiv \text{eta}\_f_1 \not \equiv \text{eta}\_\text{fun}\_\text{eta}\_\text{nat}\_f_2 \equiv f_1$</span>, which shows that the problem is indeed the lack of eta-conversion for natural numbers.</p>

<p>We have <span class="math-container">$g_1\equiv \text{eta}\_f_1 \not \equiv \text{eta}\_\text{fun}\_\text{eta}\_\text{nat}\_f_2 \not\equiv f_1$</span>. The first <span class="math-container">$\not\equiv$</span> is still due to the same reason. I think the second one is more about unfolding of fixpoints.</p>

<p>Here is a Coq script that supports what I said above:</p>

<pre><code>Fixpoint f1 n := (* predd *)
  match n with
  | O =&gt; O
  | S n' =&gt; f1 n'
  end
.

Definition eta_fun_f1 n :=
  f1 n
.

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

Definition g1 n :=
  match n with
  | 0 =&gt; 0
  | S n' =&gt; 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 =&gt; 0
  | S n' =&gt;
    match n' with
    | 0 =&gt; 0
    | S n'' =&gt; f2 n''
    end
  end
.

Definition eta_fun_f2 n :=
  f2 n
.

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

Definition g2 n := (* predd2 *)
  match n with
  | 0 =&gt; 0
  | S n' =&gt; 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.
</code></pre>

CC BY-SA 4.0
2019-02-13T15:42:32.177Z
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 https://cstheory.stackexchange.com/questions/42333/is-it-possible-to-check-equality-of-equi-recursive-types-or-recursive-%CE%BB-terms?rq=1 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
molikto
CC BY-SA 4.0
2019-02-14T15:27:58.113Z
@molikto I edited. Is it clearer?
xavierm02
CC BY-SA 4.0
2019-02-13T14:11:24.887Z
2019-02-14T15:25:09.800Z
2019-02-14T15:25:09.800Z
xavierm02
<p>The context is checking definitional equality in dependent type theory implementations.</p>

<p>Consider in Coq</p>



<pre><code>Fixpoint predd(a: nat): nat := 
  match a with
  | O =&gt; O
  | S b =&gt; predd(b)
  end.

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


Fixpoint predd2(a: nat): nat := 
  match a with
  | O =&gt; O
  | S b =&gt; preddd(b)
  end.
</code></pre>

<p>So <code>predd</code> is a function that recursively call itself and return <code>O</code> eventually. it is popositionaly equal to <code>_ =&gt; O</code></p>

<p><code>preddd</code> is the <code>predd</code> unfold once inside.</p>

<p><code>predd2</code> is just <code>predd</code> but calls <code>preddd</code> inside.</p>

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

<p>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 <em>similarity relation</em>.</p>

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

<p>Can this be constructively implemented?</p>

CC BY-SA 4.0
2019-02-13T14:04:56.117Z
Why is `predd` is propositionally equal to `fun _ => 0`? (Try proving it.)
Andrej Bauer
CC BY-SA 4.0
2019-02-13T15:38:15.660Z
@AndrejBauer sorry I means assuming function extensionality
molikto
CC BY-SA 4.0
2019-02-13T15:47:59.883Z
@AndrejBauer also see my comment below https://cstheory.stackexchange.com/questions/42371/definitional-equality-of-recursive-function-definition-by-infinite-unfolding/42379#comment98423_42379 for some clearance....
molikto
CC BY-SA 4.0
2019-02-13T18:34:07.183Z
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"?
Andrej Bauer
CC BY-SA 4.0
2019-02-14T01:23:07.897Z
@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
molikto
CC BY-SA 4.0
2019-02-14T08:06:33.910Z
Checking equality of infinte trees can be problematic (which is what your unfoldings are). If you know something extra about the trees (for instance, if they're [regular](https://en.wikipedia.org/wiki/Regular_tree_grammar)) then there might be an algorithm. In the present case, after you've figured out what you mean by "infinite unfolding", it looks like you don't stand a chance. The trees will be very complex.
Andrej Bauer
<type-theory><dependent-type><recursion>
Definitional equality of recursive function definition by "infinite unfolding"
molikto
# Definitional equality of recursive function definition by "infinite unfolding"

(Asked by: username_0 on 2019-02-13)

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?

**Tags:** type-theory, dependent-type, recursion

> **Comments:**
> **username_1**: Why is `predd` is propositionally equal to `fun _ => 0`? (Try proving it.)  
> **username_0**: @AndrejBauer sorry I means assuming function extensionality  
> **username_0**: @AndrejBauer also see my comment below https://cstheory.stackexchange.com/questions/42371/definitional-equality-of-recursive-function-definition-by-infinite-unfolding/42379#comment98423_42379 for some clearance....  
> **username_1**: 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"?  
> **username_0**: @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  
> **username_1**: Checking equality of infinte trees can be problematic (which is what your unfoldings are). If you know something extra about the trees (for instance, if they're [regular](https://en.wikipedia.org/wiki/Regular_tree_grammar)) then there might be an algorithm. In the present case, after you've figured out what you mean by "infinite unfolding", it looks like you don't stand a chance. The trees will be very complex.  

---

## 1 answers

### Answer by username_2 on 2019-02-13. Score: 2

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.

> **Comments:**
> **username_0**: 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 https://cstheory.stackexchange.com/questions/42333/is-it-possible-to-check-equality-of-equi-recursive-types-or-recursive-%CE%BB-terms?rq=1 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  
> **username_2**: @username_0 I edited. Is it clearer?  

---

