11 ms·

What does “Undecidable” mean, anyway

156 points by BerislavLopac 1y ago

aatd86 1y ago
And here I thought it was simply about a system of equations solving down to a single solution (decidable). As opposed to having too many free variables.
skydhash 1y ago
One 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'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).
- Gruzzy 1y ago
  Would you have book recommendations / resources to share?
  - skydhash 1y ago
    Introduction to the Theory of Computation by Michael Sipser. There's also his course based on the book on YouTube[0]. 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_JNv2MmK3wkOt9syvfQWY https://www.youtube.com/playlist?list=PLUl4u3cNGP60_JNv2MmK3...
    - soulofmischief 1y ago
      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.
      - skydhash 1y ago
        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 the other subdomains (to enact actions and query data). These communications are equally important as each subdomain. The hope is to have something that reflects the business domain, especially the cost of changes. Something that's easy/hard to change in the business should be easy/hard to change in the code, With OOP, this often results in verbose code, because each view of the data (which has its own rules) has its own class. With FP, because you often use more primitive data structures, it's easier to commute between subsets of data.
        soulofmischief 1y ago
        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.
  - nixpulvis 1y ago
    Might be hard to approach but my favorite is Pierce's "Types and Programing Languages": https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ (known as TAPL). Was grateful to take a graduate level class using it in college.
    - skydhash 1y ago
      TAPL is nice, and also very dense. I haven't fully read it, but my current understanding is the follow: Both the Turing Machine and the lambda calculus only describes how to act on data. They don't actually describes what the data is. So you can craft an algorithm that works well, but it can be supplied with the wrong type of data and it will goes haywire. Your only recourse is to trust the user of your algorithm. What type does is to have a set of classes of data, then have rules between those classes. You then annotate your code with those classes (combining them if it's possible) and then your type system can verify that the relations between them hold. To the type system, your program is data.
      - lanstin 1y ago
        I think undecidable means more like there are classes of problems for which there is no algorithm (that runs in finite time) can give the answer to. To square N, there is an algorithm that always works. To see if the Turing machine N halts in input M, there is not such an algorithm. The halting problem is undecidable. There is a clever way to encode Turing machines into Diophantine equations, so Diophantine equations (linear equations
    - tel 1y ago
      I really like TAPL but would recommend Harper’s Practical Foundations of Programming Languages (PFPL) first (though skip the first 2 chapters I think?). https://www.cs.cmu.edu/~rwh/pfpl.html https://www.cs.cmu.edu/~rwh/pfpl.html It’s far more directed than TAPL, so I think it’s easier to read from start to finish. TAPL feels better as a reference.
  - downboots 1y ago
    Mertens Theory of Computation
    - Jtsummers 1y ago
      > Mertens Theory of Computation No such book exists. Do you mean The Nature of Computation by Moore and Mertens?
      - downboots 1y ago
        Sure, M&M's
        deleted 1y ago
        [deleted]
- Aicy 1y ago
  Really? I studied it in my undergrad degree, and since then have worked as a SWE and not found it relevant at all really
  - skydhash 1y ago
    It's the recursive nature of it. Almost any program can be written in a DSL that solves the class of problem that the program solves. So if you consider the user stories of your project as that class of problem, you can come up with with a DSL (mostly in form of pseudocode) that can describe the solution. But first you need to refine the terms down to some primitives (context free grammar). You then need to think about the implementation of the execution machine. which will be a graph of states (automata). The transition between the states will be driven by an execution machine. The latter needs not be as basic as the Turing machine. But often, you do not need to do all these stuff. You can just use common abstractions like design patterns, data structures, and basic algorithms to have a ready made solution. But you still have to compose them and if you understand how everything works, it's easier to do so.
  - drdrey 1y ago
    it depends what you're working on, if you do any form of program analysis (security, compiler stuff) you bump into undecidability everyday
- nitwit005 1y ago
  I have to vote the opposite direction. I don't think it's ever been relevant. As an example, A practical walk through of what a simple CPU is doing was quite useful for getting the idea of what's going on. The concept of a Turing machine, which was originally intended for mathematical proofs, was not.
  - tialaramex 1y ago
    I completely disagree. For example understanding the theory gives me a very powerful bullshit detector because entire categories of problem which might sound merely difficult are in fact Undecidable. Knowing that the actual regular expressions can be recognised by a finite automaton but PCRE and similar "LOL, just whatever neat string matching" extensions cannot means you can clearly draw the line and not accidentally make a product which promises arbitrary computation for $1 per million queries. I agree that understanding something of how the CPU works is also useful, but it's no substitute for a grounding in theory. The CPU is after all obliged to only do things which are theoretically possible, so it's not even a real difference of kind.
  - skydhash 1y ago
    The CPU is an implementation of theory. It just happens that the realization of several axioms in the Turing machine is realizable physically. And the rest hold true. The nice thing with notation is that they're more flexible than building/creating/executing the thing they describe.
    - nitwit005 1y ago
      If you look back at the history, CPUs were often designed for specific tasks, and some of the early ones lacked conditional jumps that you'd normally consider nessesary for a Turing machine. We've made them more general purpose as that sells better, not because people cared about making Turing machines.
      - skydhash 1y ago
        Jump is not required for a Turing machine, only being able to move to a specific case by sliding. Conditional jump is an abstraction. Just like looping.
- deleted 1y ago
  [deleted]
- DonaldPShimoda 1y ago
  > One of the biggest boost to my SWE career was studying theory of computation and programming languages theory. I totally agree with you. > My major was electronic engineering, so I didn't touch those at the university. Unfortunately, ever more computer science graduates lack the same belief, even if they go to "top" university programs. Of course, I think part of the problem is the way the material is presented; "learn this to pass the exam" without fundamental motivation is pretty much always a bad set-up to get students interested. But, speaking anecdotally, a large part also seems to be a semi-recent surge of undergraduate students who genuinely believe that their academic career is nothing more than a hurdle to be muddled through in service of getting a piece of paper that lets them get a high-paying, low-labor-intensity job. They just don't engage with theory-focused material beyond what's strictly necessary to graduate, and then they dump the thoughts from their minds the second the semester is over. This manifests in all sorts of ways, but a common one is undergrads telling one another how little their professors know about the "real world" because they use (not even that) outdated technology in their lectures. Or maybe the profs use some less popular language and the students think of it as a waste of time. There's comparatively little self-motivation among modern CS students, where historically I think there was rather a lot. I suppose I'm not really going anywhere specific with this other than complaining, so maybe I can ask: What do you think it was that helped you realize that learning fundamental theory would be beneficial? (I don't have any indication that you were the same kind of student as these that I mention, since you were in a different major altogether, but I'm always looking for insights to help motivate students to study theory more, and insights can come from anywhere.)
gnulinux 1y ago
The reason decidability makes no or very little sense to tons of CS or Math majors is because the logical basis of decidability is almost never explained in school. Even if you're in a logic/computability class you likely won't get a very concrete explanation, unless you're in a Philosophy of Math class. The 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.ExcludedMiddle.html 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+mathematics https://ncatlab.org/nlab/show/neutral+constructive+mathemati...
- LPisGood 1y ago
  I was with you until here: > which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd... Why did you randomly shoehorn in homotopy type theory? Maybe I’m overreacting to this, but the only person I’ve ever known to shoehorn homotopy type theory into largely unrelated discussion has left quite a poor impression for me.
dunkeltaenzer 1y ago
The problem there is overlap between fractal and non-fractal spaces. Our Math and Logic were created to work in non-fractal spaces. Whenever we cross the boundaries into fractal spaces (recursion in programming, for example), our math and logic have a tendency to explode, because there are infinities flying around everywhere and things stop to be guaranteed to be deterministic, because you have to assure determinability for several dimensions of infinities. You have to accept certain quantum rules, in those spaces. And being deterministic isn't compatible with quantum rules. That's why quantum physics is struggling so badly to get rid of all those infinities flowing in with every new dimension they add to the wave function. That thing wasn't designed for fractal spaces. So it becomes harder and harder to contain all those leaking infinities into a workable magic ball. We stored most of our fractal remembrance in pictures for a reason. Much easier to draw fractals than to compute them with math, not made for fractal spaces
paulddraper 1y ago
> 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.
- cobbzilla 1y ago
  I really enjoyed the author’s explanation of undecidability. 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.”
  - wat10000 1y ago
    I'm not sure about that. These are also easily solved with a general-purpose CPU, if you don't care about running time. And there's nothing that says that a halt detector would be fast. The impossibility result is more interesting than just "it would take a million times the age of the universe to complete if every atom in it were put to the sole purpose of computing it" as we often see with cryptography.
    - hwayne 1y ago
      That's not necessarily true. Consider the program `x := 4; loop {if !sum_of_two_primes(x) {return true}; x += 2}`. If we run this on a general purpose CPU, this will halt if and only if Goldbach's conjecture has a counterexample. Otherwise it will run forever. So even if a working halt detector takes 14 million billion years, it will definitely tell us if the conjecture is true or not. Whereas if the general purpose CPU is still running after that time, we still have no way of knowing whether it's because it's going to run forever or if it simply hasn't reached the first (ludicrously large) counterexample.
      - 1y ago
brap 1y ago
I 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…
- ryandamm 1y ago
  Purely intuitively, it seems like there should be a connection between the two (computation and intelligence). But I have not formally studied any relevant fields, I would be interested to hear thoughts from those who have.
  - brap 1y ago
    I was thinking the same thing, maybe a level above in the Chomsky Hierarchy…
  - wat10000 1y ago
    The known laws of physics are computable, so if you believe that human intelligence is purely physical (and the known laws of physics are sufficient to explain it) then that means that human intelligence is in principle no more powerful than a Turing machine, since the Turing machine can emulate human intelligence by simulating physics. If there's a nonphysical aspect to human intelligence and it's not computable, then that means computers can never match human intelligence even in theory.
    - deleted 1y ago
      [deleted]
- bawolff 1y ago
  Philosophers have been trying to define what it means to be conscious since forever. I think that is informally what you mean here. If you just mean what problems can it solve, and how quickly, we already have a well developed theory of that in terms of complexity classes -https://complexityzoo.net/Complexity_Zoo https://complexityzoo.net/Complexity_Zoo
kazinator 1y ago
An undecidable problem in the Turing computational model is this: it is a problem for which no algorithm exists which can ] decide every input case. This doesn't preclude some input cases from being decided. What happens it that every attempt at making an algorithm for an undecidable problem will run into two issues: there will be input cases for which an answer exists, but for which the algorithm either gets into an infinite loop/recursion or else produces the wrong answer. Why would a decision procedure ever yield the wrong answer? That is due to mitigations of the infinite looping problem. To avoid becoming trapped by the input cases that trigger infinite calculations, the algorithm has to resort to some mechanism of arbitrarily stopping, without having reached the decision. Like for instance by capping the number of steps executed. But when that situation is reached, the correct answer is not yet known. The algorithm can return "yes" or "no", but that will be wrong half the time. Or it can report "failed", which is always incorrect, not matching either "yes" or "no". A classic example of an undecidable problem is the Halting Problem: the question of whether a given program (or algorithm) P, operating on an input I, will halt or not. So the space of inputs for this problem is <P, I> pairs. The input space is infinite, but all instances in that space are finite: finite length programs P operating on finite inputs I. The problem is that just we have a given finite P and finite I doesn't mean that halting can be decided in finite steps. No matter how cleverly someone constructs a halting decider, it is easy to produce test cases which will cause that decider to either stop and produce the answer (decide incorrectly) or else iterate or recurse forever. (Demonstrating how such test cases can be produced for any decider is at the heart of a popular proof which shows that halting is undecidable.) The Halting Problem is at the center of decidability, because every decision procedure of any kind (not necessarily a decision in the Halting Problem) is a <P, I> pair. For instance the decision whether a list of N integers is sorted in ascending order is a <P, I> pair. P is an algorithm for sweeping through the integers to check that they are ordered, and I is some list of integers. Since it is a <P, I> pair, it is in the domain of the Halting Problem. P is not in the Halting Problem: P is in the domain of processing a list of integers. But <P, I> is an input case of the Halting Problem: does list-processing algorithm P halt on the list of integers I. The upshot is that when we are solving some decision problem by running an algorithm, which is taking long, and we ask "will this decision terminate, or is it in a loop?" we are then posing another problem, and that problem is an input case of the Halting Problem. And we know that the Halting Problem is undecidable. What that means is that if we happen to be calculating a problem which is undecidable, the Halting Problem informs us that there is no guaranteed shortcut for us to know whether our calculation is hung, or whether it is working toward halting. When we try to apply "meta reasoning" about an algorithm that appears stuck, our reasoning itself may also get stuck. We may have to give up, cut the investigation short, and report "we don't know". I.e. we don't know whether or not our decision program is forever stuck or working toward the solution. Undecidability is a somewhat important topic to a software engineer for the following reasons. In your career you may from time to time encounter requirements that call for a the calculation of an undecidable problem. If you know can recognize it, you can take action to revise the requirements. For instance, perhaps you can negotiate the requirements such that it's acceptable for the decision to be incorrect, erring on one side of the other (false positive or false negative). Equivalently, maybe some inputs can be rejected before the algorithm, leaving a decidable subset. You may have a People Problem there because the requirements are coming from non-computer-scientists who don't know about decidability; you have to be careful not to make it look like you are refusing to do hard work due to not believing in your skill, or laziness. As an example, we could use the Halting Problem itself. Say you work on some virtual machine for sandboxing untrusted programs and your boss says, can we detect programs which loop infinitely, and not run them at all? Just reject them? If you know about undecidability, you can tell your boss, no, that is an undecidable problem! What we can do is limit the number of instructions or run time, which will stop some programs that are not looping infinitely but are just taking long to calculate something. Or here is another thing we can do instead; only admit programs written in a language that is not Turing Complete: has only bounded loops and no recursion. The sandbox compiler can reject all others. Or we can allow recursion but stacked recursion only (not tail) and limit the depth. Of course, that's just an easy example; undecidability can sneak into the requirements in forms that are not immediately recognizable.
johnea 1y ago
I don't know, I can't decide...
- deleted 1y ago
  [deleted]
deleted 1y ago
[deleted]
cubefox 1y ago
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. Another way to express this is to say that the continuum hypothesis is undecidable (in ZFC). Kurt Gödel used this sense of "undecidable" in his famous paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I". ("On formally undecidable propositions in Principia Mathematica and related systems I") Are these two meanings of "undecidable" related in some way? I guess probably yes. But I'm not sure how.
- ttctciyf 1y ago
  > Are these two meanings of "undecidable" related I can't claim to answer this, but you might like to look at A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory[0] which (amongst other interesting things) does discuss the proposition "ZFC is consistent", which is independent from ZFC, in terms of a Turing Machine which enumerates all possible proofs in ZFC and halts when it finds a contradiction (e.g. a proof of 0=1). But I don't think there's a simple equivalence here, all the same. The logician's undecidable is always relative to a set of axioms, whereas the question of whether a property of strings can be decided by some TM doesn't place any constraints on the TM, which is to say the deciding TM is not required to, nor prohibited from, implementing any particular axiom set. (It's tempting to try and show "provable in ZFC" to be a (CS)undecidable property by having a TM enumerate ZFC proofs and halt on finding a proof or disproof of the input string, and imagine the TM running forever when given a statement of the Continuum Hypothesis. But the TM could proceed by other means - for example [1] shows a proof of CH's independence in a theorem prover, so that a TM incorporating this construction could indeed reject CH statements as unprovable in ZFC. Which is not to say "ZFC-provable" *isn't* (CS)undecidable, just that showing this isn't as simple as constructing a ZFC-proof-enumerator and giving it the CH as input.) 0: https://arxiv.org/abs/1605.04343 https://arxiv.org/abs/1605.04343 1: https://arxiv.org/abs/2102.02901 https://arxiv.org/abs/2102.02901
- tel 1y ago
taeric 1y ago
I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. It isn't that the drawing doesn't exist. It is that you still have some freedom in how long certain parts could be. Crucially, not all. It could be that parts of the drawing are indeed fully specified. Same can go with programs. You can constrain parts of it enough that you can answer some pretty specific questions. And similar to how a drawing with fewer lines is easier to constrain, a program that has restricted constructs can be easier to constrain.
- constantcrying 1y ago
  >I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. That is just solution theory of a non-linear system of equations. The solution space can have exactly one solution (fully constrained), more than one (under constrained) or zero (over constrained). To be honest I do not really see a connection.
  - taeric 1y ago
    I meant more as how to mentally model it in a way that can get someone across the line. My assertion is that caring about undecidability is almost certainly a waste of time for most people. That said, the reason we work in small chunks is often so that we can more easily answer questions about programs. Moving the graphical drawing and constraints over to a symbolic system also helps see how many symbols it can take to cover a simple system. Of course, the real reason for me thinking on this is that I'm playing with FreeCAD for the first time in a long time. :D
deleted 1y ago
[deleted]
- deleted 1y ago
  [deleted]
nialv7 1y ago
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.
- mreid 1y ago
  I had exactly the same reaction, which prompted me to write this comment: https://news.ycombinator.com/item?id=44122045 https://news.ycombinator.com/item?id=44122045
- bubblyworld 1y ago
  ...which is the same thing as Rice's theorem, and many other mind-bending results. It's all diagonalization under the hood =)
