3
$\begingroup$

Where can I find a proof that Martin-Löf Type Theory isn't Turing Complete, if such proof exists?

$\endgroup$
11
  • 2
    $\begingroup$ Where have you looked? What have you tried? $\endgroup$
    – Raphael
    Commented Aug 29, 2016 at 11:18
  • $\begingroup$ I tried googling a lot $\endgroup$ Commented Aug 29, 2016 at 11:18
  • $\begingroup$ Well I also tried thinking about it being able to express Heyting arithmetic therefore also Peano by double negation translation, therefore by Matiyasevich it is Turing complete. But i dont know if thats correct $\endgroup$ Commented Aug 29, 2016 at 11:31
  • $\begingroup$ That's too hand-wavy. What does "express Heyting arithmetic" mean? $\endgroup$ Commented Aug 29, 2016 at 13:54
  • 1
    $\begingroup$ @TroyMcClure It's convenient to separate recursion and proving well-foundedness of the recursion separately. Even a program like $gcd$ is annoying to write using just primitive recursion. Using general recursion and then proving that the recursion is well-founded is easer. Division of labour. However, under the hood, all the termination checker does is proving that the program could be reduced to primitive recursion. $\endgroup$ Commented Aug 30, 2016 at 13:44

2 Answers 2

6
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$
    – Raphael
    Commented Aug 30, 2016 at 10:42
0
$\begingroup$

Section 4 of P. Martin-Löf's An Intuitionistic Theory of Types presents a normalisation proof of (a variant of) MLTT.

More (related) proofs can be found in the following papers.

A problem with normalisation of MLTT is that there are many variants of MLTT, and even small changes in the definition of what MLTT is might have substantial effect on normalisation.

$\endgroup$
4
  • $\begingroup$ Is this a question or an answer? If the former, I'd convert to a comment; if the latter, please expand a little bit to include more than just a link, which may break at any time. $\endgroup$
    – Raphael
    Commented Aug 30, 2016 at 10:42
  • 1
    $\begingroup$ This doesn't answer the question. MLTT could be normalizing and still able to express all computations. $\endgroup$ Commented Aug 30, 2016 at 20:58
  • $\begingroup$ @Gilles in what sense? $\endgroup$ Commented Aug 30, 2016 at 21:57
  • 1
    $\begingroup$ @Gilles I wonder how? Doesn't the fact that every program terminates implies that a programming language is not Turing complete? How could a type theory be normalizing and express programs such as $\Omega$? $\endgroup$ Commented Aug 3, 2018 at 15:06

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.