5
$\begingroup$

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

$\endgroup$
7
  • $\begingroup$ 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? $\endgroup$ May 9 at 16:33
  • $\begingroup$ 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. $\endgroup$ May 9 at 18:26
  • $\begingroup$ The paper arxiv.org/abs/1610.01213 seems relevant $\endgroup$
    – dkt
    May 9 at 18:51
  • $\begingroup$ 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). $\endgroup$ May 10 at 6:43
  • $\begingroup$ The paper you linked to is not relevant for function extensionality. $\endgroup$ May 10 at 6:44
2
$\begingroup$

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

$\endgroup$
0

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.