What does “Undecidable” mean, anyway
buttondown.com
What does “Undecidable” mean, anyway
1–10 of 196 posts
Re: What does “Undecidable” mean, anyway
#2The boost was how easy it is to find the mechanism to some abstractions. And instead of being those amazing and complex tools that you have to use carefully, they've become easier to use and reason about. I would say very much like the study of forms, value, and perspectives for an artist, or music theory for a musician. It just makes everything easier. Especially the understanding about automata (regex), context-free grammar (programming language), and the Turing machine (CPU).
Re: What does “Undecidable” mean, anyway
#3The problem that's usually not told to kids is that decidability has different sort of implications to classical mathematics and constructive mathematics. Since most undergrad programs only teach mainstream math (i.e. classical) and don't even mention constructive logic, decidability becomes a black magic situation for some confused students.
Here's the crucial part: decidability really only has material impact on our reasoning if we're in some kind of constructive setting. Undecidability does not and cannot have any impact on the results of classical mathematics, period, but it does have effect on the proofs of those classical theorems. It can also have impact on classical mathematics if we're reasoning classically but describing results in constructive settings (e.g. this is what happens when we do computability theory in classical mathematics).
In short, classically we're always allowed to work around undecidability by using an "oracle". But it can be important to state that we can only do it this way (similar to how we can state the need to use the axiom of choice).
One way to re-phrase Aristotle's law of excluded middle (forall P, P or not P) is to say: "every relation is decidable" which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd...
This doesn't mean in classical mathematics every relation "literally" is decidable. Classical mathematics can still study constructive settings by creating a computational model (e.g. Turing Machine model). But it does mean that in classical mathematics every relation effectively is indistinguishable from decidable relations since given a statement like "Program P will halt" you are always allowed to say "either (program P will halt) or (program P won't halt)" regardless of our impossibility to prove one of the cases in general.
Also note that we call this kind of constructive reasoning "neutral constructive mathematics" which is when we operate in a constructive reasoning setting (like Agda's type theory above) but allow ourselves to say things like "AxiomOfChoice implies ExcludedMiddle" etc, read: https://ncatlab.org/nlab/show/neutral+constructive+mathemati...
Re: What does “Undecidable” mean, anyway
#4One of the biggest boost to my SWE career was studying theory of computation and programming languages theory. My major was electronic engineering, so I didn't touch those at the university. But I use some books to at least grasp the introductory knowledge. The boost was how easy it is to find the mechanism to some abstractions. And instead of being those amazing and complex tools that you have to use carefully, they…
Re: What does “Undecidable” mean, anyway
#5Re: What does “Undecidable” mean, anyway
#6> The halting problem says that we cannot create an algorithm that, when applied to an arbitrary program, tells us whether the program will halt or not.
Or more simply:
No program can tell whether any program will halt or not.
Re: What does “Undecidable” mean, anyway
#7Are there classes of intelligence? Are there things that some classes can and cannot do? Is it a spectrum? Is the set of classes countable? Is it finite? Is there a maximum intelligence? One can dream…
Re: What does “Undecidable” mean, anyway
#8> I often see the halting problem misconstrued as "it's impossible to tell if a program will halt before running it." This is wrong. > The halting problem says that we cannot create an algorithm that, when applied to an arbitrary program, tells us whether the program will halt or not. Or more simply: No program can tell whether any program will halt or not.
I found this bit was really helpful:
“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.”
Re: What does “Undecidable” mean, anyway
#9One of the biggest boost to my SWE career was studying theory of computation and programming languages theory. My major was electronic engineering, so I didn't touch those at the university. But I use some books to at least grasp the introductory knowledge. The boost was how easy it is to find the mechanism to some abstractions. And instead of being those amazing and complex tools that you have to use carefully, they…
Would you have book recommendations / resources to share?
Language Implementation Patterns by Terence Parr. It avoids the theory in other books, going for a more practical approach.
Then it was just trying a lot of programming paradigms like functional programming with Common Lisp and Clojure, logic programming with Prolog, array and stack programming with Uiua. And reading snippets of books and papers. It was chaotic.
But the most enlightening lesson was: Formalism is the key. You define axioms, specify rules and as long as you stay consistent, it's ok. The important thing is to remember the axioms and understanding the rules.
[0]: https://www.youtube.com/playlist?list=PLUl4u3cNGP60_JNv2MmK3...
Re: What does “Undecidable” mean, anyway
#10I sometimes wonder if the concept of “intelligence” is going to benefit from a formal model the way “computation” benefited from Turing Machines. Are there classes of intelligence? Are there things that some classes can and cannot do? Is it a spectrum? Is the set of classes countable? Is it finite? Is there a maximum intelligence? One can dream…