Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
$\begingroup$
$\endgroup$
5
-
3$\begingroup$ I'm glad you are asking all those questions. I recall that, a couple of years ago, when I tried to get into dependent type theories, I found it hard to find what had been tried, what had been proven. Like many active areas of research, that field lacks an up-to-date summary of the state of the art. $\endgroup$– Martin BergerCommented Mar 21, 2021 at 12:37
-
$\begingroup$ Yes, just throw in those judgemental equalities. It's consistent. $\endgroup$– Andrej BauerCommented Mar 22, 2021 at 7:16
-
$\begingroup$ @AndrejBauer what if I don't want to change the equality checking algorithm? $\endgroup$– user61651Commented Mar 22, 2021 at 7:29
-
1$\begingroup$ But you must change it (if you want it to be complete) because you are introducing new judgemental equalities. $\endgroup$– Andrej BauerCommented Mar 22, 2021 at 7:30
-
$\begingroup$ No I meant that I want a type $T$ with two judgmentally commutative binary operations on it such that externally we can prove there is a bijection from the set of closed terms of $T$ to the usual natural numbers respecting the operations. I don't want to introduce any new rules to type theory. $\endgroup$– user61651Commented Mar 22, 2021 at 7:48
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
3
This is impossible.
- Suppose that we have such a type $T$, with an implementation of addition $\mathit{add} : T \to T \to T$, which is judgementally commutative.
- Because MLTT is strongly normalising, we know that we can put $\mathit{add}$ in $\beta$-normal, $\eta$-long form.
- Now suppose that we have two variables $x, y$ of type $T$.
- Now consider the terms $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$.
- Substituting $x$ and $y$ for the formal parameters of $\mathit{add}$ will not create any new $\beta$-reducible expressions, because $x$ and $y$ are neutral terms.
- Now, $\eta$-expand the occurences of $x$ and $y$ as demanded by the definition of $T$.
- Now, the resulting terms will be identical except that we've permuted the occurences of $x$ and $y$.
- Recall that judgemental equality for $\beta$-normal, $\eta$-long terms is just $\alpha$-equivalence.
- Since we assumed $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$ were assumed to be judgementally equal, this means that the normal forms for these two terms are $\alpha$-equivalent.
- Since anywhere that $x$ occurs in the normal form for $\mathit{add}\,x\,y$, a $y$ occurs in the corresponding position of the normal form for $\mathit{add}\,y\,x$, the only way that these two terms can be $\alpha$-equivalent is if neither $x$ nor $y$ occurs in the term.
- This means that $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$ do not use their arguments!
- As a result, we can conclude that $\mathit{add}\,1\,1$ and $\mathit{add}\,0\,0$ are also judgementally equal.
- Therefore $T$ cannot be the natural numbers, since $2$ and $0$ must not be judgementally equal.
answered Mar 22, 2021 at 10:05
-
$\begingroup$ Could you explain step 9 in more detail? $\endgroup$– user61651Commented Mar 22, 2021 at 14:44
-
-
1$\begingroup$ It seems that I've given pretty much the same answer for another question. $\endgroup$ Commented Mar 23, 2021 at 10:28
$\begingroup$
$\endgroup$
CoqMT (Coq Modulo Theory) was an extension of the Coq proof assistant that allows one to parametrize a development with a decidable first-order theory T. Since equality on natural number expressions with addition and multiplication is decidable, this would be a valid application of CoqMT. Unfortunately, the implementation has not been updated in over 10 years.
