Apart from problems that specifically have to do with Turing machines, like "Simulate a Turing Machine with the given description", are there any problems that require Turing-complete potentially nonterminating recursion?

For example, are there any known non-Turing-machine-related problems that can't be solved in Coq?

  • $\begingroup$ Are you asking for examples of semi-decidable undecidable problems (i.e. a recursively-enumerable and not recursive language?) $\endgroup$
    – JimN
    Jul 31 '16 at 21:30
  • 1
    $\begingroup$ Anything that tries to solve an undecidable problem: showing termination, proving theorems in first/higher-order logic, null pointer analysis... $\endgroup$
    – cody
    Aug 1 '16 at 11:44

Given a system of polynomials with integer coefficients (Diophantine system), find a solution if there is one, or else run forever. Any program which does this must necessarily be partial because the set of solutions of Diophantine systems is a complete c.e. set, see Hilbert's tenth problem.


Not the answer you're looking for? Browse other questions tagged or ask your own question.