Live data from Hacker News

What does “Undecidable” mean, anyway

buttondown.com

81–90 of 196 posts

Re: What does “Undecidable” mean, anyway

#81
I think it helps to understand my namesake's Incompleteness Theorem[0]. They are actually connected [1,2]

  1) no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers. 
  For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.

  2) the system cannot demonstrate its own consistency.
Any axiomatic system will have true statements that are unprovable. Which means basically any system of logic. If you've made an assumption you'll end up with this. You're always making assumptions, even if you don't realize it. It's usually a good idea to figure out what those are.

I hear a lot of people say "from first principles". If you're not starting from your axioms, you're not starting from first principles. Think Carl Sagan making a pie from scratch.

[0] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

[1] https://scottaaronson.blog/?p=710

[2] https://cstheory.stackexchange.com/questions/10635/halting-p...

Re: What does “Undecidable” mean, anyway

#82
post #79

"This to me is a strong "intuitive" argument for why the halting problem is undecidable: a halt detector can be trivially repurposed as a program optimizer / theorem-prover / bcrypt cracker / chess engine. It's too powerful, so we should expect it to be impossible." I don't buy this. Bcrypt cracking and solving chess is easy already if you don't care about runtime complexity (both have rather trivial finite -- albeit…

What do you not buy? He's saying it could be used to do anything for free. He gave four examples. The first two don't have general solutions, and never will. You don't like the last 2 examples because we have algorithms for them, ok. It doesn't undermine the argument. And in any case both things were developed with effort and ingenuity... they weren't spit out of a halting problem calculator.

Re: What does “Undecidable” mean, anyway

#83
post #82
post #79

"This to me is a strong "intuitive" argument for why the halting problem is undecidable: a halt detector can be trivially repurposed as a program optimizer / theorem-prover / bcrypt cracker / chess engine. It's too powerful, so we should expect it to be impossible." I don't buy this. Bcrypt cracking and solving chess is easy already if you don't care about runtime complexity (both have rather trivial finite -- albeit…

What do you not buy? He's saying it could be used to do anything for free. He gave four examples. The first two don't have general solutions, and never will. You don't like the last 2 examples because we have algorithms for them, ok. It doesn't undermine the argument. And in any case both things were developed with effort and ingenuity... they weren't spit out of a halting problem calculator.

Having a decision algorithm does not make a computation free. It may take exponential time in the input size, doubly exponential time, some time involving Graham's number, ... etc. It may also take up an unreasonable amount of space. Indeed, some problems have such complex algorithms that you should expect the universe to end before the answer is determined and/or the computing device is doomed to collapse into a black hole, making the answer irretrievable.

So the blog post's claims that a hypothetical halting algorithm would solve anything "overnight" are exaggerated and naive.

Re: What does “Undecidable” mean, anyway

#84
post #76
post #74

Earlier quoted context omitted.

I wonder if this is a correct argument. A function string -> boolean is always expressible? Simply because the set of all possible mappings from all possible finite strings to booleans is countable. It's better to say that some functions like "does this program halt?" simply don't exist.

`S = {str -> bool}` is actually uncountable. `S` is isomorphic to the power set (set of all subsets) of `str`, and `2^str` is at least as big as the set of real numbers, as any real number (like π) can be mapped to the set of string prefixes (like `{"3", "3.1", "3.14", ...}`). Since the reals are uncountable, so is `2^str` and `S`.

> `S` is isomorphic to the power set

D'oh. I missed that.

Re: What does “Undecidable” mean, anyway

#85
post #83
post #82

Earlier quoted context omitted.

What do you not buy? He's saying it could be used to do anything for free. He gave four examples. The first two don't have general solutions, and never will. You don't like the last 2 examples because we have algorithms for them, ok. It doesn't undermine the argument. And in any case both things were developed with effort and ingenuity... they weren't spit out of a halting problem calculator.

Having a decision algorithm does not make a computation free. It may take exponential time in the input size, doubly exponential time, some time involving Graham's number, ... etc. It may also take up an unreasonable amount of space. Indeed, some problems have such complex algorithms that you should expect the universe to end before the answer is determined and/or the computing device is doomed to collapse into a bla…

"Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist.

> So the blog post's claims that a hypothetical halting algorithm would solve anything "overnight" are exaggerated and naive.

I agree "overnight" is misleading in this context. However, I am fairly sure the author is aware of the point you are making.

Re: What does “Undecidable” mean, anyway

#86

Earlier quoted context omitted.

I'd recommend codifying such axioms, rules and grammar into a domain-specific language, and then writing your logic in that DSL. It will keep things consistent and allow newcomers to quickly understand the domain, enabling them to contribute without need for deep institutional knowledge.

That's one of the foundation of Domain-Driven Design. First you try to comes up with a glossary (aka your axioms). Then you'll notice that some have relations with each other and some terms may have the same name, but refers to two different concepts (or two parts of the same whole). So now you will have your boundaries. Then you try to make a subdomain internally consistent. But you still have to communicate with th…

Exactly. Getting DDD to be implemented and followed in past orgs has been difficult but it pays in spades. It's hard enough to push startup engineering teams to use consistent terminology, much less adopt DDD.

I do find it sometimes can lead to less verbose code even in OOP, because it makes logic more focused and DRY. It certainly can greatly reduce the amount of bugs in large codebases.

Re: What does “Undecidable” mean, anyway

#88
post #74
post #65

This is a really nice explanation of decidability. One extra thing it might be worth mentioning is that there are many more functions `f : string -> boolean` then there are programs that implement those functions. When I first encountered this topic I had trouble intuitively understanding how there could not exist an `IS_HALTING` function when it is also just a function that takes in a string (representing a program…

I wonder if this is a correct argument. A function string -> boolean is always expressible? Simply because the set of all possible mappings from all possible finite strings to booleans is countable. It's better to say that some functions like "does this program halt?" simply don't exist.

I think you are experiencing the same confusion I felt when I first started thinking about the difference between a program and a function.

The set of all possible mapping from all possible finite strings to booleans is definitely *not* countable.

What I (and the article) mean by a "function" `f : string -> boolean` here is any arbitrary assignment of a single boolean value to every possible string. Let's consider two examples:

1. Some "expressible" function like "f(s) returns True if the length of s is odd, and returns False otherwise".

2. Some "random" function where some magical process has listed out every possible string and then, for each string, flipped a coin and assigned that string True if the coin came up heads, and False if it came up tails and wrote down all the results in a infinite table and called that the function f.

The first type of "expressible" function is the type that we most commonly encounter and that we can implement as programs (i.e., a list of finitely many instructions to go from string to boolean).

Nearly all of the second type of function -- the "random" ones -- cannot be expressible using a program. The only way to capture the function's behavior is to write down the infinite look-up table that assigns each string a boolean value.

Now you are probably asking, "How do you know that the infinite tables cannot be expressed using some program?" and the answer is because there are too many possible infinite tables.

To give you an intuition for this, consider all the way we can assign boolean values to the strings "a", "b", and "c": there are 2^3 = 8. For any finite set X of n strings there will be 2^n possible tables that assign a boolean value to each string in X. The critical thing here is that 2^n is always strictly larger than n for all n >= 1.

This fact that there are more tables mapping strings to boolean than strings still holds even when there are infinitely many strings. What exactly we mean by "more" here is what Cantor and others developed. They said that a set A has more things than a set B if you consider all possible ways you can pair a thing from A with a thing from B there will always be things in A that are left over (i.e., not paired with anything from B).

Cantor's diagonalization argument applied here is the following: let S be the set of all finite strings and F be the set of all functions/tables that assigns a boolean to each element in S (this is sometimes written F = 2^S). Now suppose F was countable. By definition, that would mean that there is a pairing that assigns each natural number to exactly one function from F with none left over. The set S of finite strings is also countable so there is also a pairing from natural numbers to all elements of S. This means we can pair each element of S with exactly one element of F by looking up the natural number n assigned to s \in S and pairing s with the element f \in F that was also assigned to n. Crucially, what assuming the countability of F means is that if you give me a string s then there is always single f_s that is paired with s. Conversely, if you give me an f \in F there must be exactly one string s_f that is paired with that f.

We are going to construct a new function f' that is not in F. The way we do this is by defining f'(s) = not f_s(s). That is, f'(s) takes the input string s, looks up the function f_s that is paired with s, calculates the value of f_s(s) then flips its output.

Now we can argue that f' cannot be in F since it is different to every other function in F. Why? Well, suppose f' was actually some f \in F then since F is countable we know it must have some paired string s, that is, f' = f_s for some string s. Now if we look at the value of f'(s) it must be the same as f_s(s) since f' = f_s. But also f'(s) = not f_s(s) by the way we defined f' so we get that f_s(s) = not f_s(s) which is a contradiction. Therefore f' cannot be in F and thus our premise that F was countable must be wrong.

Another way to see this is that, by construction, f' is different to every other function f in F, specifically on the input value s that is paired with f.

Thus, the set F of all functions from strings to boolean must be uncountable.

Re: What does “Undecidable” mean, anyway

#89
post #52
post #15

There are at least two meanings of "undecidable". The one, from computer science, is discussed in the blog post. The other, from formal logic, is a synonym to "independent". A proposition (not property) is independent of some axiomatic theory with respect to a proof system, if and only if the proposition can neither be proved nor disproved in that theory. For example, the continuum hypothesis is independent of ZFC. A…

Independent and undecidable aren't quite the same, even in formal logic. Or rather, sometimes they are but it’s worth being specific. A proposition P being independent of a theory T means that both (T and P) and (T and not P) are consistent. T has nothing to say about P. This may very well be what Gödel was indicating in his paper. On the other hand, undecidable has a sharper meaning in computation contexts as well a…

Could I say that 'P is Undecidable' is defined as: It is False that {There exists T such that [(T and P) and (T and not P) are both consistent]}?

Re: What does “Undecidable” mean, anyway

#90
post #85
post #83

Earlier quoted context omitted.

Having a decision algorithm does not make a computation free. It may take exponential time in the input size, doubly exponential time, some time involving Graham's number, ... etc. It may also take up an unreasonable amount of space. Indeed, some problems have such complex algorithms that you should expect the universe to end before the answer is determined and/or the computing device is doomed to collapse into a bla…

"Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist. > So the blog post's claims that a hypothetical halting algorithm would solve anything "overnight" are exaggerated and naive. I agree "overnight" is misleading in this context. However, I am fairly sure the author is aware of the point you are making.

> "Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist.

Right.

But brute force solvers for bcrypt and chess are already "free" in the sense of thought, cleverness, insight. We already have the "everything" algorithm: iterate through all possible solutions in O(2^n) time and pick the best one.

A halting solver gains us nothing in these scenarios.

(The code for scoring a solution is the same code that would need to go into the halting solver. For bcrypt it's checking if the input matches, for chess it's the number of turns until checkmate.)

Post reply on HN