mreid 1y ago
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 plus its inputs) and outputs True or False depending on whether it halts or not. The argument in the article does a great job of showing that `IS_HALTING` cannot exist because it is in some sense "too powerful" but that means there is a mapping f : strings -> boolean that cannot be represented as a program, which seems weird if you've been programming for ages and every function you encounter is expressed as a program. The result becomes less weird when you realize that that almost all functions from string -> boolean are not expressible as a program. Why? Well there are countable many programs since there are only countably many finite length strings and every program, by definition, is a finite length string. However, there are uncountably many functions from string -> boolean since these functions map one-to-one to sets of strings (just let the set be all inputs that map to True) and the cardinality of the set of sets of strings is uncountable. This is essentially due to Cantor's diagonalization argument which shows you cannot put all elements in a set X into a 1-1 correspondence with all the subsets of X, even when X is countably infinite. This fact is at the heart of a lot of these computability results since it shows there is a gap between all functions (= any arbitrary subset of finite strings) and a program (= a finite string).
- cyberax 1y ago
  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.
  - hwayne 1y ago
    `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`.
gerdesj 1y ago
I'm not sure
graycat 1y ago
> What does “Undecidable” mean, anyway A big and relatively recent example is to take (1) the axioms of Zermelo-Fraenkel set theory and (2) the axiom of choice and ask if (1) can be used to prove or disprove (2). The surprising answer is "No", i.e., (1) cannot be used either to prove or disprove (2). So, can work with (1) and, whenever convenient, assume (2), continue on, and never encounter a problem. So, given (1), (2) is undecidable. The work was by Paul J. Cohen as at https://en.wikipedia.org/wiki/Paul_Cohen https://en.wikipedia.org/wiki/Paul_Cohen The field of research about what is undecidable also goes back to Kurt Gödel as at https://en.wikipedia.org/wiki/Kurt_G%C3%B6del https://en.wikipedia.org/wiki/Kurt_G%C3%B6del Another example, starting with (1), of an undecidable statement is the continuum hypothesis: There is no set whose cardinality is strictly between that of the integers and the real numbers. In simple terms, "cardinality" means that there is no set X that is too large to be put into 1-1 correspondence with the set of integers and too small to be put into 1-1 correspondence with the set of real numbers.
Animats 1y ago
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 it's important.
- ummonk 1y ago
  Yes, the article is clearly confused about the concepts, given its mention of bcrypt cracking and chess engines.
  - dmurray 1y ago
    Yes, I thought the article was really good until it got to that point. > 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.) A Turing machine can be trivially repurposed as a bcrypt cracker or chess engine (for the same definition of trivial the author is using), so if it's not intuitive that a computer can do this, then your intuition is wrong. Program optimizers and theorem provers also exist, of course, but in those cases the problems really are undecidable so no Turing machine is guaranteed to work on any given program or theorem.
    - bubblyworld 1y ago
      A solution to the Halting problem can be repurposed as a general-purpose theorem prover. The author is correct. You simply write a program that searches all possible valid proofs till it finds the one you are looking for (or maybe doesn't and runs forever). Then you check whether it halts with your Halting solution - if that returns true, you know that a proof exists, otherwise you know that one doesn't. In other words, you can use undecidability of first-order logic to prove undecidability of the Halting problem if you like, although it's a bit of a chicken-egg thing historically (I believe).
Aziell 1y ago
The first time I encountered the halting problem, I was honestly confused. I kept thinking there had to be another solution. But over time, I came to realize it wasn’t a technical issue ,it was about the limits of computation itself. This article explains the concept of undecidability really well. It breaks things down in a very practical way. That last part, about the limits of how we think, really hit me.
ummonk 1y ago
"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 exponential -- runtime algorithms), and it wouldn't be any easier to transform them into halting problems.
- jonahx 1y ago
  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.
  - cvoss 1y ago
    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.
    - jonahx 1y ago
      "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.
godelski 1y ago
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_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [1] https://scottaaronson.blog/?p=710 https://scottaaronson.blog/?p=710 [2] https://cstheory.stackexchange.com/questions/10635/halting-problem-uncomputable-sets-common-mathematical-proof/10636#10636 https://cstheory.stackexchange.com/questions/10635/halting-p...
- Tainnor 1y ago
  > Any axiomatic system will have true statements that are unprovable. Any effectively computable axiomatic system of sufficient strength. The "effectively computable" condition is probably uninteresting (if we couldn't effectively decide if something is an axiom we wouldn't be able to check proofs), but the "sufficient strength" part matters. There are interesting theories that are complete (i.e. for every sentence P, either P or not(P) is a consequence), such as the theory of the natural numbers with addition (but without multiplication).
aaron695 1y ago
[dead]
irthomasthomas 1y ago
Ha, I bought https://undecidability.com https://undecidability.com, but haven't decided what to do with yet, so for now it just redirects to my public bookmarks.
curtisszmania 1y ago
[dead]
theodorethomas 1y ago
Can someone explain to me why although we've known that classical physics is not a correct description of the hardware of the universe for at least 100 years now, we are still hooked on 90-year-old Turing Machines which cannot physically exist (they violate quantum mechanics) and whose theoretical limitations are, consequently, irrelevant.
Tainnor 1y ago
My pet peeves when it comes to undecidability: 1. People saying "sure, problem A may be undecidable but it's decidable for instance X". That's not how the concept works - if you restrict the a problem to a specific instance (in the sense of having a decider for the intersection of A and {X}), then it will always be decidable because either the Turing Machine that always outputs true or the Turing Machine that always outputs false is a decider (it doesn't matter that we don't know which one). I know what people are trying to say - "just because a problem is undecidable it doesn't mean you can't solve specific instances" - but this is arguing against a misconception of what decidability means. 2. "Decidability doesn't matter because real-world computers have finite memory". Yeah, but if your solution to problem X involves running an algorithm until you've run through all possible 2^N configurations for N=the size of your memory, you haven't really practically solved it either in any way that anyone would want to use.

156 points by BerislavLopac 1y ago

And here I thought it was simply about a system of equations solving down to a single solution (decidable). As opposed to having too many free variables.

skydhash 1y ago

One 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'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).

Gruzzy 1y ago
Would you have book recommendations / resources to share?
- skydhash 1y ago
  Introduction to the Theory of Computation by Michael Sipser. There's also his course based on the book on YouTube[0]. 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_JNv2MmK3wkOt9syvfQWY https://www.youtube.com/playlist?list=PLUl4u3cNGP60_JNv2MmK3...
  - soulofmischief 1y ago
    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.
    - skydhash 1y ago
      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 the other subdomains (to enact actions and query data). These communications are equally important as each subdomain. The hope is to have something that reflects the business domain, especially the cost of changes. Something that's easy/hard to change in the business should be easy/hard to change in the code, With OOP, this often results in verbose code, because each view of the data (which has its own rules) has its own class. With FP, because you often use more primitive data structures, it's easier to commute between subsets of data.
      - soulofmischief 1y ago
        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.
- nixpulvis 1y ago
  Might be hard to approach but my favorite is Pierce's "Types and Programing Languages": https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ (known as TAPL). Was grateful to take a graduate level class using it in college.
  - skydhash 1y ago
    TAPL is nice, and also very dense. I haven't fully read it, but my current understanding is the follow: Both the Turing Machine and the lambda calculus only describes how to act on data. They don't actually describes what the data is. So you can craft an algorithm that works well, but it can be supplied with the wrong type of data and it will goes haywire. Your only recourse is to trust the user of your algorithm. What type does is to have a set of classes of data, then have rules between those classes. You then annotate your code with those classes (combining them if it's possible) and then your type system can verify that the relations between them hold. To the type system, your program is data.
    - lanstin 1y ago
      I think undecidable means more like there are classes of problems for which there is no algorithm (that runs in finite time) can give the answer to. To square N, there is an algorithm that always works. To see if the Turing machine N halts in input M, there is not such an algorithm. The halting problem is undecidable. There is a clever way to encode Turing machines into Diophantine equations, so Diophantine equations (linear equations
  - tel 1y ago
    I really like TAPL but would recommend Harper’s Practical Foundations of Programming Languages (PFPL) first (though skip the first 2 chapters I think?). https://www.cs.cmu.edu/~rwh/pfpl.html https://www.cs.cmu.edu/~rwh/pfpl.html It’s far more directed than TAPL, so I think it’s easier to read from start to finish. TAPL feels better as a reference.
- downboots 1y ago
  Mertens Theory of Computation
  - Jtsummers 1y ago
    > Mertens Theory of Computation No such book exists. Do you mean The Nature of Computation by Moore and Mertens?
    - downboots 1y ago
      Sure, M&M's
      - deleted 1y ago
        [deleted]
Aicy 1y ago
Really? I studied it in my undergrad degree, and since then have worked as a SWE and not found it relevant at all really
- skydhash 1y ago
  It's the recursive nature of it. Almost any program can be written in a DSL that solves the class of problem that the program solves. So if you consider the user stories of your project as that class of problem, you can come up with with a DSL (mostly in form of pseudocode) that can describe the solution. But first you need to refine the terms down to some primitives (context free grammar). You then need to think about the implementation of the execution machine. which will be a graph of states (automata). The transition between the states will be driven by an execution machine. The latter needs not be as basic as the Turing machine. But often, you do not need to do all these stuff. You can just use common abstractions like design patterns, data structures, and basic algorithms to have a ready made solution. But you still have to compose them and if you understand how everything works, it's easier to do so.
- drdrey 1y ago
  it depends what you're working on, if you do any form of program analysis (security, compiler stuff) you bump into undecidability everyday
nitwit005 1y ago
I have to vote the opposite direction. I don't think it's ever been relevant. As an example, A practical walk through of what a simple CPU is doing was quite useful for getting the idea of what's going on. The concept of a Turing machine, which was originally intended for mathematical proofs, was not.
- tialaramex 1y ago
  I completely disagree. For example understanding the theory gives me a very powerful bullshit detector because entire categories of problem which might sound merely difficult are in fact Undecidable. Knowing that the actual regular expressions can be recognised by a finite automaton but PCRE and similar "LOL, just whatever neat string matching" extensions cannot means you can clearly draw the line and not accidentally make a product which promises arbitrary computation for $1 per million queries. I agree that understanding something of how the CPU works is also useful, but it's no substitute for a grounding in theory. The CPU is after all obliged to only do things which are theoretically possible, so it's not even a real difference of kind.
- skydhash 1y ago
  The CPU is an implementation of theory. It just happens that the realization of several axioms in the Turing machine is realizable physically. And the rest hold true. The nice thing with notation is that they're more flexible than building/creating/executing the thing they describe.
  - nitwit005 1y ago
    If you look back at the history, CPUs were often designed for specific tasks, and some of the early ones lacked conditional jumps that you'd normally consider nessesary for a Turing machine. We've made them more general purpose as that sells better, not because people cared about making Turing machines.
    - skydhash 1y ago
      Jump is not required for a Turing machine, only being able to move to a specific case by sliding. Conditional jump is an abstraction. Just like looping.
deleted 1y ago
[deleted]
DonaldPShimoda 1y ago
> One of the biggest boost to my SWE career was studying theory of computation and programming languages theory. I totally agree with you. > My major was electronic engineering, so I didn't touch those at the university. Unfortunately, ever more computer science graduates lack the same belief, even if they go to "top" university programs. Of course, I think part of the problem is the way the material is presented; "learn this to pass the exam" without fundamental motivation is pretty much always a bad set-up to get students interested. But, speaking anecdotally, a large part also seems to be a semi-recent surge of undergraduate students who genuinely believe that their academic career is nothing more than a hurdle to be muddled through in service of getting a piece of paper that lets them get a high-paying, low-labor-intensity job. They just don't engage with theory-focused material beyond what's strictly necessary to graduate, and then they dump the thoughts from their minds the second the semester is over. This manifests in all sorts of ways, but a common one is undergrads telling one another how little their professors know about the "real world" because they use (not even that) outdated technology in their lectures. Or maybe the profs use some less popular language and the students think of it as a waste of time. There's comparatively little self-motivation among modern CS students, where historically I think there was rather a lot. I suppose I'm not really going anywhere specific with this other than complaining, so maybe I can ask: What do you think it was that helped you realize that learning fundamental theory would be beneficial? (I don't have any indication that you were the same kind of student as these that I mention, since you were in a different major altogether, but I'm always looking for insights to help motivate students to study theory more, and insights can come from anywhere.)

gnulinux 1y ago

The reason decidability makes no or very little sense to tons of CS or Math majors is because the logical basis of decidability is almost never explained in school. Even if you're in a logic/computability class you likely won't get a very concrete explanation, unless you're in a Philosophy of Math class. The 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.ExcludedMiddle.html 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+mathematics https://ncatlab.org/nlab/show/neutral+constructive+mathemati...

LPisGood 1y ago
I was with you until here: > which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd... Why did you randomly shoehorn in homotopy type theory? Maybe I’m overreacting to this, but the only person I’ve ever known to shoehorn homotopy type theory into largely unrelated discussion has left quite a poor impression for me.

dunkeltaenzer 1y ago

The problem there is overlap between fractal and non-fractal spaces. Our Math and Logic were created to work in non-fractal spaces. Whenever we cross the boundaries into fractal spaces (recursion in programming, for example), our math and logic have a tendency to explode, because there are infinities flying around everywhere and things stop to be guaranteed to be deterministic, because you have to assure determinability for several dimensions of infinities. You have to accept certain quantum rules, in those spaces. And being deterministic isn't compatible with quantum rules. That's why quantum physics is struggling so badly to get rid of all those infinities flowing in with every new dimension they add to the wave function. That thing wasn't designed for fractal spaces. So it becomes harder and harder to contain all those leaking infinities into a workable magic ball. We stored most of our fractal remembrance in pictures for a reason. Much easier to draw fractals than to compute them with math, not made for fractal spaces

paulddraper 1y ago

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

cobbzilla 1y ago
I really enjoyed the author’s explanation of undecidability. 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.”
- wat10000 1y ago
  I'm not sure about that. These are also easily solved with a general-purpose CPU, if you don't care about running time. And there's nothing that says that a halt detector would be fast. The impossibility result is more interesting than just "it would take a million times the age of the universe to complete if every atom in it were put to the sole purpose of computing it" as we often see with cryptography.
  - hwayne 1y ago
    That's not necessarily true. Consider the program `x := 4; loop {if !sum_of_two_primes(x) {return true}; x += 2}`. If we run this on a general purpose CPU, this will halt if and only if Goldbach's conjecture has a counterexample. Otherwise it will run forever. So even if a working halt detector takes 14 million billion years, it will definitely tell us if the conjecture is true or not. Whereas if the general purpose CPU is still running after that time, we still have no way of knowing whether it's because it's going to run forever or if it simply hasn't reached the first (ludicrously large) counterexample.
    - 1y ago

brap 1y ago

I 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…

ryandamm 1y ago
Purely intuitively, it seems like there should be a connection between the two (computation and intelligence). But I have not formally studied any relevant fields, I would be interested to hear thoughts from those who have.
- brap 1y ago
  I was thinking the same thing, maybe a level above in the Chomsky Hierarchy…
- wat10000 1y ago
  The known laws of physics are computable, so if you believe that human intelligence is purely physical (and the known laws of physics are sufficient to explain it) then that means that human intelligence is in principle no more powerful than a Turing machine, since the Turing machine can emulate human intelligence by simulating physics. If there's a nonphysical aspect to human intelligence and it's not computable, then that means computers can never match human intelligence even in theory.
  - deleted 1y ago
    [deleted]
bawolff 1y ago
Philosophers have been trying to define what it means to be conscious since forever. I think that is informally what you mean here. If you just mean what problems can it solve, and how quickly, we already have a well developed theory of that in terms of complexity classes -https://complexityzoo.net/Complexity_Zoo https://complexityzoo.net/Complexity_Zoo

kazinator 1y ago

An undecidable problem in the Turing computational model is this: it is a problem for which no algorithm exists which can ] decide every input case. This doesn't preclude some input cases from being decided. What happens it that every attempt at making an algorithm for an undecidable problem will run into two issues: there will be input cases for which an answer exists, but for which the algorithm either gets into an infinite loop/recursion or else produces the wrong answer. Why would a decision procedure ever yield the wrong answer? That is due to mitigations of the infinite looping problem. To avoid becoming trapped by the input cases that trigger infinite calculations, the algorithm has to resort to some mechanism of arbitrarily stopping, without having reached the decision. Like for instance by capping the number of steps executed. But when that situation is reached, the correct answer is not yet known. The algorithm can return "yes" or "no", but that will be wrong half the time. Or it can report "failed", which is always incorrect, not matching either "yes" or "no". A classic example of an undecidable problem is the Halting Problem: the question of whether a given program (or algorithm) P, operating on an input I, will halt or not. So the space of inputs for this problem is <P, I> pairs. The input space is infinite, but all instances in that space are finite: finite length programs P operating on finite inputs I. The problem is that just we have a given finite P and finite I doesn't mean that halting can be decided in finite steps. No matter how cleverly someone constructs a halting decider, it is easy to produce test cases which will cause that decider to either stop and produce the answer (decide incorrectly) or else iterate or recurse forever. (Demonstrating how such test cases can be produced for any decider is at the heart of a popular proof which shows that halting is undecidable.) The Halting Problem is at the center of decidability, because every decision procedure of any kind (not necessarily a decision in the Halting Problem) is a <P, I> pair. For instance the decision whether a list of N integers is sorted in ascending order is a <P, I> pair. P is an algorithm for sweeping through the integers to check that they are ordered, and I is some list of integers. Since it is a <P, I> pair, it is in the domain of the Halting Problem. P is not in the Halting Problem: P is in the domain of processing a list of integers. But <P, I> is an input case of the Halting Problem: does list-processing algorithm P halt on the list of integers I. The upshot is that when we are solving some decision problem by running an algorithm, which is taking long, and we ask "will this decision terminate, or is it in a loop?" we are then posing another problem, and that problem is an input case of the Halting Problem. And we know that the Halting Problem is undecidable. What that means is that if we happen to be calculating a problem which is undecidable, the Halting Problem informs us that there is no guaranteed shortcut for us to know whether our calculation is hung, or whether it is working toward halting. When we try to apply "meta reasoning" about an algorithm that appears stuck, our reasoning itself may also get stuck. We may have to give up, cut the investigation short, and report "we don't know". I.e. we don't know whether or not our decision program is forever stuck or working toward the solution. Undecidability is a somewhat important topic to a software engineer for the following reasons. In your career you may from time to time encounter requirements that call for a the calculation of an undecidable problem. If you know can recognize it, you can take action to revise the requirements. For instance, perhaps you can negotiate the requirements such that it's acceptable for the decision to be incorrect, erring on one side of the other (false positive or false negative). Equivalently, maybe some inputs can be rejected before the algorithm, leaving a decidable subset. You may have a People Problem there because the requirements are coming from non-computer-scientists who don't know about decidability; you have to be careful not to make it look like you are refusing to do hard work due to not believing in your skill, or laziness. As an example, we could use the Halting Problem itself. Say you work on some virtual machine for sandboxing untrusted programs and your boss says, can we detect programs which loop infinitely, and not run them at all? Just reject them? If you know about undecidability, you can tell your boss, no, that is an undecidable problem! What we can do is limit the number of instructions or run time, which will stop some programs that are not looping infinitely but are just taking long to calculate something. Or here is another thing we can do instead; only admit programs written in a language that is not Turing Complete: has only bounded loops and no recursion. The sandbox compiler can reject all others. Or we can allow recursion but stacked recursion only (not tail) and limit the depth. Of course, that's just an easy example; undecidability can sneak into the requirements in forms that are not immediately recognizable.

johnea 1y ago

I don't know, I can't decide...

deleted 1y ago
[deleted]

deleted 1y ago

[deleted]

cubefox 1y ago

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. Another way to express this is to say that the continuum hypothesis is undecidable (in ZFC). Kurt Gödel used this sense of "undecidable" in his famous paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I". ("On formally undecidable propositions in Principia Mathematica and related systems I") Are these two meanings of "undecidable" related in some way? I guess probably yes. But I'm not sure how.

ttctciyf 1y ago
> Are these two meanings of "undecidable" related I can't claim to answer this, but you might like to look at A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory[0] which (amongst other interesting things) does discuss the proposition "ZFC is consistent", which is independent from ZFC, in terms of a Turing Machine which enumerates all possible proofs in ZFC and halts when it finds a contradiction (e.g. a proof of 0=1). But I don't think there's a simple equivalence here, all the same. The logician's undecidable is always relative to a set of axioms, whereas the question of whether a property of strings can be decided by some TM doesn't place any constraints on the TM, which is to say the deciding TM is not required to, nor prohibited from, implementing any particular axiom set. (It's tempting to try and show "provable in ZFC" to be a (CS)undecidable property by having a TM enumerate ZFC proofs and halt on finding a proof or disproof of the input string, and imagine the TM running forever when given a statement of the Continuum Hypothesis. But the TM could proceed by other means - for example [1] shows a proof of CH's independence in a theorem prover, so that a TM incorporating this construction could indeed reject CH statements as unprovable in ZFC. Which is not to say "ZFC-provable" *isn't* (CS)undecidable, just that showing this isn't as simple as constructing a ZFC-proof-enumerator and giving it the CH as input.) 0: https://arxiv.org/abs/1605.04343 https://arxiv.org/abs/1605.04343 1: https://arxiv.org/abs/2102.02901 https://arxiv.org/abs/2102.02901
tel 1y ago

taeric 1y ago

I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. It isn't that the drawing doesn't exist. It is that you still have some freedom in how long certain parts could be. Crucially, not all. It could be that parts of the drawing are indeed fully specified. Same can go with programs. You can constrain parts of it enough that you can answer some pretty specific questions. And similar to how a drawing with fewer lines is easier to constrain, a program that has restricted constructs can be easier to constrain.

constantcrying 1y ago
>I'm curious if you could make an analogy to the idea of "underspecified" in FreeCAD. That is just solution theory of a non-linear system of equations. The solution space can have exactly one solution (fully constrained), more than one (under constrained) or zero (over constrained). To be honest I do not really see a connection.
- taeric 1y ago
  I meant more as how to mentally model it in a way that can get someone across the line. My assertion is that caring about undecidability is almost certainly a waste of time for most people. That said, the reason we work in small chunks is often so that we can more easily answer questions about programs. Moving the graphical drawing and constraints over to a symbolic system also helps see how many symbols it can take to cover a simple system. Of course, the real reason for me thinking on this is that I'm playing with FreeCAD for the first time in a long time. :D

deleted 1y ago

[deleted]

deleted 1y ago
[deleted]

nialv7 1y ago

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.

mreid 1y ago
I had exactly the same reaction, which prompted me to write this comment: https://news.ycombinator.com/item?id=44122045 https://news.ycombinator.com/item?id=44122045
bubblyworld 1y ago
...which is the same thing as Rice's theorem, and many other mind-bending results. It's all diagonalization under the hood =)

mreid 1y ago

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 plus its inputs) and outputs True or False depending on whether it halts or not. The argument in the article does a great job of showing that `IS_HALTING` cannot exist because it is in some sense "too powerful" but that means there is a mapping f : strings -> boolean that cannot be represented as a program, which seems weird if you've been programming for ages and every function you encounter is expressed as a program. The result becomes less weird when you realize that that almost all functions from string -> boolean are not expressible as a program. Why? Well there are countable many programs since there are only countably many finite length strings and every program, by definition, is a finite length string. However, there are uncountably many functions from string -> boolean since these functions map one-to-one to sets of strings (just let the set be all inputs that map to True) and the cardinality of the set of sets of strings is uncountable. This is essentially due to Cantor's diagonalization argument which shows you cannot put all elements in a set X into a 1-1 correspondence with all the subsets of X, even when X is countably infinite. This fact is at the heart of a lot of these computability results since it shows there is a gap between all functions (= any arbitrary subset of finite strings) and a program (= a finite string).

