patternMinor
MLTT not being Turing Complete
Viewed 0 times
mlttbeingcompleteturingnot
Problem
Where can I find a proof that Martin-Löf Type Theory isn't Turing Complete, if such proof exists?
Solution
It is a general feature of reasonable total programming languages that they do not have self-interpreters, but interpreters for reasonable programming languages are Turing-computable. So, a concrete example of a total computable function which is not definable in a total programming language is an interpreter for that programming language.
See Definition 2.1, Theorem 2.2, and Corollary 2.3 of this note. It proves that a self-interpreter for Gödel's T is not definable in Gödel's T. You can use the exact same proof for MLTT.
It is generally well known that a confluent terminating normalization system such as that of MLTT leads to a Turing-computable normalization procedure.
See Definition 2.1, Theorem 2.2, and Corollary 2.3 of this note. It proves that a self-interpreter for Gödel's T is not definable in Gödel's T. You can use the exact same proof for MLTT.
It is generally well known that a confluent terminating normalization system such as that of MLTT leads to a Turing-computable normalization procedure.
Context
StackExchange Computer Science Q#62994, answer score: 6
Revisions (0)
No revisions yet.