Live data from Hacker News

What does “Undecidable” mean, anyway

buttondown.com

111–120 of 196 posts

Re: What does “Undecidable” mean, anyway

#111
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…

I still think what I said was correct.

> On the other hand, undecidable has a sharper meaning in computation contexts as well as constructive logics without excluded middle. In these cases we can comprehend the “reachability” of propositions. A proposition is not true or false, but may instead be “constructively true”, “constructively false”, or “undecidable”.

Yes, but that just means that independence/undecidability depend on the proof system, as I said before. So when using a constructive proof system, more statements will turn out to be undecidable/independent of a theory than with a classical one, since the constructive proof system doesn't allow non-constructive proofs, but the classical one does.

Re: What does “Undecidable” mean, anyway

#112
post #59

One of my favorite insights is that the existence of undecidable problems is the same thing as the uncountability of real numbers. Too bad the author didn't get into it.

...which is the same thing as Rice's theorem, and many other mind-bending results. It's all diagonalization under the hood =)

Re: What does “Undecidable” mean, anyway

#113

Earlier quoted context omitted.

Turing machine works going left or right writing/reading on a tape of 1s and 0s. Your CPU works on RAM writing and reading 1s and 0s. CPU in principle isn't that different and is largely just using a more sophisticated instruction set. Move 5 vs right right righy right right. swap vs read, write, right, write. etc Definitely not necessary for programming but it's not some completely theoretical mumbo jumbo. Moreover…

If the only principle you look at is "does this compute?" then they're not that different. Otherwise they're about as far apart as you can get. A Turing machine (at least one that isn't designed in some super wacky way to prove a point) has a few bits of internal state and no random access memory. If you want RAM you have to build a virtual machine on top of the Turing machine. If you try to program it directly it's…

Turing machine in essence is a finite state machine + memory (the tape) + some basic instructions for reading and writing to the memory.

Its a very simple, rudimentary computer, not some completely abstract mathematical object, which was what I was responding to.

With universal turing machines, its not difficult to start writing composable functions, like an assembly instruction set, adders, multipliers, etc.

TMs certainly arent fundemental, but when you look at TMs, lambda calculus and understand why they are equivalent, wouldnt you say you gain an understanding of what is fundamental? Certainly constructions like for loops, the stack etc are not fundamental, so youd want to go deeper in your study of languages

Re: What does “Undecidable” mean, anyway

#114
post #109
post #99

Earlier quoted context omitted.

The complaint is that Hillel is providing an intuitive explanation but that intuition is clearly faulty, as demonstrated by two of the examples he gave. P.S., you can run that proof finding algorithm (iterate through every candidate proof one by one and check for validity) for proofs of finite length in general, not just some fixed finite length. Where the halting oracle comes in is that you can use it to check wheth…

> for proofs of finite length in general, not just some fixed finite length. For a brute force proof finder, for your program to be guaranteed to finish in theory, you have to pick a length. So it is fixed. Ofc you can choose whatever length you want. But you don't have that constraint with the halting oracle. Perhaps we're saying the same thing?

For the program to be guaranteed to finish in theory, all that is required is that a valid proof exists. You don't have to pick a length in advance - the program just has to keep trying proofs of progressively longer lengths.

Re: What does “Undecidable” mean, anyway

#115
post #102
post #73

Any deterministic system with a finite number of states is decidable, in the halting problem sense. Either it halts or repeats a state. The halting problem only applies for infinite memory. Now, there are finite state systems where the halting problem is arbitrarily hard. But that's not undecidability. That's complexity. That's a problem in the space where P=NP lives. The article does not make this distinction, and i…

The halting problem applies also for finite-but-unbounded memory. If you give me a decider that can tell me for any program with a state space up to size N whether it halts or not, then I will be able to produce another program with a larger state space and which then your decider won't be able to decide. This new program doesn't use infinite space. Just more than your decider can handle. You can't produce a single d…

That doesn't sound right. All my decider needs to do is wait for a repeated state (no halt) or a halt. If the state space is finite then one of these is guaranteed to happen.

Re: What does “Undecidable” mean, anyway

#116

Earlier quoted context omitted.

> Definitely not necessary for programming but it's not some completely theoretical mumbo jumbo. While I'm a big fan of teaching theory, I regret to inform you that the Turing machine is kind of completely theoretical mumbo jumbo. The theoretical equivalent of the modern processor is the Von Neumann machine. Certainly there is a direct connection to be made to the Turing machine, as all computation can be framed as a…

I'm not sure what were arguing to be honest. You definitely don't need to understand Turing machines to understand how computers work, and certainly not how to do programming. But as far as understanding computer science, computational theory, etc certainly you'd want to study Turing machines and lambda calculus. If you were say, writing a programming language, it would be nice to understand the fundamentals. I mean,…

Suppose I were to teach theoretical CS using only RAM models of computation, with no reference to Turing Machine tapes. Would there be any downside to doing this, pedagogically? (Other than, of course, the backward compatibility concern of students being able to engage with existing literature, which is the main reason this isn't done I think)

Re: What does “Undecidable” mean, anyway

#117
post #102

Earlier quoted context omitted.

The halting problem applies also for finite-but-unbounded memory. If you give me a decider that can tell me for any program with a state space up to size N whether it halts or not, then I will be able to produce another program with a larger state space and which then your decider won't be able to decide. This new program doesn't use infinite space. Just more than your decider can handle. You can't produce a single d…

That doesn't sound right. All my decider needs to do is wait for a repeated state (no halt) or a halt. If the state space is finite then one of these is guaranteed to happen.

And how does your decider recognize that a state has been attained twice? If I make the input system large enough then you don't have enough space in your decider to save all the states which it has observed.

Re: What does “Undecidable” mean, anyway

#118
post #117

Earlier quoted context omitted.

That doesn't sound right. All my decider needs to do is wait for a repeated state (no halt) or a halt. If the state space is finite then one of these is guaranteed to happen.

And how does your decider recognize that a state has been attained twice? If I make the input system large enough then you don't have enough space in your decider to save all the states which it has observed.

What do you mean "space in your decider"? My decider takes finite but unbounded memory, same as the machine it's deciding.

Re: What does “Undecidable” mean, anyway

#119
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…

> The result becomes less weird when you realize that that almost all functions from string -> boolean are not expressible as a program.

I think this is one of those cases where a maths background makes computer science much easier. It only takes enough calculus to get you to entry level differential equations before you’re confronted with the fact that most functions ℝ → ℝ aren’t elementary functions (or admit any closed-form expression at all). In a certain sense, “program” is really just a weird word for “closed-form expression”.

Re: What does “Undecidable” mean, anyway

#120
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.

> It's better to say that some functions like "does this program halt?" simply don't exist.

Let f : (p: String) -> Boolean equal the function that returns True if p is a halting program, and False otherwise

Post reply on HN