cyberax 1y ago
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.
- hwayne 1y ago
  `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`.

gerdesj 1y ago

I'm not sure

graycat 1y ago

> What does “Undecidable” mean, anyway A big and relatively recent example is to take (1) the axioms of Zermelo-Fraenkel set theory and (2) the axiom of choice and ask if (1) can be used to prove or disprove (2). The surprising answer is "No", i.e., (1) cannot be used either to prove or disprove (2). So, can work with (1) and, whenever convenient, assume (2), continue on, and never encounter a problem. So, given (1), (2) is undecidable. The work was by Paul J. Cohen as at https://en.wikipedia.org/wiki/Paul_Cohen https://en.wikipedia.org/wiki/Paul_Cohen The field of research about what is undecidable also goes back to Kurt Gödel as at https://en.wikipedia.org/wiki/Kurt_G%C3%B6del https://en.wikipedia.org/wiki/Kurt_G%C3%B6del Another example, starting with (1), of an undecidable statement is the continuum hypothesis: There is no set whose cardinality is strictly between that of the integers and the real numbers. In simple terms, "cardinality" means that there is no set X that is too large to be put into 1-1 correspondence with the set of integers and too small to be put into 1-1 correspondence with the set of real numbers.

Animats 1y ago

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 it's important.

ummonk 1y ago
Yes, the article is clearly confused about the concepts, given its mention of bcrypt cracking and chess engines.
- dmurray 1y ago
  Yes, I thought the article was really good until it got to that point. > 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.) A Turing machine can be trivially repurposed as a bcrypt cracker or chess engine (for the same definition of trivial the author is using), so if it's not intuitive that a computer can do this, then your intuition is wrong. Program optimizers and theorem provers also exist, of course, but in those cases the problems really are undecidable so no Turing machine is guaranteed to work on any given program or theorem.
  - bubblyworld 1y ago
    A solution to the Halting problem can be repurposed as a general-purpose theorem prover. The author is correct. You simply write a program that searches all possible valid proofs till it finds the one you are looking for (or maybe doesn't and runs forever). Then you check whether it halts with your Halting solution - if that returns true, you know that a proof exists, otherwise you know that one doesn't. In other words, you can use undecidability of first-order logic to prove undecidability of the Halting problem if you like, although it's a bit of a chicken-egg thing historically (I believe).

Aziell 1y ago

The first time I encountered the halting problem, I was honestly confused. I kept thinking there had to be another solution. But over time, I came to realize it wasn’t a technical issue ,it was about the limits of computation itself. This article explains the concept of undecidability really well. It breaks things down in a very practical way. That last part, about the limits of how we think, really hit me.

ummonk 1y ago

"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 exponential -- runtime algorithms), and it wouldn't be any easier to transform them into halting problems.

jonahx 1y ago
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.
- cvoss 1y ago
  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.
  - jonahx 1y ago
    "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.

godelski 1y ago

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_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [1] https://scottaaronson.blog/?p=710 https://scottaaronson.blog/?p=710 [2] https://cstheory.stackexchange.com/questions/10635/halting-problem-uncomputable-sets-common-mathematical-proof/10636#10636 https://cstheory.stackexchange.com/questions/10635/halting-p...

Tainnor 1y ago
> Any axiomatic system will have true statements that are unprovable. Any effectively computable axiomatic system of sufficient strength. The "effectively computable" condition is probably uninteresting (if we couldn't effectively decide if something is an axiom we wouldn't be able to check proofs), but the "sufficient strength" part matters. There are interesting theories that are complete (i.e. for every sentence P, either P or not(P) is a consequence), such as the theory of the natural numbers with addition (but without multiplication).

aaron695 1y ago

[dead]

irthomasthomas 1y ago

Ha, I bought https://undecidability.com https://undecidability.com, but haven't decided what to do with yet, so for now it just redirects to my public bookmarks.

curtisszmania 1y ago

[dead]

theodorethomas 1y ago

Can someone explain to me why although we've known that classical physics is not a correct description of the hardware of the universe for at least 100 years now, we are still hooked on 90-year-old Turing Machines which cannot physically exist (they violate quantum mechanics) and whose theoretical limitations are, consequently, irrelevant.

Tainnor 1y ago

My pet peeves when it comes to undecidability: 1. People saying "sure, problem A may be undecidable but it's decidable for instance X". That's not how the concept works - if you restrict the a problem to a specific instance (in the sense of having a decider for the intersection of A and {X}), then it will always be decidable because either the Turing Machine that always outputs true or the Turing Machine that always outputs false is a decider (it doesn't matter that we don't know which one). I know what people are trying to say - "just because a problem is undecidable it doesn't mean you can't solve specific instances" - but this is arguing against a misconception of what decidability means. 2. "Decidability doesn't matter because real-world computers have finite memory". Yeah, but if your solution to problem X involves running an algorithm until you've run through all possible 2^N configurations for N=the size of your memory, you haven't really practically solved it either in any way that anyone would want to use.