2 ms·
Is Type Theory Turing Complete?
I'm working with interval arithmetic.
Intervals have the annoying arithmetic behavior of tending to get wider.
So [1..3]+[2..5] ends up with [1..8]
On the other hand, if I'm trying to compute the "cover" of an area
this tendency to cover more area is what I want.
On the third hand, it seems that singleton intervals mirror arithmetic.
So [1..1]+[2..2] ends up with [3..3]. Since I have addition it seems I get multiplication.
Which leads me to the question... is type theory turing complete?
Can I compute any result using only types?
Can I create a "type computer"?
- andrew_jhnson_4 3y agoNot if the system is strongly normalizing, which most type systems aim for as a design objective: https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting) https://en.wikipedia.org/wiki/Normal_form_(abstract_rewritin...