Comment by zamadatix | Hacker News Reader

Comment by zamadatix | Hacker News Reader

Parent Full thread

The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims can also be rigorously proven to match the conditions of the generalized halting problem first). I.e. I'm not trying to say the halting problem does not apply to these systems in general, I'm saying it doesn't apply to the specific claims being made about these systems.

As an example of the type of thing I'm saying: one can show an algorithm which multiplies a real number by 2 cannot guarantee the output will be an even number for all inputs. Separately, one can create and prove a algorithm which takes an integer number greater than 0 and multiplies it by 2 will always meet the very same guarantee. In this scenario it clearly did not matter the first proof of lack of guarantee applied to all algorithms using real numbers, the more restricted subset of real numbers could make a guarantee.

Specifically to the halting problem and Bend again: It's not about an algorithm which can definitely answer yes or no for any program+input. The given claim/condition from Bend is simpler: it blocks mistakes (because it only accepts provably valid proofs, not because it can prove every input one way or the other).

> Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement.

It blocks AI mistakes, it only accepts ones able to be proven. Nothing in that claim says it will prove every input one way or the other, that's just an assumption which you rightly showed could not be a reasonable interpretation of the title.

It might also be prudent to ask the author if they really mean they interpretation you take before declaring the problem as beginner's lacking understanding of a foundational theory in computer science.

> No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.

What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?

As a side note, I have no affiliation or ecen prior knowledge of the project/author prior to reading this post, I just get nerd sniped by overly broad claims about the halting problem.

> It blocks AI mistakes, it only accepts ones able to be proven.

This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.

> It might also be prudent to ask the author if they really mean they interpretation you take

How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.

> What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?

I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .

> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.

I disagree, which is why I added all of the additional commentary you appear to have ignored to restate your original claim instead. I'm not sure why I should restate my response to these points when they're still available and awaiting response above.

> How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.

When someone's words on a project as complicated as this seems to violate the basic foundations of computer science it's both your problem & disrespectful to claim you know for certain the problem is because it's a common beginners mistake. This may be something we cannot come to an agreement on morally, but I suppose it won't really matter for the rest of the mathematical conversation which continues below.

> I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .

Wikipedia is a poor source to cite, but when I follow it I see no claim or definition by Turing for what non-trivial is. I see claim of what Rice meant by non-trivial in their eponymous theorem in 1951, but that's neither from 1936 nor a relevant definition for the current discussion so I must assume you mean somewhere else in Turing's actual paper I'd need to check.

Which takes us to the actual 1936 paper rather than Wikipedia's summary https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf. I see 3 mentions of triviality, none of which appear to give a definition of what a non-trivial provably haltable example is:

1. Discussion of the remainder of the theorem itself being trivial [on page 31 of his paper, page 260 of the journal]

2. Since CC_0 is already been shown provable the conditional proof of the A(M)->CC_0 is trivial by the rules of implication [p32, 261 of the journal]

3. A trivial replacement of the variable naming scheme allows translation between the two notations without changing the calculus of them. [p34, 263 of the journal]

None of these seem to define what a non-trivially provable program (Turing Machine/Algorithm) is in context of the halting problem, so I again ask can you tell me where and what actual definition in Turing's actual 1936 paper you are using to define what a non-trivial program is so that I may apply this definition to the current conversation?

As another aside, one of my favorite "simplest" examples of a non-trivially provable program we know never halts despite the general case result of the halting problem:

  for every group of positive integers (a,b,c,n) with n > 2:
    if a^n + b^n = c^n:
      halt

To prove this never halts you have to prove Fermat's last theorem. Which we have, and so we know this must never halt as you iterate infinitely over the positive integers, but it took one of the most complicated mathematical proofs known to show it.

There are certainly definitions of non-trivial where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.

>> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.

> I disagree ...

This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity.

The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion.

> There are certainly definitions of non-trivial ...

This is a logical fallacy known as "Logic Chopping" : https://iep.utm.edu/fallacy/#Logic%Chopping

> where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.

Yes, I can see that, but that's not what this discussion is about. Read this before posting again: https://en.wikipedia.org/wiki/Halting_problem

Dozens of online articles on this topic, make the same point in the same way. None of them digress into logical fallacies.

> This may be something we cannot come to an agreement on morally ...

"Morally", really? Another logical fallacy, another digression, and not the topic.

If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself (or at least a link to the specific math directly relevant to the claim), not an English text summary of an entire paper/problem on Wikipedia. Anything less is not mathematical reasoning.

I'm unable to say more at this point as I can only assume you will continue to use that as a chance to quote and discuss everything but actual mathematics.

> If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself ...

