5

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).$$

dkt
  • 51
  • 2
  • 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 May 09 '21 at 16:33
  • 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 May 09 '21 at 18:26
  • The paper https://arxiv.org/abs/1610.01213 seems relevant – dkt May 09 '21 at 18:51
  • 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 May 10 '21 at 06:43
  • The paper you linked to is not relevant for function extensionality. – Andrej Bauer May 10 '21 at 06:44
  • 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 May 10 '21 at 06:55
  • 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 May 10 '21 at 06:58

1 Answers1

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

Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165