Lean 4 solves the Halting Problem (?)

Stream: lean4

[Bernardo Borges]

What I find remarkable in Lean4 is that when a recursive function is written, some proof of termination is required. In this sense, the programmer is required to have a code terminate in order to have it compile! In this way, does Lean 4 avoid the Halting Problem alltogether or is there any false claims above?

[Joachim Breitner]

Almost: You have to prove the halting problem. At least if you want to be able to write any terminating function :-)

[Henrik Böving]

You can also get around this restriction by using a partial defwhich is still sound in the type theory due to the tricks involved but can be a non terminating function internally.

[Bernardo Borges]

Interesting. Another question that comes to mind is whether any termination is provable, or if the proof system will not accept any proof for some programs that arguably terminate. In any sense, the little extent of which i l loooked at termination_by and decreasing_by arguably cover only some "happy cases" which have simpler termination proofs

[Joachim Breitner]

I expect that there are terminating programs for which no proof of termination can be expressed within lean. Maybe Gödel can tell us more.

[Eric Rodriguez]

I think there's some also fundamental limitations to what can be proved to be terminating in Lean, iirc

[Kevin Buzzard]

There's a chance that the Collatz conjecture is true but not provable -- Conway proved that a certain generalisation had this property. So this would give us a function which is impossible to define without sorries or partial / unsafe.

[Mario Carneiro]

Joachim Breitner said:

I expect that there are terminating programs for which no proof of termination can be expressed within lean. Maybe Gödel can tell us more.

The classic example is the lean typechecker, but that doesn't really work since the typechecker actually doesn't halt under some circumstances. I think the Coq typechecker would work as an example here (i.e. Lean can't prove that the Coq typechecker halts, even though it is believed to halt with suitable large cardinal assumptions)

[Mario Carneiro]

However lean's termination checker is "complete" in the sense that if you can prove a function terminates, then you can prove it in a termination_by statement

[Jason Rute]

Joachim Breitner said:

I expect that there are terminating programs for which no proof of termination can be expressed within lean. Maybe Gödel can tell us more.

You can't enumerate a set of programs which cover all total computable functions from Nat to Nat (follows from Rice's theorem) but you can enumerate all provably terminating functions in Lean from Nat to Nat (just go through all Lean files and all amounts of time you are willing to wait for the type checker) so there must be total functions which terminate but Lean can't prove. (Also, it isn't hard to see that terminating is the only issue. partial def is Turing complete in that you can express all partial computable functions from Nat to Nat.)

[Martin Dvořák]

Kevin Buzzard said:

There's a chance that the Collatz conjecture is true but not provable

True in the standard model of natural numbers but unprovable in Peano arithmetic?

[Nir Paz]

It looks like the termination of any turing machine can be converted to asking whether or not some generalized Collatz function reaches 1 on a specific input, so Collatz could theoretically be independent of ZFC.

[James Gallicchio]

ZF+C+CH+CC (collatz conjecture)

[Mario Carneiro]

Nir Paz said:

It looks like the termination of any turing machine can be converted to asking whether or not some generalized Collatz function reaches 1 on a specific input, so Collatz could theoretically be independent of ZFC.

Do you have details on this? I haven't heard of "generalized Collatz" being turing complete

[Mario Carneiro]

(depending on how much you want to generalize...)

[Mario Carneiro]

FRACTRAN is the most similar turing complete language I'm aware of

[Nir Paz]

By a generalized Collatz function I mean a function g(n)=n⬝a_(n mod p)+b_(n mod p) where aᵢ, bᵢ are rationals chosen so that the output is always an integer (the usual function is p=2, a₀=0.5, a₁=3, b₁=1). But for the undecidability we can even let the b's be 0.

I found the original paper referenced on wikipedia (Unpredictable Iterations, Conway 1972) in a book and went over it, and the proof basically shows that if g is the "next step function" of a fractran program, then it's also a collatz function. The proof is surprisingly simple, so modulo the undecidability of fractran it's very short:

If a₁ / b₁,..., aₙ / bₙ are the rational numbers describing a fractran program, define g(n) = n ⬝ aᵢ / bᵢ for the minimal i such that this is an integer. The completeness of fractran says that the termination of g on a particular input is undecidable (I think?).

