[ch0ic3]

I'm struggling with the mini rant / motivation of the article:

> Typically, not being Turing-complete is extolled as a virtue or even a requirement in specific domains. I claim that most such discussions are misinformed — that not being Turing complete doesn’t actually mean what folks want it to mean

Why are those discussion misinformed? Most formal analysis tools (Coq, Isabelle, Agda(?)) usually require a proof that a function terminates. This is I think is equivalent to proving that it is total implying it is primitive recursive?

[IshKebab]

I haven't got to the end of it but I assume this was motivated by some configuration languages using "not Turing complete" as a feature, when the feature they really want to advertise is "reasonably bounded execution time".

It came up recently in this discussion about CEL:

https://news.ycombinator.com/item?id=40954652

[nyrikki]

As you are talking about formal proofs, and not the scientific counterexamples modern programming uses:

Proving a function is total in the general case is a NP total search problem.

IIRC this is equivalent to NP with a co-NP oracle, or the second level on the PH hierarchy, aka expensive if even possible even in many small problems.

Most of those tools work best if you structure your programs to be total, of which structural programing with only FOR or iteration count limited WHILE/recursion are some the most common methods.

While just related to SAT, look at the tractable forms of Schaefer's dichotomy theorem is the most accessible lens I can think of.

[BalinKing]

> Proving a function is total in the general case is a NP total search problem.

My intuition suggests this should be undecidable—could you elaborate on the difference between this and the halting problem?

[nyrikki]

Halt is a decision problem, TFNP is a combinatorial problem constructed of decision problems.

The HALT decider is a total Turing machine that represents a total function.

I am struggling to explain this in a rigorous fashion, and there are many open problems.

NP is where the answer "yes" is verifiable in polynomial time.

co-NP is where the answer "no" is verifiable in polynomial time.

NP is equivalent to second order predicts logic where the second term is existential 'there exists..'

co-NP is equivalent to second order predicts logic where the second term is universal 'for any'

We know P=co-P, or that the yes and no answers are both truthy.

We think that NP!=co-NP

Many useful problems are semi-decidable or recursively enumerable.

Determining if a computable function is total is not semi-decidable.

It is the subtle difference between proving a TM halts for any input vs halts for each input.

Termination analysis is the field of trying to figure out if it halts for each input. It is actually harder than HALT, being on the second level of PH on the co-NP side.

If that granularity isn't important to you, I personally don't think there is much of a risk in using the decidable metric as a lens.

Just remember that something is decidable if and only if both it and its complement are semi-decidable.

Semi-decidable problems often have practical applications even without resorting to approximations etc ...

[cvoss]

I'm not sure this really addresses GP's question, which I share.

You claimed in GGP that deciding whether a function is total is a TFNP problem. In particular, that would make it decidable. But the counter-claim is that deciding whether a function is total is actually an undecidable problem.

I've also examined a definition of TFNP and I don't see how it is related to the problem of deciding if a function is total. Rather, the definition seems to require that the function in question be total.

[colevee]

Your intuition is right. The total functions are not even a provable set. So they are definitely not recursive or even FNP; never mind TFNP. Provability of the total functions would imply decidability of an even harder problem than the halting problem: whether a given Turing machine halts on _all_ inputs.

The halting problem only asks: given a TM and input, will the TM halt on that input? That problem is actually semi-decidable/provable: we just run the machine. If the answer is yes, then at some point it will halt!

[bmillwood]

> This is I think is equivalent to proving that it is total implying it is primitive recursive?

No, as the article shows there are functions which terminate that aren't primitive recursive, and indeed Agda and (probably?) the others can prove termination for some (but necessarily not all) terminating non-primitive-recursive functions.

I think the misinformation that the article is complaining about is something like (my paraphrase):

> "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"

The article points out:

- you can be non-Turing complete and still do lots of computationally-expensive / tricky work

- your configuration language probably wants much stricter limits than merely being non-Turing complete

[chowells]

> I think the misinformation that the article is complaining about is something like (my paraphrase):

> > "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"

"Turing complete" means it can do any computation a Turing machine can. That is absolutely more power than is desired about 99.99% of the time. You almost always want your algorithms to contain no infinite loops.

(Algorithms. Not IO loops. Those are different, and the process of taking outside input while the program is running is outside the scope of what a Turing machine talks about anyway.)

Turing completeness is an ergonomics hack, and one with a decently successful history. But it's no panacea, and if we could find an ergonomic way to get rid of it, that would be a win.

Yes, even if we didn't also enforce primitive recursion. Sure, it's nice to know you're also not accidentally running Ackerman's function, but to be honest... I've had many more accidental infinite loops than accidental Ackerman's functions in my code. By approximately 10,000 to 0.

No system can ever prevent all errors. So let's focus on preventing the most common current ones.

[lanstin]

First thing I do when I am learning a new high level language is write Ackermann function and see what happens. Also write out plus and mult and expt in terms of +=1. I have seen people with O(n^4) code when they could have easily used O(log n) but never seen an Ackermann in the wild.

[nine_k]

Possibly there are more ways to be non-Turing-complete than being a nice total terminating function. For instance, an infinite loop is neither capable of universal computation nor is terminating.