This is not a philosophy discussion, and Alan Turing already plowed this ground. The original claim "Bend - a language that blocks AI mistakes via proof [...]" is unsupportable.

> ... if every program can be proven to halt ...

But that's not so. You have introduced a qualifier that is known to be false.

> ... a chance to quote and discuss everything but actual mathematics.

Yes, I agree -- you should stop doing that. I keep referring to the original technical reason the original claim is unsupportable, others keep raising objections without trying to think through their positions.

It's not as though the Halting Problem is on the Millennium Prize Problem list, open to contradiction/reconsideration by some future challenge. It's a theorem, not a conjecture.

I've given notes of where in Turing's paper any type use triviality could be found, with direct page citations of the relevant original math, along with the mathematical reasons it doesn't have anything to do with the plain English statements you are making. This effort was a kindness done in good faith that I might find said mathematical definition of non-triviality for the halting problem somewhere in the paper, not something needed to show your claim devoid of a shown basis in mathematical reasoning so far. That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.

That said, if you'd like me to formally show what e.g. the triviality in the rules of implication Turing was talking about are in a purely mathematical form I'd be glad to state with no English commentary out of good faith as well. This would seem a waste of time unless that's the part of the paper you think the definition of non-triviality can be sourced, but at least I'd at last have a clear mathematical claim from you to discuss.

It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.

> That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.

I posted the Turing Halting Problem Wikipedia page. It describes a theorem, not a conjecture that I need to prove, which shows the original poster's claim is contradicted by established facts.

Let me put it this way. If I say, "There are an infinity of primes," will you reply, saying, "I disagree"? That position would be equally appropriate -- that is to say, not appropriate at all.

Am I obliged to prove the infinity of primes by generating an infinity of candidate integers and prove that some of them are prime? No, and by the same token, I'm not obliged to reply to your naive demands and teach you why the Halting Problem falsifies the claim made by the original poster. That is not my responsibility, it is yours.

In mathematics, some things are conjectures -- the Millennium Challenge problems, for example. Others are theorems, meaning established truths, beyond dispute. Turing's Halting problem is a theorem.

Here is another authoritative reference to the fact I originally posted: "Did Turing prove the undecidability of the halting problem?" from the Oxford University Press -- https://academic.oup.com/logcom/article/36/1/exaf075/8417148 .

The question in the title is rhetorical, as you will discover if you read and understand the article I just linked.

> It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.

How many more mathematical literature references will you require before you realize I have already met any burden of proof? I could post the entire technical proof here, but (a) the editors of this forum would kick me out, and (b) you would still refuse to accept the evidence.

How do I know this? Because you keep refusing to learn what you need to know to engage in this conversation.

There are an infinity of primes -- your turn.

The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be (using a similar type of argument I gave early on for the current discussion):

  Define:
  
  A_n = n\*n
  n ∈ Z_>=2

  ∴
  
  A_n ∉ ℙ ⇒ ∀n
  
  ∴
  
  |ℙ| = ∞ ∧ ∀n ∈ ℤ_>=2, A_n ∈ ℕ ∖ ℙ

   Q.E.D.

(Apologies for the formatting, HN does not allow latex)

