[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!