Now look at g(n) / n. This function is periodic, with period some divisor of the lcd of all denominators on the list (I don't see why this is true, but it sounds like pretty simple number theory). So if we name the period P, we get that g(Pk+r)/(Pk+r)=g(r)/r, or g(Pk+r)=g(r)/r⬝(Pk+r). So g is actually a generalized collatz function!

[Nir Paz]

Well I just realized this just shows the undecidability of the question of, given a finite list of rationals, whether a Collatz function reaches a value that doesn't multiply to an integer with of them is, rather than whether it reaches 1. If someone is interested they can go look at the paper, it's a bit too much for me.

[Nilesh]

I have a newbie question about the halting problem:

I came across Univ of Toronto's CS prof Eric Hehner's views on the halting problem. He argues that the Halting problem is not a limitation of computability but an inconsistency of specification.

His views have been challenged. Some even called him a crank.
Others have found some support for his claims.

Can Lean be used to shed light on and settle this argument? :thinking:

[Edward van de Meent]

I'd certainly say so, although I do think his views are Definitely wrong.

[Edward van de Meent]

Or at least those expressed in the video of his homepage

[Kyle Miller]

When reading https://www.cs.utoronto.ca/~hehner/RHP.pdf, on page 2 it's very wrong to say that D is "completely innocent". The issue is that D is referring to H. How is this H resolved? There's no assumption about computability of H, so the function H has no textual program that can be pasted in at that position. This is the moment where the usual assumption that H is computable is tacitly assumed.

If somehow it's up to H to be able to resolve the primitive H to its own specification, then, yes, that would be an inconsistent specification, and that's sort of the point of the halting problem.

[Edward van de Meent]

indeed, i found it hard to understand what to interpret "inconsistent specification" as, other than "there is no program that fits these specifications", which is precisely the point.

[Kyle Miller]

"Specification" is referring to an axiomatic description of the function H, and "inconsistent specification" means the set of functions satisfying that description is empty. That part is fine I think — it's pure functions rather than programs that implement the functions.

[Alex Meiburg]

Nir Paz said:

It looks like the termination of any turing machine can be converted to asking whether or not some generalized Collatz function reaches 1 on a specific input, so Collatz could theoretically be independent of ZFC.

Since this thread was revived: I'm pretty sure this is wrong. It can't be independent of ZFC. That would mean that there is a model of ZFC where iterating your function f on the input n reaches 1 after some number of steps k. And if that's true, then you have a proof of that by just directly evaluating that, so it doesn't use any extra axioms; so it would be true in any model of ZFC.

In general, any "computationally verifiable" (or computationally falsifiable) statement like this can't be independent of ZFC. So the same goes for the Goldbach conjecture, Riemann hypothesis, P=NP... etc.

Now, these problems might be unprovable in ZFC. And generalized Collatz problems are indeed unprovable in ZFC. That is: there is a generalized Collatz function f which always reaches 1 on any input, but this is unprovable; you get this by encoding "Does input x constitute a valid disproof of the consistency of ZFC" into f, and having f go to infinity if it finds an inconsistency.

But being logically independent vs being unprovable are very different, and somehow end up conflated with one another very frequently!

[Nir Paz]

To be clear on definitions, when I say "independent of ZFC" I mean "cannot be proven from ZFC", or equivalently (by the completeness theorem) "is true in some model of ZFC and false in some other".

Statements like Collatz can be independent even if true because even if for every natural n, that is a number of the form 1+1+...+1, you have a proof that it terminates on Collatz, and thus is terminates in every model of ZFC, that does not mean that every model satisfies "for every natural n, Collatz terminates on n". Some models of ZFC have nonstandard natural numbers not of the form 1+1+...+1, and those might not terminate.
These nonstandard naturals are actually never computable, so you couldn't have a proof of the form "just run Collatz manually" even for specific nonstandards.

So ∀ n ∈ ℕ, ∀ M : ZFC, M ⊧ n terminates does not imply ∀ M : ZFC, M ⊧ ∀ n ∈ ℕ, n terminates, because different models have different ℕ. And when we write M ⊧ n terminates we're abbreviating the statement M ⊧ 1 + 1 + ... + 1 terminates, but not all of the naturals of M can be written like this, only the standard ones.