4
$\begingroup$

There is a slick definition of categories (as a record type with eta-equality) such that taking the opposite category twice results in the original one judgementally. Similar tricks seems to exist for judgementally associative path concatenation etc.

However, it would be unlikely to be able to give a slick definition of, say, natural numbers that satisfies the universal property (propositionally), and come equipped with addition and multiplication which satisfy judgemental laws of semirings, inside ordinary MLTT. Usually, a way to prove this is to argue that it renders type checking undecidable, by giving a reduction of the halting problem to typechecking. However for this example it doesn't work because it seems that typechecking of MLTT + Natural numbers with primitives for addition and multiplication with said judgemental equalities is still decidable. (I haven't checked, but this looks plausible and there are similar looking results.)

Is there then a way to argue that this is indeed impossible, no matter how clever and funky the encoding is?

$\endgroup$
4
  • $\begingroup$ If you have $x + y = y + x$ judgmentally with $x$ and $y$ variables, this easily contradicts termination of MLTT computation. Without that you'll need a more subtle argument. Note that the free monoid over a finite decidable type can be encoded using a clever NbE trick. $\endgroup$
    – cody
    Commented Aug 9, 2023 at 18:23
  • $\begingroup$ @cody Can you elaborate on the termination argument? Why can't they both reduce to a common expression? $\endgroup$
    – Trebor
    Commented Aug 10, 2023 at 3:45
  • $\begingroup$ Because any normal form of the LHS would have to be $\alpha$ equivalent to itself, with the variables $x$ and $y$ swapped (since reduction in MLTT commutes with substitution). It's not too hard to see that such a term cannot exist. $\endgroup$
    – cody
    Commented Aug 10, 2023 at 15:49
  • $\begingroup$ @cody Ah, nice argument. I think that's already worth an answer (perhaps with some generalizations). $\endgroup$
    – Trebor
    Commented Aug 10, 2023 at 15:58

1 Answer 1

3
$\begingroup$

This is a really interesting question! I'll try to give some pointers to some possible answers.

One more general question you might ask is

What equivalence relations have constructive quotients?

Namely: given a type $A$ and a decidable equivalence relation $\sim$ over it, can we construct a type $\overline{A}$ and functions $$ ||\cdot|| : A \rightarrow \overline{A}$$ and $$ \mathrm{lift} : \overline{A} \rightarrow A$$

such that $$ a \sim b \Rightarrow ||a|| =_{\beta\eta} ||b||$$ and $$ ||\mathrm{lift}(a)|| =_{\beta\eta} a$$ for every $a$, $b$ of the appropriate types. One may also want the equalities to hold on open terms.

In the more general case, beyond $\beta\eta$, it is known that there are examples of (decidable!) equational systems which do not admit completion, that is that it is impossible to turn them into rewrite systems which are confluent and terminating (as is $\beta\eta$).

This suggests that there may be some decidable $\sim$ that do not admit such a nice embedding. What of the specific case you mention, where $A$ is the "free semiring" and $\sim$ is the corresponding equational theory?

Well here we do run into problems with commutativity: if we had such a $||\cdot||$ working on open terms, then any $t = ||x + y||$ needs to contain both $||x||$ and $||y||$ somehow (and therefore $x$ and $y$ themselves), and $||y + x|| = t[y/x, x/y] = t$, but this is not possible, because the position of $x$ in $t$ must be different from the position of $y$ in $t$!

Note that this argument completely disintegrates on closed terms, and for good reason.

A common solution is to use reflection to turn a term into a syntactic form that does not actually contain variables (they are replaced with, say integers which can be computed with), and in the case where $\sim$ is decidable on closed terms, compute a function which returns the appropriate $\mathrm{bool}$! And hey this is what the ring tactic does in Coq!


It's worth noting that there is a class of problems which admit nice embeddings for which you get the appropriate computational equalities: e.g. free monoids over finite (decidable) sets. This subject is the matter of Normalization by Evaluation, for which there is extensive literature.

$\endgroup$
3
  • $\begingroup$ I think your requirement for $\operatorname{lift}$ is not a reasonable one: if it respects definitional equality (as any construction in type theory should), if $a \sim b$ then $|| a || =_{\beta\eta} || b ||$, and so $a =_{\beta\eta} \operatorname{lift}(||a||) =_{\beta\eta} \operatorname{lift}(||b||) =_{\beta\eta} b$. In other words, $\sim$ must be the same as definitional equality… $\endgroup$ Commented Aug 21, 2023 at 14:09
  • 1
    $\begingroup$ No, you only have $a \sim \mathrm{lift}(||a||)$! Note that $||\mathrm{lift}(a)||$ is not even of the same type as those other two (I should have used a different variable name in my answer). $\endgroup$
    – cody
    Commented Aug 21, 2023 at 15:51
  • 1
    $\begingroup$ Indeed, you are right, I read it the wrong way around. $\endgroup$ Commented Aug 23, 2023 at 17:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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