The thing blocking me from being able to do the same here is I defined a similarly styled argument about it being possible to construct a program (glad to give it in pure math if tou'd like) which blocks all non-halting programs by only allowing ones showable to be halting (n.b. much as the above example with primes, this result did not require listing every non-halting program and so does not disagree with the general halting problem) and you said Turing's paper contains some definition of non-triviality which says why that cannot be and then refuse to say what and where in this paper you believe this definition of non-triviality to be even though I could find no such thing.

If you said Euclid showed the above proof on primes does not apply because he gave some definition of non-triviality, telling me it's somewhere in his book Elements, and I said book IX proposition 20 does not say anything like that, so you say "it's on Wikipedia"... you could see why I have doubts you have any mathematical claim to produce defining said definition. At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.

> The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be ... [ snip ] ... Q.E.D.

Now I get it. I should have realized at the outset that this outcome lay in the future. You are here to pointlessly argue, not discuss nor debate.

> At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.

Yes -- notwithstanding that I have posted links to that exact evidence from multiple sources. The problem is not a lack of evidence, the problem is that you refuse to read it.

On that topic, here is a link to Alan Turing's 1936 paper -- 36 pages long: https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf

Andrew Wiles conclusively (dis)proved Fermat's Last Theorem. If you disagree, and since you have demonstrated a willingness to disagree with anything, I would have to post a link to the evidence, not the evidence itself, because the (dis)proof is 129 pages long.

As I post this, I'm trying to imagine the corpus of mathematical knowledge you're unwilling to accept, because it won't fit into a finite-sized Hacker News post -- relativity, both special and general, quantum mechanics, dozens of others.

I'm also trying to imagine someone whose literacy filter consists of "Tl;DR!"

It truly breaks my heart to see any of the math snipped out yet again. You sound more than capable of formulating your assertions in pure math but seemingly refuse to state it that way, which feels like watching a bright light in the world going out as it seeks to avoid rigor.

A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney. I believe all of these beautiful proofs, I just don't believe you've properly demonstrated you can build your chimney with them. If you ever wish to build the chimney I'd be ecstatic, until then I think I don't think anything else can be said about how the pile of bricks aren't an example of one - especially if you're going to give the URL I already provided you when asking where the definition of the connection in it was https://news.ycombinator.com/item?id=49761146

I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you. It's something I hold dear. I'll keep notifications in my script enabled in case you do want to start discussing the math rigorously, but I'll no longer try to convince you that's what's needed for your claims to hold mathematical weight anymore or any of the other things which seem to be bothering you for no gains.

> It truly breaks my heart to see any of the math snipped out yet again.

A false statement. I posted a link to the evidence, which cannot be summarized to satisfy your short attention span. Your unwillingness to read it only reveals your shallow grasp of modern technical topics.

Here is a short list of topics that cannot be converted into bumperstickers, your preferred medium of expression:

   Special and General Relativity

   Quantum Physics et. al.

   Cosmology

   Biology

   Modern Set Theory

This list is by no means complete, but the last entry overlaps with the topic of this conversation, for reasons that will not be obvious to you unless and until you overcome your distaste for evidence.

> I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you.

Excuse, me, what? I have posted links to the evidence that proves your position to be false, but you won't read it. You are to modern times what a religious fundamentalist is to science -- the primary obstacle to human progress.

Am I saying your unwillingness to absorb ideas outside your short attention span is itself an obstacle to human progress? No, actually, I'm saying you should avoid drawing conclusions without first examining the evidence.

It isn't only that you won't read the evidence that proves your position to be wrong -- that is simply sad, not fatal. It is that you draw conclusions without first examining the readily available evidence.

> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.

Wow. You just dismissed the validity of all the topics in my list above, each of which produce everyday valid conclusions derived from very complex logical and mathematical antecedents.

Get professional help.

> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.

A second reply. What you're not getting is that the mathematical equations in Turing's paper don't make its point. There are plenty of equations, but the paper's meaning lies in its logical arguments, for which the equations can only play a supporting role.

If the equations are taken out of the paper and presented separately, as you have repeatedly demanded, the paper's thesis falls apart. But to understand this, you would have to read the paper itself and absorb Turing's logical arguments. And the paper can't be made shorter without losing its meaning.

More evidence for this is given by the fact that Alonzo Church published a similar paper in 1936, different author, different equations, but the same logical argument and conclusion, such that Church and Turing are now given equal credit for the basic idea -- an idea that is supported by equations but not provided by them (https://courses.fit.cvut.cz/MI-VYC/church-a-note-on-the-ents...).

This is true in many parts of mathematics and logic. Another example is Einstein's 1905 paper later identified as the source of "special relativity". If you remove the equations and present them separately, all meaning is lost. In fact, in that case, the actual meaning of a particular equation was lost to Einstein himself, but that meaning occurred to his former math teacher Hermann Minkoswski, who went on to publish about something Minkowski called "spacetime". As before, the equations didn't convey the paper's real meaning, they could only play a supporting role. About this outcome Einstein later said, "Since the mathematicians have invaded relativity theory, I don't understand it myself any more."

Another more recent example is the recently solved "Navier–Stokes existence and smoothness problem" as it was titled by the Clay Mathematics Institute. The equation is easy to render, but as with the other examples, the problem to be solved goes far beyond the equation itself, and the meaning of the recent result lies not in the equation, but in its treatment and processing by AI.

In Navier-Stokes, everyone had access to the equations, but until recently no one could answer a fundamental question about it, and as with the prior examples, the real meaning requires one to read the articles that provide the logical reasoning. In each of these examples and many more, listing the equations can only be a preliminary step to true understanding.

More importantly, the meaning of the papers cannot be summarized in fewer words than are provided by the papers themselves. Mathematicians don't go out of their way to make their papers longer than their contents require, in fact, quite the opposite.

I can't believe you're still expecting bumperstickers to stand in for technical articles. As before, you should read the original articles instead of complaining that they're too long for your limited attention span.

> There are plenty of equations, but the paper's meaning lies in its logical arguments

This is the difference I feared. I trust, understand, and take lead of the rigorous math of the paper, you opt to follow in English arguments of what you think it's supposed to mean or apply to. No matter how much math is discussed, it'll never lead to anything if that's not where your understanding of the paper comes from.

It's one of the main things which separate hard sciences from things like Psychology where anyone can just talk about what they understand/see or want to link instead of define it in logic itself, and I must admit I've never believed much of the soft sciences because of that lack of rigor. Maybe that rejection of soft science as truth is a limitation of mine :) but I don't see myself abandoning the view any time soon.

>> There are plenty of equations, but the paper's meaning lies in its logical arguments

> This is the difference I feared. I trust, understand, and take lead of the rigorous math of the paper, you opt to follow in English arguments of what you think it's supposed to mean or apply to.

Excuse me? The articles don't prove their theses with mathematics, they prove them with logic. Equations are assistants, but they're entirely replaceable, as proven by the fact that Church and Turing used different equations in support of their theses -- articles that come to the same conclusion.

How did you miss the significance of the Alonso Church article's final sentence: "The general case of the Entscheidungsproblem of the engere Funktionenkalkül is unsolvable." Where are the equations that you think make the point better than these words? Certainly not in the article. Why didn't Church refer to an equation to support his conclusion? The answer is that his conclusion is a logical one, not a mathematical one.

In the case of Navier–Stokes, the equation is a preliminary, a self-evident statement about energy, inertia, pressure and a few other things. If it were rewritten (as it often is), the problem remained to be solved. Those who solved it didn't post a new equation, they posted a new insight.

In the relativity example, Einstein wrote an equation but didn't understand it -- his math teacher took over. Any number of equivalent expressions would have provided a basis for progress toward a more comprehensive theory. The point was the ideas, not the equations.

> ... the rigorous math of the paper ...

Nonsense. In both papers, the authors use mathematics only to support their points, in the same way that an author uses words to craft a story. If separated from the logical thread, the words (the equations) lose all meaning. This is proven by the fact that the two papers use different mathematics to support the same thesis.

But I see I'm wasting my time. Mathematics is a language, but to use it, you must have something to say.

Church and Turing did not prove their papers with the words, they described the math proving their statements in them and what that math implies (which is why the ending summary would not be math, it must already have been shown to be a summary). In however many comments you have certainly used a lot of words to describe your thought but have given nothing in the way of the math used to base the difference in your claim between that of Church/Turings.

A psychologist could just as well assert the halting problem contains math applicable to any system and therefore blue cars mathematically make us angry. The doubt would then not be on Turing but on the psychologist to show how on Earth they are mathematically linking what they are saying with what Turing actually showed. That they don't see a requirement in having the chain of math rigorously define and prove the claim when they make it is precisely why they are a soft science - they can just claim it seems to relate by less rigorous means. Defend that kind of approach if you wish, it does not make it more rigorous.

I expect we'll soon hear words about more mathematicians and scientist, related to the current problem or not, rather than math. Perhaps I've allowed myself baited by hope again on the mention of what math is needed being discussed.

> Church and Turing did not prove their papers with the words,

THAT STATEMENT IS FALSE. The two articles used DIFFERENT EQUATIONS TO SUPPORT THE SAME LOGICAL ARGUMENT. Church and Turing are jointly credited with the same logical conclusion, even though they used different mathematical arguments. NO ONE said, "Wait, the equations are different, therefore the conclusion must be different." At least no one with an education.

> ... they described the math proving their statements in them and what that math implies (which is why the ending summary would not be math, it must already have been shown to be a summary).

Church and Turing made the same logical claim, using the same words but different mathematical arguments. This places the math in a supporting role, below logical reasoning. This is true in all the examples I provided. Math is a language, but to use it, you must have something to say.

In the Relativity example I gave, Einstein's math teacher used the SAME equation to draw a DIFFERENT CONCLUSION, because EQUATIONS SUPPORT IDEAS, THEY AREN'T THEMSELVES IDEAS.

Just as with words, math equations never stand by themselves -- they support ideas, and the same idea can be expressed by different mathematical arguments. That was the point of all my examples, which clearly fell on the ears of a religious true believer.

This equation -- y = sqrt(1-x*x) -- can be taken to mean (a) pi/4 if integrated on the interval 0 < x < 1, or (b) space and time are separate dimensions, which is what Minkowski noticed and Einstein didn't. But by itself, THE EQUATION MEANS PRECISELY NOTHING -- for that, you must have ideas.

If you possessed the intellectual integrity of the average 12-year-old, you would realize that using the same words as Ernest Hemingway doesn't make you a great writer, and using the same equations as Einstein doesn't make you an original thinker. That requires ideas, not equations.

I post this for the benefit of other readers, who unlike you might have some depth of understanding, some grasp of the relation between ideas and equations.

Reply on news.ycombinator.com