[HN Gopher] What does "Undecidable" mean, anyway
___________________________________________________________________
What does "Undecidable" mean, anyway
Author : BerislavLopac
Score : 49 points
Date : 2025-05-28 19:37 UTC (3 hours ago)
(HTM) web link (buttondown.com)
(TXT) w3m dump (buttondown.com)
| skydhash wrote:
| 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 wrote:
| Would you have book recommendations / resources to share?
| skydhash wrote:
| 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_JNv2
| MmK3...
| soulofmischief wrote:
| 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 wrote:
| 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.
| nixpulvis wrote:
| Might be hard to approach but my favorite is Pierce's "Types
| and Programing Languages":
| https://www.cis.upenn.edu/~bcpierce/tapl/ (known as TAPL).
| Was grateful to take a graduate level class using it in
| college.
| skydhash wrote:
| 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.
| downboots wrote:
| Mertens Theory of Computation
| Jtsummers wrote:
| > Mertens Theory of Computation
|
| No such book exists. Do you mean _The Nature of
| Computation_ by Moore and Mertens?
| downboots wrote:
| Sure, M&M's
| Aicy wrote:
| Really? I studied it in my undergrad degree, and since then
| have worked as a SWE and not found it relevant at all really
| nitwit005 wrote:
| 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.
| gnulinux wrote:
| 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.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...
| dunkeltaenzer wrote:
| 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 wrote:
| > 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 wrote:
| 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."
| nullc wrote:
| > No program can tell whether any program will halt or not.
|
| Might try for another wording which isn't easily misunderstood.
| I was going to suggest every instead of any but that supports a
| different misunderstanding.
| zqna wrote:
| There will always be more questions the fool will ask, than a
| wise man will be able to answer
| brap wrote:
| 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 wrote:
| 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 wrote:
| I was thinking the same thing, maybe a level above in the
| Chomsky Hierarchy...
| bawolff wrote:
| 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
| mystified5016 wrote:
| I think this is more about levels or classifications of
| intelligence.
|
| If you've ever interacted with a very smart animal, it's easy
| to recognize that their reasoning abilities are on par with a
| human child in a very subjective and vague way. We can also
| say with extreme confidence that humans have wildly different
| levels of intelligence and intellectual ability.
|
| The question is, how do we define what we mean by "Alice is
| smarter than Bob". Or more pertinently, how do we effectively
| compare the intelligence and ability of an AI to that of
| another intelligent entity?
|
| Is ChatGPT on par with a human child? A smart dog? Crows? A
| college professor? PhD level?
|
| Of course we can test specific skills. Riddles, critical
| thinking, that sort of thing. Problem is that the results
| from a PhD will be indistinguishable from the results of a
| child with the answer key. You can't examine the mental state
| of others, so there's no way to _know_ if they 've
| synthesized the answer themselves or are simply parroting.
| (This is also a problem philosophers have been thinking about
| for millenia)
|
| Personally, I doubt we'll answer these questions any time
| soon. Unless we do actually develop a science of
| consciousness, we'll probably still be asking these questions
| in a century or two.
| skydhash wrote:
| Intelligence is often a measure how quickly we can embrace
| a new model and how effectively we can use it. Building
| such a model can be done haphazardly or be guided with
| skill transfer methodology. Once that done, intelligence is
| how well we can select the correct model, filter the
| relevant parameters out and then produce a correct answer.
|
| There's a lot of factors there and more that I haven't
| specified. But one thing that I believe is essential is the
| belief that an answer is correct or uncertain.
| joe_the_user wrote:
| I don't either philosophical conceptions of consciousness or
| theories of computational complexity count as even "efforts
| to formalize intelligence". They are each focused on
| something significantly different.
|
| The closest effort I know of as far characterizing
| intelligence as such is Steven Smale's 18th problem.
|
| https://en.wikipedia.org/wiki/Smale%27s_problems
| joe_the_user wrote:
| I agree the idea of a formal view of intelligence is appealing.
| The hurdle that any such view faces is that most intelligence
| seems to involve rough, approximate reasoning.
|
| I think this approximate nature of intelligence is essentially
| why neural nets have been more successful than earlier
| Gofai/logic based system. But I don't think that means formal
| approaches to intelligence are impossible, just they face
| challenges.
| mystified5016 wrote:
| This is one of those ideas that great minds have been chewing
| on for all of recorded history.
|
| In modern thinking, we do certainly recognize different classes
| of intelligence. Emotional intelligence, spatial reasoning,
| math, language, music.
|
| I'd say the classes of intelligence are finite. Primarily
| because different types of intelligence (generally) rely on
| distinct parts of our finite brains.
|
| As for maximum intelligence, I like the angle taken by several
| SciFi authors. Generally, when an AI is elevated to the
| extremes of intelligence, they detach from reality and devolve
| into infinite naval gazing. Building simulated realities or
| forever lost in pondering some cosmic mystery. Humans brought
| to this state usually just die.
|
| For physical, finite entities, there's almost certainly an
| upper limit. It's probably a _lot_ higher than we think,
| though. Biological entities have hard limits on energy,
| nutrients, and physical size beyond which it 's just impossible
| to maintain any organism. Infinities are rarely compatible with
| biology, and we will always be limited.
|
| Even an AI is still beholden to the practicalities of moving
| energy and resources around. Your processor can only get so
| large and energy/information can only move so fast.
| Intelligence in AI is probably also bounded by physical
| constraints, same as biological entities.
| kazinator wrote:
| 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.
| cubefox wrote:
| Do you know whether there is an algorithm which "mostly" solves
| the halting problem, by returning either "halts", "doesn't
| halt" or "don't know", while only very rarely returning "don't
| know" for (what we would intuitively consider) natural
| algorithms?
| JonChesterfield wrote:
| Yes. Take the one which might not halt and add an integer
| argument which you decrement on recursion/loop, possibly
| called "fuel", and return don't know when that hits zero.
| Then call your algorithm with a large integer for that
| argument and wait.
| kazinator wrote:
| Practically speaking, if your goal is to protect system
| resources, which is a practical concern removed from
| theoretical computer science, the halting problem isn't
| even the right concern. It's good to know about and all,
| but the problem is that programs which halt can be a
| nuisance. You don't care about the difference between "runs
| for 5 days and halts" and "runs forever".
|
| Some programs run indefinitely by design, like services.
| Those may be acceptable in a system, but not CPU-intensive,
| long-running programs.
|
| So you in fact have to reject some programs which halt, and
| accept some which don't.
| mrkeen wrote:
| I think it would be much more fruitful to flip it around the
| other way.
|
| Start with small pieces which halt, and see how far you can
| get by combining them into larger programs. Compiler-help is
| available: https://docs.idris-
| lang.org/en/latest/tutorial/theorems.html...
|
| A down-side of a yes/no/maybe halting checker is that it
| wouldn't tell you _why_. You 'd get your "doesn't halt"
| result and then have to debug the algorithm.
| skydhash wrote:
| > _undecidability can sneak into the requirements in forms that
| are not immediately recognizable._
|
| The whole issue is loops and recursions (more complicated
| loops). And how to avoid the bad sort is to inspect your
| invariants. For classic loops, you need to prove that your
| condition will eventually be false. For iterators, you need to
| prove that your data is bounded. And for recursion, that the
| base case will eventually happens. The first two are easier to
| enforce.
|
| The goal is for your code to be linear. If you have code as one
| of your input, you force it to be linear too.
| johnea wrote:
| I don't know, I can't decide...
| cubefox wrote:
| 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 Godel used this sense of "undecidable" in his famous paper
| "Uber formal unentscheidbare Satze 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.
| aatd86 wrote:
| 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.
| taeric wrote:
| 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 wrote:
| >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.
___________________________________________________________________
(page generated 2025-05-28 23:00 UTC)