<p>Yes, you can. However:</p>
<p>The complexity issue is bad -- testing whether two <span class="math-container">$2^n \to 2$</span> functions are equal is NP-complete, and to make it bearable in practice would require some clever integration with a SAT solver or BDD engine in the implementation of definitional equality.</p>
<p>Moreover, you can potentially defeat such smartness by asking questions about Boolean functions which are free variables. For example, for any <span class="math-container">$f : 2 \to 2$</span>, it is extensionally the case that <span class="math-container">$f(f(f(x))) = f(x)$</span>, which you establish by exhaustive enumeration.</p>
<p>You can find some links to papers with algorithms for coproduct in this link:</p>
<p><a href="https://cstheory.stackexchange.com/questions/10608/programming-languages-with-canonical-functions">Programming languages with canonical functions</a></p>

CC BY-SA 4.0
2021-05-09T19:40:48.813Z
2021-05-09T19:48:44.770Z
2021-05-09T19:48:44.770Z
Neel Krishnaswami
<p>Denote by <span class="math-container">$a$</span> and <span class="math-container">$b$</span> the canonical terms of <span class="math-container">$\mathbf{2}$</span>.</p>
<p>For any map <span class="math-container">$f:\mathbf{2}\to \mathcal{U}$</span> we have the eliminator<span class="math-container">$$\mathrm{ind}_{\mathbf{2}}(f) : \big(f(a) \times f(b)\big) \to \prod_{x:\mathbf{2}} f(x).$$</span></p>
<p>Can we add the rule that for any <span class="math-container">$f:\mathbf{2}\to \mathcal{U}$</span> and any <span class="math-container">$g:\prod_{x:\mathbf{2}} f(x)$</span> we have a definitional equality <span class="math-container">$$g=\mathrm{ind}_{\mathbf{2}}(f)(g(a)\times g(b))$$</span>and have decidable equality checking and decidable type checking?</p>
<p>So for example take <span class="math-container">$f=\lambda x:\mathbf{2}.\mathbf{2}$</span>. Then this rule would imply a definitional equality <span class="math-container">$$\lambda x:\mathbf{2}.x=\mathrm{ind}_2(f)(b\times a)\circ \mathrm{ind}_2(f)(b\times a).$$</span></p>

CC BY-SA 4.0
2021-05-09T16:33:29.943Z
What do you mean by "can"?  Are you asking whether postulating such judgemental equalities breaks decidability of equality checking? How precisely would you state the rules?
Andrej Bauer
CC BY-SA 4.0
2021-05-09T18:26:21.570Z
Ok, thanks for clearing up what you are wondering. What is $\mathrm{ind}$? The formula you are suggesting does not seem to have the form of function extensionality.  Also, you cannot do it by "ranging over canonical terms", that's not how inference rules in type theory work.
Andrej Bauer
CC BY-SA 4.0
2021-05-09T18:51:10.087Z
The paper https://arxiv.org/abs/1610.01213 seems relevant
dkt
CC BY-SA 4.0
2021-05-10T06:43:36.887Z
The way you use $\mathrm{ind}$ does not make any sense, and if I had to guess what you were trying to get to, I would say you're asking about the $\eta$-rule for funcitons, not function extensionality. This question needs to be clarified, or moved to cs.stackexchange.com (and probably both).
Andrej Bauer
CC BY-SA 4.0
2021-05-10T06:44:14.427Z
The paper you linked to is *not* relevant for function extensionality.
Andrej Bauer
CC BY-SA 4.0
2021-05-10T06:55:52.013Z
Thanks. I can see what you're after now, but it would really help if you actually wrote down what $\mathrm{ind}_2$ is in your question. As things stand, I still have to *guess* from your comment what the type of $\mathrm{ind}_2$ is, and what equations you might think govern it. Also, did you really mean $p$ and $q$ to map from $\mathbb{N}$ to $\mathbb{N}$?
Andrej Bauer
CC BY-SA 4.0
2021-05-10T06:58:52.393Z
Ok, thanks for clearing that up. Would you mind editing your question and adding some of these details? I think that would help any future readers.
Andrej Bauer
<type-theory>
Definitional function extensionality for functions out of $\mathbf{2}$
dkt
# Definitional function extensionality for functions out of $\mathbf{2}$

(Asked by: username_0 on 2021-05-09)

Denote by $a$ and $b$ the canonical terms of $\mathbf{2}$.

For any map $f:\mathbf{2}\to \mathcal{U}$ we have the eliminator$$\mathrm{ind}\_{\mathbf{2}}(f) : \big(f(a) \times f(b)\big) \to \prod\_{x:\mathbf{2}} f(x).$$

Can we add the rule that for any $f:\mathbf{2}\to \mathcal{U}$ and any $g:\prod\_{x:\mathbf{2}} f(x)$ we have a definitional equality $$g=\mathrm{ind}\_{\mathbf{2}}(f)(g(a)\times g(b))$$and have decidable equality checking and decidable type checking?

So for example take $f=\lambda x:\mathbf{2}.\mathbf{2}$. Then this rule would imply a definitional equality $$\lambda x:\mathbf{2}.x=\mathrm{ind}\_2(f)(b\times a)\circ \mathrm{ind}\_2(f)(b\times a).$$

**Tags:** type-theory

> **Comments:**
> **username_1**: What do you mean by "can"?  Are you asking whether postulating such judgemental equalities breaks decidability of equality checking? How precisely would you state the rules?  
> **username_1**: Ok, thanks for clearing up what you are wondering. What is $\mathrm{ind}$? The formula you are suggesting does not seem to have the form of function extensionality.  Also, you cannot do it by "ranging over canonical terms", that's not how inference rules in type theory work.  
> **username_0**: The paper https://arxiv.org/abs/1610.01213 seems relevant  
> **username_1**: The way you use $\mathrm{ind}$ does not make any sense, and if I had to guess what you were trying to get to, I would say you're asking about the $\eta$-rule for funcitons, not function extensionality. This question needs to be clarified, or moved to cs.stackexchange.com (and probably both).  
> **username_1**: The paper you linked to is *not* relevant for function extensionality.  
> **username_1**: Thanks. I can see what you're after now, but it would really help if you actually wrote down what $\mathrm{ind}_2$ is in your question. As things stand, I still have to *guess* from your comment what the type of $\mathrm{ind}_2$ is, and what equations you might think govern it. Also, did you really mean $p$ and $q$ to map from $\mathbb{N}$ to $\mathbb{N}$?  
> **username_1**: Ok, thanks for clearing that up. Would you mind editing your question and adding some of these details? I think that would help any future readers.  

---

## 1 answers

### Answer by username_2 on 2021-05-09. Score: 2

Yes, you can. However:

The complexity issue is bad -- testing whether two $2^n \to 2$ functions are equal is NP-complete, and to make it bearable in practice would require some clever integration with a SAT solver or BDD engine in the implementation of definitional equality.

Moreover, you can potentially defeat such smartness by asking questions about Boolean functions which are free variables. For example, for any $f : 2 \to 2$, it is extensionally the case that $f(f(f(x))) = f(x)$, which you establish by exhaustive enumeration.

You can find some links to papers with algorithms for coproduct in this link:

[Programming languages with canonical functions](https://cstheory.stackexchange.com/questions/10608/programming-languages-with-canonical-functions)


---

