In Types and Programming Languages by Pierce, is it correct that

  • the language introduced in Chapter 3 Untyped Arithmetic Expressions is not Turing complete? Because it doesn't provide recursion.

    enter image description here

    enter image description here

  • the language introduced in Chapter 5 Untyped Lambda Calculus is Turing complete? Because it provides recursion.

    enter image description here


  • $\begingroup$ Hint: try to prove that all computations are terminating. If you can, then it must not be Turing Complete. $\endgroup$ – jmite Sep 9 '19 at 3:19
  • $\begingroup$ Thanks. I don't have a sufficient background to prove or disprove the two examples. I just seem to recall seeing some book about reasoning about whether a language is Turing complete, by whether it has recursion. If following your comment, for the first example, evaluation of all its terms seem to terminate, while for the first example, (\x.x x) (\x.x x) does not terminate. $\endgroup$ – Tim Sep 9 '19 at 9:52
  • $\begingroup$ Nontermination is necessary for a language to be Turing complete, but not sufficient. Having unbounded recursion is a good indicator that a language might be Turing complete. In this case, the Untyped Arithmetic Expressions language is terminating, so is not Turing complete. Proving something is Turing complete is more work, but it is well known that the untyped $\lambda$-calculus is Turing complete, unlike the simply-typed $\lambda$-calculus. $\endgroup$ – varkor Mar 17 '20 at 13:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.