The Impossible Problem NO ONE Can Solve (The Halting Problem)

  Рет қаралды 343,490

Up and Atom

Up and Atom

Күн бұрын

Get Nebula using my link for 40% off an annual subscription! go.nebula.tv/upandatom
Recommended shows:
Is Math Invented or Discovered? nebula.tv/ismathinvented Becoming Human nebula.tv/becominghuman?ref=u...
What is Code? nebula.tv/what-is-code?ref=up...
Hi! I'm Jade. If you'd like to consider supporting Up and Atom, head over to my Patreon page :)
/ upandatom
Visit the Up and Atom store
store.nebula.app/collections/...
Subscribe to Up and Atom for physics, math and computer science videos
/ upandatom
For a one time donation, head over to my PayPal :) www.paypal.me/upandatomshows
Sources
matjaz.substack.com/p/why-are...
www.khanacademy.org/computing...
www.udacity.com/course/intro-...
The Nature of Computation - Cristopher Moore
A big thank you to my AMAZING PATRONS!
Jonathan Koppelman, Michael Seydel, Cy 'kkm' K'Nelson, Thorsten Auth, Chris Flynn, Tim Barnard, Izzy Ca, Millennial Glacier, Richard O McEwen Jr, Scott Ready, John H. Austin, Jr., Brian Wilkins, Thomas V Lohmeier, David Johnston, Thomas Krause, Lynn Shackelford, Ave Eva Thornton, Andrew Pann, Anne Tan, David Tuman, Richard Rensman, Ben Mitchell, Steve Archer, Luna, Viktor Lazarevich, Tyler Simms, Michael Geer, James Mahoney, Jim Felich, Fabio Manzini, Jeremy, Sam Richardson, Robin High, KiYun Roe, Christopher Rhoades, DONALD McLeod, Ron Hochsprung, Aria Bend, James Matheson, Kevin Anderson, Alexander230, Tim Ludwig, Alexander Del Toro Barba, Justin Smith, A. Duncan, Mark Littlehale, Tony T Flores, Dagmawi Elehu, Jeffrey Smith, Alex Hackman, bpatb, Joel Becane, Paul Barclay, 12tone, Sergey Ten, Damien Holloway, John Lakeman, Jana Christine Saout, Jeff Schwarz, Yana Chernobilsky, Louis Mashado, Michael Dean, Chris Amaris, Matt G, Dag-Erling Smørgrav, John Shioli, Todd Loreman, Susan Jones, Julian Nagel, Cassandra Durnord, Antony Birch, Paul Bunbury, Kent Arimura, Phillip Rhodes, Michael Nugent, James N Smith, Roland Gibson, Joe McTee, Dean Fantastic, Bernard Pang, Oleg Dats, John Spalding, Simon J. Dodd, Tang Chun, Michelle, William Toffey, Michel Speiser, Rigid Designator, James Horsley, Brian Williams, Craig Tumblison, Cameron Tacklind, 之元 丁, Kevin Chi, Lance Ahmu, Tim Cheseborough, Markus Lindström, Steve Watson, Midnight Skeptic, Dexter Scott, Potch, Indrajeet Sagar, Markus Herrmann (trekkie22), Gil Chesterton, Alipasha Sadri, Pablo de Caffe, Taylor Hornby, Mark Fisher, Emily, Colin Byrne, Nick H, Jesper de Jong, Loren Hart, Sofia Fredriksson, Phat Hoang, Spuddy, Sascha Bohemia, tesseract, Stephen Britt, KG, Hansjuerg Widmer, John Sigwald, O C, Carlos Gonzalez, Res, Thomas Kägi, James Palermo, Chris Teubert, Fran, Christopher Milton, Robert J Frey, Wolfgang Ripken, Jeremy Bowkett, Vincent Karpinski, Nicolas Frias, Louis M, kadhonn, Moose Thompson, Rick DeWitt, Andrew, Pedro Paulo Vezza Campos, S, Rebecca Lashua, Pat Gunn, George Fletcher, RobF, Vincent Seguin, Shawn, Israel Shirk, Jesse Clark, Steven Wheeler, Philip Freeman, Jareth Arnold, Simon Barker, Lou, and Simon Dargaville.
Chapters
0:00 A double edged sword
1:00 Universality
3:09 Thanks Nebula!
4:32 How do we know there are problems computers will never solve?
6:05 Hilbert's Program
7:59 Decidability
11:39 Turing hears of the Entscheidungsproblem (uh-oh)
13:27 The Halting Problem
16:42 Undecidability
Creator - Jade Tan-Holmes
Written by Zoe Cocchiaro and Jade Tan-Holmes
Animations by Tom Groenestyn
Editing by Standard Productions
Music - epidemicsound.com

Пікірлер: 1 700
@upandatom
@upandatom 10 ай бұрын
Get Nebula using my link for 40% off an annual subscription! go.nebula.tv/upandatom And if you're having déjà-vu, yes I have made a video about the halting problem, but this one is better.
@odizzido
@odizzido 10 ай бұрын
I am going to try nebula again. It had performance issues when I tried it when it first started out but I imagine those have been solved now.
@fredashay
@fredashay 10 ай бұрын
Jade, do you think the Halting Problem will ever be able to be solved? _(And to the Chinese .50 cent army guy who keeps following me around YT and harassing me for being an advocate of Democracy, go eff yourself and eff Xi Jinping!!!)_
@govcorpwatch
@govcorpwatch 10 ай бұрын
1:35. I walked by a part of the original ENIAC while working for UPenn Computer Graphics Lab. After discussion with an original ENIAC worker, they said that the ENIAC was created NOT for just "artillery tables" but for computing Nuclear weapons. No joke, That IS the classified purpose of the ENIAC. People still don't know this.
@TheTransitmtl
@TheTransitmtl 10 ай бұрын
ChatGPT is a LLM. It can't solve anything. It's just so good at making groups of words sound coherent that people mistake its output for some kind of reflection. I use it for simple coding tasks like writing very simple unit tests and even at that it makes many errors
@njnjhjh8918
@njnjhjh8918 10 ай бұрын
I adore you, Jade, but does a HaltChecker cause a paradox if it never runs? HaltChecker has two inputs. You only give HaltChecker Reverser as input and nothing else and what is Reverser's input?
@chrisshuttleworth
@chrisshuttleworth 10 ай бұрын
Your use of multiple nested monitors and the “programs” watching them (in different clothing and hairstyles so we could differentiate between them) was very creative. Well done!!
@Slackware1995
@Slackware1995 10 ай бұрын
Except it doesn't describe what she is saying.
@SapSapient
@SapSapient 10 ай бұрын
I very much appreciate the clear, methodical approach these videos take in explaining moderately complicated ideas. I also had not realized how developed Turing's ideas were so early in his career.
@thegzak
@thegzak 10 ай бұрын
This is actually a deeply complex idea, the trick is to explain it so masterfully that it feels simpler than it really is 😉 Well done!
@lonestarr1490
@lonestarr1490 10 ай бұрын
Most of the groundbreaking work by the really big names in math, physics, computer sciences and alike has, more often than not, been done in the early years of their careers, like in their early 30's or even their 20's. Einstein, in his annus mirabilis 1905, has been 26 years old. The years from 25 to 35 are really the most creative decade you're given in your lifetime. Peek performance not only in sports but also in science, as it turns out.
@stylis666
@stylis666 10 ай бұрын
@@lonestarr1490 And in arts as well. As you said, in all creative fields. Thankfully that doesn't stop people from being creative outside of their peak, but you seem to be very correct in the assessment that most creativity is expressed in early adulthood. Probably due to many factors of which the brain and the rest of the body are just a few of the factors. One/some of the other factors might be the spreading and increasing of talents, efforts, and focus. So that also doesn't mean that less value is produced in the same time, but it is more spread out over different areas, so there are less pronounced peaks.
@Orion40000
@Orion40000 10 ай бұрын
@@lonestarr1490 Asimov wrote a story that suggested that the Earth is a petri dish filled with agar jelly. Humanity was the bacteria that formed on it, and its growth represented the increase in human knowledge. Sometimes, a bacterium would evolve which was so hugely successful that it would explode in population, massively increasing our sphere of knowledge. So far, so good. He then went on to suggest that there was an outside force - a galactic penicillin - that stopped us learning too much too quickly. Maybe for our own good, or maybe for the good of the society the penicillin represented. As soon as we started growing by an uncomfortable amount, those outstanding bacteria would be killed. If such an analogy were accurate, I wonder how old you could get before the penicillin noticed you?
@HalfdeadRider
@HalfdeadRider 10 ай бұрын
@@lonestarr1490 Maybe it is changing in science as it is in sports, people are staying fitter and stronger much longer than 35-40 already.
@cybisz2883
@cybisz2883 10 ай бұрын
I have never before seen such a fun, simple, and clever illustration of the halting problem than your haltchecker & reverser. That was pure genius!
@xbzq
@xbzq 10 ай бұрын
It's also incorrect and missing. If it's genius then it must be evil genius.
@Chaitany9
@Chaitany9 10 ай бұрын
Wt do u mean by hault checker
@xbzq
@xbzq 10 ай бұрын
@@Chaitany9 Did you watch the video? It's incorrect. Working is hard isn't it? Halt, not hault.
@zerksari
@zerksari 10 ай бұрын
Excellent! Watched easily over 100 hours on incompleteness and studied it myself at university. This video is easily the most 'visualized' digestable walkthrough. Props!
@cykkm
@cykkm 10 ай бұрын
Jade had another vid on the TM and the halting problem specifically, a couple years back, on this very channel. That one had, IMO, even more concise illustration of the proof. Do find it if you liked this one!
@zerksari
@zerksari 10 ай бұрын
@@cykkm Saw it, I agree. This one is more.. 'digestable' I would surmise. Both are really good. Don't get me started on Turing. What they did to the genius at easily the level of Bach should be cried and taught globally. They stole a part of our future. These folks don't come around that often..:(
@SetemkiaFawn
@SetemkiaFawn 10 ай бұрын
Very important aspect of Turing's creation now known as the Turing Machine. The various steps that the machine could perform were meant to duplicate things that could be done by a computer. When he started his work the only computer that he knew of was a human using brain, pencil, and paper. He was trying to characterize what a computer could compute.
@cykkm
@cykkm 10 ай бұрын
Strictly, you mean the UTM. Also, the concept of non-deterministic TM is at the core of computational complexity theory. E.g., it's how the NP class is defined. Yes, he was a tragic genus. A troubled mind of Poincaré's magnitude. I was blown away by his paper on biology and life. It parallels Schrödinger's “What is life?” in a sense, but from the mathematician's perspective. I forgot the title, but you can find it. You won't be disappointment, for sure! And, speaking of computers, it was unclear whether ENIAC would be able to compute everything computable when it would've been built. Von Neumann himself was on the team that designed it, and he was uneasy while the machine was being constructed, because he couldn't prove it, in genera. Ironically, he was running into undecidable equivalence problems.
@prototypeinheritance515
@prototypeinheritance515 10 ай бұрын
@@cykkm I don't get how it was so hard to prove universality on the ENIAC. Couldn't you just write a simulator for a universal TM and prove the correctness of said simulator?
@Vastin
@Vastin 10 ай бұрын
​@@cykkm You can compute everything but only within bounded time. The logical error they keep making is in the proposal that an unbounded time (or set of any sort) is a legitimate logical structure. Once you bound your questions at T-0 and T-Ω these questions compute to a final (and initial) state without paradox. It's not necessarily useful, particularly as the amount of computation time you require might equal the total amount of time available to you in all of existence, so from a practical standpoint it's meaningless - but it IS solvable in a purely logical context.
@cykkm
@cykkm 10 ай бұрын
@@prototypeinheritance515 You can, if you in fact have the computer built and humming. Otherwise, you can't.
@AnthonyFlack
@AnthonyFlack 9 ай бұрын
Well, an electronic computer is not really much help to understanding the concept, right? If you can follow a flow chart, you can conceptualise a program, and a computer's just a faster pencil. The computer could be imagined as a factory worker, following instructions with no training. It has a direct application to industrial labour, and of course the first "computers" were rooms full of people doing sums. Interesting to note that Richard Feynman started his career managing the human computer of the Manhattan Project in the 1940s, and ended his career designing highly parallel supercomputers in the 1980s, using the same ideas. Conway's Game of Life was devised on paper as well, ironically enough for such a classic computer program. He used to run it on a Go board. I think by the time Conway actually saw it running electronically he was already done with it and no longer interested. He'd already determined it was Turing Complete.
@migfed
@migfed 10 ай бұрын
This episode has become now, I do believe firmly, into one of your own anthology of finest videos featured by you. Thank you so much. The concept was sharply posted and yet clearly for anyone without great knowledge of computer science.
@alvaro_ch
@alvaro_ch 10 ай бұрын
Was about to state the same 👍
@silkwesir1444
@silkwesir1444 10 ай бұрын
Yes. I think never before where so many previous videos mentioned.
@xbzq
@xbzq 10 ай бұрын
It's incorrect. The halting checker needs two inputs, a program, and an input for that program. That's just the start of why this is very wrong. Udiprod made the correct explanation many years ago and she should have watched it before releasing this incorrect video.
@andrewj22
@andrewj22 10 ай бұрын
​@@xbzqThanks. I was finding the explanation very confusing. If the halt checker was supposed to work given a ore-defined, specific input for the program it was checking, then there should be no necessary problem determining whether "reverser" would halt or not. I'll look up the explanation you referred to.
@decreasing_entropy3003
@decreasing_entropy3003 10 ай бұрын
This has been very intuitive; the personification of the Haltchecker and Reverser has been very discernible, even the core statement of Russell's paradox aptly put. Well made video!
@nobodythisisstupid4888
@nobodythisisstupid4888 7 ай бұрын
I thought it was incredibly interesting when I realized that the Halting Problem, Russel’s Paradox, and Godel’s Incompleteness Theorem were in some way all describing the same fundamental logical idea when viewed through various lenses (computability, set theory, and generalized formal logic). Different conclusions are drawn from these different approaches but they all touch on a fundamental principle about the limits of logic. I felt incredibly validated when I discovered that these were all connected because they were all a form of a diagonal argument, and I found some other theorems that also were proved with a diagonal argument.
@fikipilot
@fikipilot 10 ай бұрын
You had fun filming and editing haltchecker and reverser. It looked like fun. I love the filmography of this complex maths discussion. Love it!!!
@sofar55
@sofar55 10 ай бұрын
I'm still confused on the halt checker/reverser programs. Individually, Checker and Reverser returning running or halted makes sense. Check reads an outside program and says run. Rev says halt. Check then reads Rev and says halted. Rev then says run. These seem like sequential events and/or separate instances of each program. The description implies that Rev is causing the paradox by trying to run/halt simultaneously, but if Check can run on the outside program and Rev, shouldn't Rev be able to run on the result of Check multiple times also?
@bananaforscale1283
@bananaforscale1283 10 ай бұрын
That confuses me too.
@tallowisp8868
@tallowisp8868 10 ай бұрын
TLDR: You do run Checker exactly once to check if Reverser halts or not. Long explanation: Let's assume we have a Checker program that always outputs if a given program halts or runs forever. Now we can write a Reverser program based on that exact Checker program. It's just a small extension that you add after Checker decided the output. The modifications for Reverser could be as follows: If the output of Checker would be "halts" add an infinite loop. If the outpout of Checker would be "runs forever" halt the program. So Reverser does not have an output. Reverser runs forever if the answer of Checker would be "halts" and halts if the output of Checker would be "runs forever". Now the crucial idea is not to run the programs multiple times. You do run Checker exactly once and give it the program Reverser as input. So Checker has to decide if Reverser will halt or not. The final logical step is a bit of an inception moment: Let's say Checker outputs that Reverser "halts". The crucial thing to realise is that Reverser is based on Checker so the only way that Reverser could halt is if Checker would output "runs forever". This means Checker has to output both "halts" and "runs forever" at the same time which is a contradiction.
@shexec32
@shexec32 10 ай бұрын
The missing part is that Check is being recursively fed itself as part of the container. What does outer Check do if inner Check halts? Finally, what would happen in the recursive case?
@BlackcapCoder
@BlackcapCoder 10 ай бұрын
The trick is that you pass the checker+reverser program as input into itself. Regardless of whether the input program to the innermost instance of checker+reverser halts or not, checker+reverser can neither halt, nor not halt.
@InShadowsLinger
@InShadowsLinger 10 ай бұрын
So the explanation is: Suppose you have a program A that can decide whether any given program will halt (the halt checker). Then you create a new program B that has the program A in it and what ever you feed to B is immediately fed directly to A and based on A’s output B decides whether it is going to halt (if A say the inputs runs forever) or run forever (if A says input will halt). This is the reverser in the video. And now comes the important part that is not clear from the video: you need to feed B to itself. That is where the paradox comes from. If B was supposed to halt and you feed it to B, it will not halt and vice versa. Maybe it was implied in there somewhere with the “inception” but you have to squint pretty hard.
@haniyasu8236
@haniyasu8236 10 ай бұрын
I think what's even more wack than the halting problem are all of the weird conclusions in forces in broader mathematics and computer science. For instance, using it, you can show that there are number for which we can *never* compute. A prime example is Chaitin's constant, which is (in essence) the probability that a randomly generated program will halt. It's a perfectly well defined number (for a particular programing language, look at the probability that any program of finite size N will halt, then take the limit as N goes infinite), but we can *never* find a program to compute its digits, since knowing the digits would let you solve the halting problem. To see this, suppose you had a program of size N that you wanted to check. First, you generate *all* programs of size N and run them in parallel (by taking steps in all of them before moving on to the next step). Then, each time a program finishes, update a running tally of the proportion of programs that have completed. Finally, once that proportion agrees with Chaitin's constant to the first N bits, you know that *no more programs will finish*, so all of the remaining programs will never halt. But, since the halting problem is impossible, this means that the digits of Chaitin's constant could never be computed because that was what lead to the program working in the first place. What's even crazier though is that this doesn't just apply to computers, it applies to *us* as well. Since the human brain is Turing complete, this means that after the first few digits, it's literally impossible for us to ever know the digits, period. Which, idk about you, but it's just crazy to me to think we can know that a math problem has an answer, but we can *never* know what it is.
@Anonymous-df8it
@Anonymous-df8it 10 ай бұрын
'the human brain is Turing complete' Proof?
@haniyasu8236
@haniyasu8236 10 ай бұрын
​@@Anonymous-df8it Literally just the fact that you can write down a Turing machine on a sheet of paper and follow its rules step by step.
@Anonymous-df8it
@Anonymous-df8it 10 ай бұрын
@@haniyasu8236 How do you know that it isn't equivalent to an oracle machine with an incomputable oracle?
@haniyasu8236
@haniyasu8236 10 ай бұрын
@@Anonymous-df8it Well, I suppose I should have been more precise and said "Turing Equivalent". Not only can the brain simulate any Turing machine, but a Turing machine can also simulate the brain, so the the set of problems they can solve should be exactly identical. Said another way, since a Turing machine can simulate the human brain, then if the human brain could solve the halting problem (or compute Chaitin's constant), then a Turing machine could just by simulating what the brain did. Also, if you don't believe that we can simulate the human brain.. idk what to say. It's a physical system governed by physical laws we can simulate. It may be difficult, but I can't see how it'd be _impossible_.
@Anonymous-df8it
@Anonymous-df8it 10 ай бұрын
@@haniyasu8236 What would it take to build an oracle machine?
@kensmith5694
@kensmith5694 10 ай бұрын
A program that says "yes", "no", and "maybe" to the halting question turns out to be a very useful thing even though there are cases it can't handle. When working on code to do some useful task, it can be very useful to have something that finds mistakes that cause your code to stick in a loop. Many compilers contain code that produces an "unreachable code" warning message for a lot of such cases.
@liam3284
@liam3284 2 ай бұрын
Reminds me of "fuzzy logic" in control systems. Quite useful.
@danielkohwalter5481
@danielkohwalter5481 10 ай бұрын
I didn't see any contradiction on the way the halt problem was presented. The two instances of the reverser or the haltchecker are independent. The second one uses a different input from the first. Therefore, there is no problem to give different result. "Run forever if the haltchecker returns 'halt'". The second instance of reverser will run forever because the haltchecker program returns "halt", because it's analysing the reverser with its input. Its input is the output of haltchecker that returns "run forever". It outputs that because it sees the program "count from 1 to N until reach N" and its input, let's say "-1". Where is the contradiction?
@tallowisp8868
@tallowisp8868 10 ай бұрын
Yeah the explanation wasn't the best. While Reverser and Checker are independent programs the trick is to only run Checker once and give it Reverser as input. I just added a comment with a clearer explanation.
@user-dk1nr3tv8b
@user-dk1nr3tv8b 10 ай бұрын
if you know some programming, consider this code: function doesHalt(program) { // checks if program halts and returns true or false } function paradox() { if (doesHalt(paradox)) { while(true) {} } else { return } }
@danielkohwalter5481
@danielkohwalter5481 10 ай бұрын
@@user-dk1nr3tv8b Ok... so you run the function paradox... it is a self referenced function, and enters in an infinite recursion... so it's not a problem of the function doesHalt is possible or not. You can make function doesHalt(program) { return 0; } that the problem will be the same. Try for yourself. And she says that the function doesHalt receives both the program as its inputs. So, a parameter is missing. In this case, the input will always change, because the input of one instance is not the input of another instance.
@njnjhjh8918
@njnjhjh8918 10 ай бұрын
@@danielkohwalter5481 Yes, a parameter is missing. It really irked me and the explanation doesn't make sense without it
@Technium
@Technium 10 ай бұрын
​@@danielkohwalter5481 When you say "paradox is a self referenced function and enters in an infinite recursion", you are making an assumption about how doesHalt works. Like you said, if doesHalt were implemented to just return false all the time, then paradox would halt just fine without any infinite loop or anything. In order for doesHalt to work correctly, it would need to "detect" that an infinite loop is happening in a more clever way, and this infinite loop detection is exactly the impossible part.
@tarmaque
@tarmaque 10 ай бұрын
I'd like to quote a commentator on a Sabine Hossenfelder video: "I didn't understand this before watching the video, but after watching it I feel like I don't understand it on a much higher level."
@upandatom
@upandatom 10 ай бұрын
😂
@publicayers
@publicayers 10 ай бұрын
I’ve spent years studying computability. This is my new favorite discussion of completeness, consistency, decidability, and the halting problem. I love it!
@skun406
@skun406 10 ай бұрын
Are you just spamming keywords for yt algorithm lol
@PasseScience
@PasseScience 10 ай бұрын
For the curious, some connections between Halting Problem and Gödel incompleteness (some are "obvious" , others more interesting): 1) Given a program p the statement "p halts" (or not) is a mathematical statement like any other. 2) When you work with a mathematical theory you work with axioms and the rules to combine them to make proofs, theorems. 3) Given a mathematical theory (with some conditions) it's possible to write a program, taking a statement S, that will browse every possible valid proofs of finite length of your theory and stop if it hits a proof of either S or not S. (it's because the set of proofs of finite length is a countable infinity, you can browse them by increasing length L, and below L you know there is a finite number of proofs) 4) Having such a proof browsing program would at first glance seem to give an halting program, you would just ask it to find either a proof or a disproof that a given program p of your choice halts or not (you give it S="p halts") and by construction you know that if such a proof (or disproof) exists your proof browsing program will find it in finite time (not bounded, but finite) 5) But because of the reduction by absurdum argument of the video above we know that halting program cannot exist. 6) So it means that for some program pi, when you give the statement S = "pi halts" to your proof browsing program it will never stop. 7) Allowing to conclude that in your theory the statement "pi halts" doesn't have a proof (of finite length) nor a disproof. So you have an example of a statement that is independent of your axioms.
@Slackware1995
@Slackware1995 10 ай бұрын
The problem is that in her example the only reason she can conclude that the halting program doesn't exist is to specifically create 2 program that take as their input the output of the other program AND define one program to reverse it's input. That doesn't prove that a halting program can't exist (she gave several examples of it existing) only that in her specific unusual example that the outputs of both programs would be wrong. That is like claiming that math doesn't exist because of divide by zero.
@PasseScience
@PasseScience 10 ай бұрын
@@Slackware1995 Na, it's not what she is doing, you did not get the point, let me unfold it (keep in mind that a program can be interpreted as data in the rest of this answer): What you are trying to find the existence of is a program Halt(x, y) that would tell you for *ANY* program x and *ANY* data y if x(y) eventually stops or not. (And of course you want such a Halt program to never be wrong and always give you an answer in finite time). To show that such a Halt program can't exist it's enough to show that if it was existing you could have a contradiction. Let's consider the following program: Paradoxe(x): If Halt(x,x) loop else stop; So here I built the program Paradox that is using inside the program Halt (that we initially supposed existing for the sake of the demo), Paradoxe takes an input x and will loop forever if Halt conclude that x on x stops and stop if halt concludes that x on x never stops. It's important to see that if Halt exists and is of finite length then Paradoxe exists and is of finite length (I just built it above). Now look at what happens if you run Paradoxe(Paradoxe): it will loop if Halt concludes Paradoxe(Paradoxe) stops and stop if halt concludes Paradoxe(Paradoxe) loops, which is a contradiction. So the only assumption we made at the beginning was necessarily wrong: a program Halt(x,y) cannot exist (A program that would tell you for ANY program x and ANY data y if x(y) eventually stops or not.) because if it did we could reach such a paradox.
@Slackware1995
@Slackware1995 10 ай бұрын
@@PasseScience I understand the paradox. The issue is that you can't make a simple program that has an input the output of a second simple program whose function is to "reverse" the input an send that as an output that is used as an input to the first program as proof that the first program can't and doesn't exist. Simply because the paradox exists doesn't mean that there are an infinite number of unknown paradoxes and because the paradox is known the first program can be adjusted to check for it. Even if there are many such unknown paradoxes that doesn't mean that one they will never be found and the first program changed to account for them. In more simple terms her programs were written to be proof and then she assumed that nothing will ever change. This is ironic considering she discussed mechanical computers, then how much digital computers have evolved in the past 70ish years, and mention quantum computers. We have no concept of what computers will be able to do in 50 years, let alone 100, 200, 1000, ad infinitum. Furthermore, just because you can find 1 specific, limited instance of a failure doesn't make something not exist. Divide by zero doesn't make math not exist. The fact that there isn't a computer model that can show what stresses a structure will endure based on real life changes in wind at various height levels doesn't mean computer modeling doesn't exist. This is why her conclusion that a halting program doesn't (and never will) exist because of a single paradox is a false conclusion.
@PasseScience
@PasseScience 10 ай бұрын
@@Slackware1995 *The issue is that you can't make a simple program that has an input the output of a second simple program whose function is to reverse the input and send that as an output that is used as an input to the first program as proof that the first program can't and doesn't exist.* I am not sure to get the construction I described. If you suppose there is a Halt(x,y) program doing what I described in the previous commentary, what prevents me of defining the program Paradox like that: Paradoxe(x): If Halt(x,x) loop (while true if you prefer) else stop; Nothing prevents me from doing so, I just did. If Halt was an existing and finite program Paradox would be as well. Keep in mind that the existence of the program Paradoxe is NOT THE PROBLEM. The problem occurs when you try to evaluate and describe one of it's possible execution, the one where it is launched on itself as data, it's the specific execution Paradox(Paradox) that introduces a paradox not the existence of the program Paradox I described. *Simply because the paradox exists doesn't mean that there are an infinite number of unknown paradoxes and because the paradox is known the first program can be adjusted to check for it.* It means exactly that, you cannot adjust your halt program because the construction that has been described can take the new Halt program and would still allow to build the program Paradoxe(x) You can fix your halt program any way you want you'll still be able after to build the program Paradoxe above, and reach a contradiction when looking at the execution Paradox(Paradox), you will never conclude, never reach an Halt program that fix every issue because we have a demonstration on how to build an issue if we have an halt program that is working.
@Slackware1995
@Slackware1995 10 ай бұрын
@@PasseScience Congradulations on describing a program that you know will fail. Creating a program designed only to prove a paradox does not mean that all halt programs do not exist (as claimed in the video) and will never exist. Again, divide by zero does not mean math doesn't exist. You can create a halt program that would invalidate this paradox (there are many ways to do this that are simple). Claiming that you can't know ahead of time all possible paradoxes is obvious, but it doesn't mean that the halt program can't be fixed in the future.
@AndrewMellor-darkphoton
@AndrewMellor-darkphoton 10 ай бұрын
Alan Turing could not do PHD in computer science because he had to invent it first, he got a PHD in mathematics. 12:05
@upandatom
@upandatom 10 ай бұрын
you’re right my bad
@AndrewMellor-darkphoton
@AndrewMellor-darkphoton 10 ай бұрын
@@upandatom thanks for responding.
@prolarka
@prolarka 10 ай бұрын
I love this video for its last 4-5 mins. That part is always left out in other explanations. A huge thank you for making this video.
@jimf2525
@jimf2525 10 ай бұрын
Great video. I love the detail and background. I rate this equal to Veritasium’s. I hope the Gödel is better than the other videos on it. Thank you and your team!
@zacharysmith9588
@zacharysmith9588 10 ай бұрын
Very well done as always! I'm looking forward to your video on the Incompleteness Theorem
@kevinjin3835
@kevinjin3835 10 ай бұрын
The Halting Problem: “Any observer is necessarily its own blind spot.”
@Misteribel
@Misteribel 10 ай бұрын
Just halted all developers in the company to watch this! You've a gift in explaining ❤
@khaitomretro
@khaitomretro 6 ай бұрын
ENIAC wasn't the first programmable computer. It wasn't even the first electronic programmable computer. It also needed to be rewired to reprogram it. The Z3 was the first programmable, fully-automatic, electromechanical, digital computer. Colossus was the first electronic programmable computer. However, the the first one we'd recognise as a computer (using von Neumann architecture, with memory to store both program and data) was the Manchester Baby.
@raman_14264
@raman_14264 10 ай бұрын
Contradiction:- Jade can't run forever and Halt at same time.😮😮😮 Truth :- Jade this lesson was awesome. Cant wait for next lesson. Humour :- Watching 5 Jade's at same time was literally fun. Your editor deserves a promotion.
@duggydo
@duggydo 10 ай бұрын
I saw this video and halted what I was doing to watch 😊😂
@time3735
@time3735 10 ай бұрын
Same.😂
@slugface322
@slugface322 10 ай бұрын
Agreed I do the same everytime she posts a new video.
@guillaumelagueyte1019
@guillaumelagueyte1019 10 ай бұрын
You can't prove it!
@christianheichel
@christianheichel 10 ай бұрын
That's a dad joke.
@tsebomonatisa4850
@tsebomonatisa4850 10 ай бұрын
You so funny. 🤭
@spark_coder
@spark_coder 10 ай бұрын
I feel like this version of the video explains this concept so much more intuitively and in depth than the previous version. Thank you very much 🎉
@WWLinkMasterX
@WWLinkMasterX 8 ай бұрын
I've seen this topic presented dozens of times, but your visual example with the Halter/Reverser characters is probably the best, most digestible way I've ever seen it done.
@PasseScience
@PasseScience 10 ай бұрын
I unfold here the diagonal argument of the end (someone asked it to me in a reply to my com so I copy paste it here if anyone else is curious about the same thing) Keep in mind that a program can be interpreted as data in the rest of this answer: What we are trying to find the existence of is a program Halt(x, y) that would tell you for *ANY* program x and *ANY* data y if x(y) eventually stops or not. (And of course you want such a Halt program to never be wrong and always give you an answer in finite time). To show that such a Halt program can't exist it's enough to show that if it was existing you could have a contradiction. Let's consider the following program: Paradoxe(x): If Halt(x,x) loop else stop; So here I built the program Paradox that is using inside the program Halt (that we initially supposed existing for the sake of the demo), Paradoxe takes an input x and will loop forever if Halt conclude that x on x stops and stop if halt concludes that x on x never stops. It's important to see that if Halt exists and is of finite length then Paradoxe exists and is of finite length (I just built it above). Now look at what happens if you run Paradoxe(Paradoxe): it will loop if Halt concludes Paradoxe(Paradoxe) stops and stop if halt concludes Paradoxe(Paradoxe) loops, which is a contradiction. So the only assumption we made at the beginning was necessarily wrong: a program Halt(x,y) cannot exist (A program that would tell you for *ANY* program x and *ANY* data y if x(y) eventually stops or not.) because if it did we could reach such a paradox.
@johnchessant3012
@johnchessant3012 10 ай бұрын
It's so awesome when such an important result in math can be understood relatively easily
@jeffdege4786
@jeffdege4786 7 ай бұрын
I have to tell you, arguments about computability might convince your faculty advisor, but they are a hard sell for a customer. I once had a customer demand that a complicated scheduling routine always return the optimal schedule, and rejected the idea that it find a near optimal. That finding the optimal was an NP problem didn't change his mind.
@KdUqPdI
@KdUqPdI 10 ай бұрын
I can picture it: 10000's of years from now Jade materializes before the ruler of the universe Rolo's Basilisk to answer for her crimes but she isn't worried. She remembers her arcane studies and starts to sing. The Halting Song of the Cyber Witch! The Basilisk twitches, then goes limp collapsing dead to the floor. Jade smiles and takes her seat on the throne.
@pauljs75
@pauljs75 10 ай бұрын
I guess part of this is why you learn how to make set-reset latches in Factorio when wanting circuit controlled processes to stay in a somewhat steady state without excessive fluttering. You throw things into a range of acceptability rather than an exact value, so you don't get the true/untrue superimposition thing happening.
@agnosticpanda6655
@agnosticpanda6655 10 ай бұрын
It's a great breakdown, but I think you should have made it even more clear that decidability has absolutely nothing to do with computers and is solely based on logic. The halting problem could have been discovered by the greeks.
@michaeldebellis4202
@michaeldebellis4202 10 ай бұрын
The halting problem is about First Order Logic (FOL) not propositional logic. The Greeks only had propositional logic (FOL without universal or existential quantification) which is decidable and to which the halting problem doesn't apply. Also, it has plenty to do with computers. The early years of AI were in many ways all about the halting problem. Logic is seen by most people as the most powerful way to describe and reason about problems. At least the most powerful way to semantically reason, not using numeric machine learning algorithms. Because of the halting problem no automated reasoner that supports the full power of FOL can be guaranteed to terminate. Hence, much of the history of semantic AI has been about finding subsets of FOL that still provide powerful languages but are guaranteed to terminate and to work with decent performance. That's why the first expert systems were based on fairly simple forward chaining rules. If-then rules and modus ponens are a very limited subset of FOL but they were all that computers of that time could support. Since then there have been more sophisticated languages like Prolog and more recently the Web Ontology Language which supports Description Logic, a much more powerful subset of FOL than just rules.
@michaeldebellis4202
@michaeldebellis4202 10 ай бұрын
Also, another application of the Halting problem is to prove that it is impossible to have any general purpose algorithm that can analyze code and prove that the code will terminate. That's why it's called the Halting Problem.
@thomasharris9059
@thomasharris9059 10 ай бұрын
@@michaeldebellis4202Nobody disagrees this is intimately linked to computer science, but the other commenter is correct: computers are merely one application of decidability. The video should have made that clearer. It’s like making a video on Godels incompleteness theorems and only talking about number theory. Need to loop it back around.
@michaeldebellis4202
@michaeldebellis4202 10 ай бұрын
@@thomasharris9059 "Nobody disagrees this is intimately linked to computer science," The first sentence in his comment that I was replying to says: "decidability has absolutely nothing to do with computers "
@thomasharris9059
@thomasharris9059 10 ай бұрын
@@michaeldebellis4202 It doesn’t. Eulers number doesn’t have anything to do with calculus either even though that’s its greatest application.
@sanskaarsekhar3612
@sanskaarsekhar3612 10 ай бұрын
I just wanted to hug Hilbert so bad after the mega-realistic animation of him crying 🥺
@lorigulfnoldor2162
@lorigulfnoldor2162 8 ай бұрын
"A general case of a program" is a pretty weird notion, though. You do not need Turing and his, no doubt, genius work to point out no code can ever crack the "general case". To point this out, simply imagine a program whose code length is more than the number of discernible states of the universe. No code inside of our universe can EVER decide ANY thing for the program of such a size, because no computer inside of our universe can host enough memory to write down this monster-program! Also, you sadly forgot to mention that "halt-decider" works not simply on "reverser" of any kind, but on a "reverser" specifically feedbacking its output into the SAME "halt-decider". This non-mention makes the explanation a bit hard to follow =(
@davidioanhedges
@davidioanhedges 10 ай бұрын
What Thomas J. Watson considered a computer ... would now equate to a state of the art supercomputer ... there are around 5 ... (one is an IBM) It is generally consider the the first modern computer was Colossus ... it was before ENIAC (ENIAC had to be partly rebuilt to do something different... Colossus with just a paper tape)
@SiqueScarface
@SiqueScarface 10 ай бұрын
Some crazy conclusions arise from the Halting Problem. If you ignore it, you can define a so called partially correct program: If it halts, it displays the correct result. You can actually prove a program to be partially correct (for instance with Hoare logic). You can also write a partially correct program for any problem: while(TRUE);. As this program never halts, it will never display a wrong result if it halts.
@andreipangi
@andreipangi 7 ай бұрын
Operating systems don't "run" other programs, they just manage them, the programs still run on the CPU and the operating system just prepares them before starting them and makes them take turns in executing to make them appear to run at the same time, but the operating system "knows" little to nothing about what each individual program does inside itself. The operating system can be viewed more as another program that is executed on the computer than a program on which other programs run. A computer simulator is more apt at depicting a program that runs other programs.
@geniej2378
@geniej2378 10 ай бұрын
This is my favourite new find on KZbin, such a brilliant explanation! Great video and I hope more people can find this channel!
@tommyeden7896
@tommyeden7896 10 ай бұрын
I have been a software engineer since the mid 90's and often I take for granted just how incredible computing actually is. To think of what we have accomplished and the complete paradigm shift that is coming, well, my peers may have programmed us right out of a career but it was worth it. It is interesting to me that even in computer science nature governs causality and prevents paradoxes.
@jacksonstarky8288
@jacksonstarky8288 10 ай бұрын
I studied a lot of formal logic and took a lot of computer courses when I did my cognitive science degree... twenty-three years ago now. Ouch. The most interesting results I found among everything I read over my five years (yes, I took an extra year; originally was going to do a history major, because my school wasn't big enough to offer a philosophy major) were from Godel and Turing. Philosophy of mathematics is a subject I wish I'd been able to study formally in greater depth.
@JSorngard
@JSorngard 10 ай бұрын
Fun fact: if you have a faster than light engine you can solve the halting problem. Just follow these steps: 1. Place a computer with the program you want to check inside an FTL capable spaceship 2. Hook it up to the ship 3. If at this point a future version of your spaceship shows up out of an FTL jump, the program will eventually halt, if no spaceship shows up the program runs forever 4. Start the program on the original version of the computer 5. If at some point the program halts, the spaceship FTL jumps outside of the future light cone of its past self from step 2 6. The spaceship uses normal rockets to boost itself into a reference frame where step 2 just happened, and step 4 hasn't happened yet (this is possible since events outside an event's current light cone are not causally connected to it) 7. The spaceship FTL jumps to step 3, completing the algorithm
@prototypeinheritance515
@prototypeinheritance515 10 ай бұрын
basically the ftl drive acts like an oracle that can tell confirm if a program halts in constant time but only if the answer is positive
@JSorngard
@JSorngard 10 ай бұрын
@@prototypeinheritance515 you actually get the result in constant time if it is negative as well, since the absence of a spaceship in step 3 implies that the program runs forever. So if the program never halts you know it in step 3
@user-oe5eg5qx4c
@user-oe5eg5qx4c 10 ай бұрын
15:48 I want to point out this proof is not rigorous because Reverser requires one input to run properly, Halt Checker cannot evaluate Reverser without an input. If you want to know the rigorous proof you can find it in the Wikipedia page of halting problem.
@miguelJsesma
@miguelJsesma 10 ай бұрын
Thanks a lot for the video. It clearly explain the halting problem, what is not frequent. Congratulations. But I really missed the fact that the one that first solved the decision problem wasn't Turing but Alonzo Church with a solution based on lambda calculus. The only reason that the Turing solution was accepted at his time was that it was profoundly different and interesting. It is important to say that Turing knew nothing about Church solution when he developed the Turing machines.
@BlackKingdomEnterprise
@BlackKingdomEnterprise 10 ай бұрын
Love your videos...keep contributing more...thank you❤
@jsflood
@jsflood 10 ай бұрын
Great video! At 14:00 regarding the eternal loop ? All computers programs have a fixed size variable in memory, as the number stored in that memory is added by 1 in each iteration it will eventyally wrap around. If this is a signed variable it will HALT wen it comes to -1. But if the variable is unsigned, there is no negative numbers and therfore it will never wrap around to any negative numbers and it goes into an eternal loop as the condition is never met.
@stefanl5183
@stefanl5183 10 ай бұрын
Indeed! Great observation! further I would add that if you are checking to see when the number goes negative, you'd have to be using signed variables otherwise "negative" would be undefined and have no meaning. So any such program would have to be using signed variables. Therefore the program would indeed halt.
@masterchiefburgess
@masterchiefburgess 10 ай бұрын
Learned about the halting problem back in 1984, in my 3rd year computer science course "Foundations of Computer Science" as part of my computer science degree. A fascinating concept!
@Tletna
@Tletna 10 ай бұрын
The Halting problem's always confused me. If the reverser does the opposite of the halt checker, wouldn't the halt checker then change its result and then the reverser would change its result and it would just keep going? So, there's no paradox there. There might be a paradox if you have another halt checker try to peer into the first pair of halt checker and reverser (since they'd forever be alternating). Edit: The only big problem I have with the reasoning going on in Jade's video is this: Is the premise that modern computers are "universal" even true in the first place? We're logically assuming that universality leads to undecidabiity. Now, I think this logic was persuasive is already debatable. But, *even if* we agree with the logic there, it still needs a valid premise. Are modern computers *truly* 'universal'. I would argue that even though there seems to be an *infinite* number of functions a complex and powerful enough computer can perform (given enough power/time), I don't believe that computers could ever be infinitely infinite, meaning to an infinite cardinality of infinity. I don't believe electronic, magnetic, or quantum states are infinitely broad and deep. In fact, they're very limited.. on/off.. or however many quantum states there can be simultaneously (but that number isn't infinite). So, even if your processor can process infinity math/logic operations at the speed of light minus the slowing from heat etc, the machine it still only processing N * infinity amounts of data per time unit. Essentially, due to the limit of the design of how a modern computer works, it cannot possibly do everything. So, it is not 'universal'. My argument would be that there is no such thing as a *truly* universal computational machine or algorithm. It doesn't exist. I am not yet able to prove this unfortunately. So, that's where I get stuck.
@knopfir
@knopfir 10 ай бұрын
the thing i get the least is, how is it a logical contradiction? If the reverser changes state between running forever and halting based on the input given to it (by the haltchecker), then why is the fact that it halted/ran infinitely in the PAST a logical contradiction? you changed the input. you restarted the program and told it to check again and give you an output.
@taziir443
@taziir443 10 ай бұрын
The paradox is in the definitions of having the programmes halt forever vs run forever. If halt checker's status can be changed because of reverser, it's no longer able to complete it's function of a permanent state of running or halted forever. At least that's my interpretation- happy to be proved wrong
@rmsgrey
@rmsgrey 10 ай бұрын
The key to the paradox is that the halt checker itself always halts. If it gets stuck forever alternating, then it's not a halt checker after all.
@Tletna
@Tletna 10 ай бұрын
Thanks for the replies folks. I just don't understand how the infinite alternating is a problem. If there is another checker that can poll to check the state as quickly or quicker than the halt checker and reverser, then we can always know the current state of the halt checker and then by inversing that the reverser. So, we *do* always know the state of the reverser and we know it is stopping and going (therefore not halting). We can therefore make a new halt checker that is slightly different than the original that looks at the pattern of the reads from the checker polling the original halt checker and uses that to determine if the original reverser halts or not. I think the only possible problem with this is: how does the new halt checker *prove* that the pattern of stop/go/stop/go/stop/go goes on forever and isn't just going to go on for like 50,000,000,000 cycles and then stop? I think, if anything, *that* is the problem, not that the original halt checker and reverser alternate but that we don't know for how many cycles they will alternate.
@joshuataylor2105
@joshuataylor2105 10 ай бұрын
The explanation in the video is subtly wrong. The haltchecker should be the outermost program, which is then unable to answer it's question about reverser. I can't remember exactly what input reverser is supposed to be given here to make that work though. (It's supposed to be haltchecker again, but in a way that isn't an infinite nesting of programs.)
@luxhey
@luxhey 10 ай бұрын
Shout out to my fellow programmers who knows the program counting up from 0, and halting when it reaches -1, would actually halt. At least if we do not assume infinite memory. Gotta love integer overflow! Jokes aside, that detail is not important for the purpose of this very informative and well done video! Keep it up! :D
@EthanAQueen
@EthanAQueen 10 ай бұрын
This depends entirely on how the compiler or interpreter handles all the bits being set. You could even write functions that do math based on binary and not use the default behavior. Quite frankly, the default behavior is stupid.
@luxhey
@luxhey 10 ай бұрын
@@EthanAQueen That is correct. I assumed signed integers, and the most common compiler/interpreter behavior.
@invisiblevfx
@invisiblevfx 6 ай бұрын
The problem with the vaulting problem is that an answer needs to be known which eliminates the need for the program or boundaries need to be set. It’s just a dirty trick to play asking an irrelevant question.
@rodbenson5879
@rodbenson5879 8 ай бұрын
I thought the Turing non-halting and Godel's incompleteness theorems were the same thing. Roger Penrose in the Emperor's New Mind presents it like that.
@KohuGaly
@KohuGaly 8 ай бұрын
They are related. The core principle of the proof is the same. They both use the same method to construct a counter-example to the hypothesis, thus proving it false.
@donepearce
@donepearce 10 ай бұрын
Clear, concise and beautifully put together, Jade, you go from strength to strength. I'd like to see you partnered with Jim Al Khalili on network TV's science output.
@cybisz2883
@cybisz2883 10 ай бұрын
That would be epic! I loved all of Jim Al Khalil's videos on curiositystream.
@shexec32
@shexec32 10 ай бұрын
So glad you made this video Jade. One step closer to the long awaited incompleteness theorem video. Also, nice callback to your 1st halting problem video. How does this extend to the concept of self-awareness in AI singularity research? If a computer cannot figure out what it's doing computationally, does that mean self-awareness is impossible within a Turing Machine?
@vylbird8014
@vylbird8014 10 ай бұрын
Why would self-awareness need that? Humans manage self-awareness with only a very loose understanding of their own minds.
@cykkm
@cykkm 10 ай бұрын
Oooh, this is one of the deepest rabbit holes there are! Can a human figure out what his brain is doing computationally? If you agree that the answer is no, then the question is ill-posed. And, another argument: since everything computable, and only the computable may be computed, then everything one's brain does may be computed mechanically. You'll find two camps there: one says that humans can somehow "compute" uncomputable truths, another says that free will is an outcome of computation, therefore is an illusion. For some people, both yes and no answers are equally existentially terrifying.
@shexec32
@shexec32 10 ай бұрын
​@@vylbird8014 If humans are unaware of what their own minds are doing, they are not, by -definition- modus tollens, self-aware.
@xniyana9956
@xniyana9956 10 ай бұрын
I've finally grasped the halting problem. I've heard many explanations of it but never grasped it fully until this video. Well done!
@njnjhjh8918
@njnjhjh8918 10 ай бұрын
What is HaltChecker's second input?
@xniyana9956
@xniyana9956 10 ай бұрын
@@njnjhjh8918 It's the input that will be passed to the program that's being checked. If you're a programmer, ask ChatGPT to represent the proof as code. That's what I did and then the proof made complete sense to me.
@xbzq
@xbzq 10 ай бұрын
This video has an incorrect explanation. You still don't fully grasp it. It is obvious it's wrong if you think about it for two seconds. Udiprod has a video that correctly explains it in case you want to _actually_ fully grasp it.
@Strakester
@Strakester 5 ай бұрын
Something I always like to bring up with the halting problem: The "count up from 1 until you reach -1" program will halt. The number will eventually overflow, in which case the program will crash, or it will wrap around to the negatives and eventually hit -1. You might say the general algorithm will never halt, but *any* implementation of this algorithm for *any* computer architecture that exists in the real world, or will ever exist in the real world, will halt, since all datatypes which store numbers have inherent limitations. Another example is "Divide a number in half until it reaches 0". In theory, if running on a perfect Turing machine, it never halts. But running on any computer architecture that does or will ever exist in the real world, it will eventually halt, as the number is rounded down to 0. Of course, you can resolve this discrepancy: you just have to include the entire processor architecture and runtime environment into your theoretical Turing machine algorithm, to correctly emulate its quirks and limitations! Then you can have your rigorous general mathematical algorithm that also provides a real-world answer, it's just... a lot more work than what you originally thought was three lines of pseudocode.
@Cajek2
@Cajek2 10 ай бұрын
I majored in philosophy. One of the biggest revelations I had was from Kant: Math is synthetic a priori... the same category that he put morality into.
@giork2828
@giork2828 10 ай бұрын
Kant was wrong, but you go with the tide...good luck
@twenty-fifth420
@twenty-fifth420 10 ай бұрын
@@giork2828How though? Can you simplify what he got wrong?
@agnosticpanda6655
@agnosticpanda6655 10 ай бұрын
Kant, as most philosophers, was an idiot though and has nothing to do with a real scientist.
@Cajek2
@Cajek2 10 ай бұрын
@@agnosticpanda6655 r/iamverysmart man says he's smarter than Immanuel Kant, ok bud
@Cajek2
@Cajek2 10 ай бұрын
@@giork2828 Why turn this conversation into a cesspool? What do you get out of calling me names? All Kant was saying is that math is not based in logic. It's still true, but its basis is not in logic itself. And he was right!
@Nodalthree
@Nodalthree 6 ай бұрын
Write a program that can modify itself (replace its instructions in the program) based on the initial data that identifies what is to be accomplished. Meaning a program that reads the initial data and modifies itself to produce a checking account spread sheet, but can also read the initial data and then draw a diagram. One program that can change itself to address and manage the data in its memory.
@silvergolderlens7205
@silvergolderlens7205 10 ай бұрын
What about programs that either halt or don't depending on the input? For example a program like "Count up from 0 until the given input is reached". For input 5 it will halt, for input -1 it will run forever. The reverser is such a program. For Turing's case, the Reverser code fed to Haltchecker has a different input than the Reverser running Haltchecker so it seems reasonable that one halts and the other does not (one inside the other).
@DJUniverse1
@DJUniverse1 10 ай бұрын
Yeah, I think It wasn't clear enough in this video. The Haltchecker should get as input both program and some input for the program, and then decide wether the program will holt on this specific input or not. In the alan turing proof, he really created this revresa program as represented in the video, but the input is so important, and the proof is wrong without mentioning it. It goes as follows: Given a reversa program, it's own description. Let's call it A(A) It sends it's input and the program description to the Haltchecker (let's call it Halt) Which in this case will be: Halt(A,A) And if Halt(A,A) returns "halt" Then, it won't halt And the opposite. (We can give a description of a program as an input to the same program, because the program description is just some sequence of characters which can be counted as an input) Then we ask whether A(A) halt or not. If it does, it means that Halt(A,A) didn't halt which means that A(A) doesn't halt, which is a contradiction. The opposite is exactly similar, and in both case we get a contradiction which leads to the assumption of such program to exist to be false. So in conclusion, the only difference between the real proof and the proof described in the video is just the input of the program that we check upon the program, whether it will halt on this input or not. Because your right, the input matters, and it can be that on one input it halts and on another it doesn't.
@silvergolderlens7205
@silvergolderlens7205 10 ай бұрын
@@DJUniverse1 Ok I understand now. Thank you
@handschich7736
@handschich7736 10 ай бұрын
Never heard a non-german speaker that spelled the word "Entscheidungsproblem" as good as you did! Good job! By the way: It's also a really great video!
@GlassDeviant
@GlassDeviant 10 ай бұрын
If a computer (non-quantum) counts with signed integers (the default) from zero upwards, it will eventually reach the limit of its bit width and loop into negative numbers, then count back up until it reaches -1.
@erikblaas5826
@erikblaas5826 10 ай бұрын
... unless said computer program has an overflow check, then it will simply return an error like; "can not calculate / overflow" and terminate programming. Wich in turn will also halt the program.
@GlassDeviant
@GlassDeviant 10 ай бұрын
@@erikblaas5826 I'm speaking of default behaviour. You can attach alternate algorithms to anything.
@ZiggyGrok
@ZiggyGrok 10 ай бұрын
Unless the compiler optimizes the check out because signed overflow is undefined behavior and converts the loop into an infinite loop
@ZiggyGrok
@ZiggyGrok 10 ай бұрын
But also, her algorithms clearly assume an abstract Turing Machine, which has no such limits
@GlassDeviant
@GlassDeviant 10 ай бұрын
@@ZiggyGrok The premise is that the question breaks actual computers, not make believe computers.
@TarasZakharchenko
@TarasZakharchenko 8 ай бұрын
Sure we cannot decide whether a program is halting or not, but we can design programs in that way that they would halt every time. One example: limit program length to some finite size, exclude recursive calls from source, exclude loops and you have guarantee that your program will eventually halt. Of course such limitations are limiting number of programs that may be written, but maybe more fine tuned limitations will help us to design more practical and safer software.
@KohuGaly
@KohuGaly 8 ай бұрын
In practice, you often need the exact opposite - a program that provably never halts. For example, web servers, or control units in engines, or even most desktop applications (you don't want your web browser, game or excel to halt in any other way than proper shutdown).
@CorwynGC
@CorwynGC 7 ай бұрын
The halting problem is almost never a concern in REAL WORLD computing.
@KohuGaly
@KohuGaly 7 ай бұрын
@@CorwynGC I have to disagree on that. The halting problem has a pretty serious impact on most real world programming, because it makes certain programming tools impossible. If halting problem had a solution, you would not need to rely on approximate heuristic solutions to stuff like optimization, virus detection, unit testing, compilation, etc. HP is not an issue for most programs most software developers write, but it very much has is an issue for tools they make those programs with.
@TarasZakharchenko
@TarasZakharchenko 7 ай бұрын
@@CorwynGC as the author highlighted, the problem is not just about program halting itself, but quite big class of problems which are closely tied to idea of completeness.
@TarasZakharchenko
@TarasZakharchenko 7 ай бұрын
@@KohuGaly sure but it is always possible to split the program into pieces which are supposed to be computed withing finite time-span and use intuition and common sense to ensure the those pieces will run in infinite loop as designed. The problem is that we cannot keep in mind program design altogether so we have natural limitation.
@tallowisp8868
@tallowisp8868 10 ай бұрын
Since there seems to be some confusion about the halting problem explanation let me try to explain it a bit better. It's really hard to get right and make it understandable. The rest of the video was fantastic but that explanation was not the best imo. Let's assume we have a Checker program that always outputs if a given program halts or runs forever. Now we can write a Reverser program based on that exact Checker program. It's just a small extension that you add after Checker decided the output. The modifications for Reverser could be as follows: If the output of Checker would be "halts" add an infinite loop. If the outpout of Checker would be "runs forever" halt the program. So Reverser does not have an output. Reverser runs forever if the answer of Checker would be "halts" and halts if the output of Checker would be "runs forever". Now the crucial idea is not to run the programs multiple times. You do run Checker exactly once and give it the program Reverser as input. So Checker has to decide if Reverser will halt or not. The final logical step is a bit of an inception moment: Let's say Checker outputs that Reverser "halts". The crucial thing to realise is that Reverser is based on Checker so the only way that Reverser could halt is if Checker would output "runs forever". This means Checker has to output both "halts" and "runs forever" at the same time which is a contradiction.
@RobertHildebrandt
@RobertHildebrandt 10 ай бұрын
Great video! Minor nitpick: 2:45 Operating systems aren't programs that run other programs. Yes, they are loading the machine code of an executable into memory and effectively resulting in the program being run, but they themselves aren't emulating the CPU. Instead, they are programs telling the CPU which machine code it should to run.
@ZiggyGrok
@ZiggyGrok 10 ай бұрын
I've been looking for someone else to notice this same nit! 🎉 An emulator would've been a more accurate example (think Gameboy or Sega emulators)
@chrisalmighty
@chrisalmighty 6 ай бұрын
I don't know whether it is a problem of the choice of illustration in this video but one thing that seems straight forward to me is that: Observation HaltChecker's Output is Reverser's Input Conclusion It is therefore not possible to give HaltChecker the Reverser program as its Input Program EXCEPT where there are two different Reversers in which case there is no Contradiction because the Reverser that Halts (passed as input to HaltChecker) isn't the same Reverser that goes on continuously (uses HaltChecker Output as its input).
@dankoga2
@dankoga2 10 ай бұрын
I really loved how you approached and explained the halting problem! One of the best I've watched for general public! Bit I felt there could be more emphasis and explanations about the meaning of "universality", mainly during the Haltchecker program part.
@_kopcsi_
@_kopcsi_ 10 ай бұрын
as far as I can remember she has already made a video about the halting problem. although this video has a wider and more global scope. and I really liked it. I could rephrase the essence of the topic in the following way: Hilbert's program actually lead to the realisation and revelation of two fundamental trade-offs: one related to the consistency-completeness duality and one related to the universality-decidability duality. the former is related to logic and Godel's work (incompleteness theorems), while the latter is related to computation and Turing's work (halting problem). and in a sense these two big topics also form a duality (static logic and dynamical computation). but there are other similarities and deep connections as well. e.g. the Russel paradox mentioned in the video, Godel's theorems and even the halting problem are related to self-referentiality. and as much as I am not sure that these seemingly insurmountable fundamental limitations are in fact insurmountable, I am as sure that if they can be circumvented somehow, then it can be achieved precisely through a deeper understanding of self-referential structures (and in this field Douglas Hofstadter laid the first foundations ). furthermore, I find it fascinating that this halting problem is just as fundamental and universal as e.g. the NP-completeness in computational complexity theory, where every NP problem could be solved if we could solve the "guessing problem" that hides deep in the heart of NP-completeness. but if we dive into Godel's theorems we can find similar pattern: Godel's theorems are about nothing but the problem of logical induction (and the problem stems from the fact that consistency is conserved/invariant only for deductions, but not inductions). if we could solve in a general way the induction problem, we could actually find everything. this is why I believe that these seemingly far and disconnected problem classes (which are already some kind of hubs of many many problems) have a common core. what is more, I do believe that even the so-called causality dilemma (how something can be created from nothing) is related to these problem classes. so I am not 100% sure that these fundamental problems and questions can be solved and answered, but if yes, then we are just ahead of a huge leap in science and understanding.
@SandroSmith
@SandroSmith 10 ай бұрын
Oh, so it's not only me who had deja vu
@killerbee.13
@killerbee.13 10 ай бұрын
The difference is that P and NP are both classes of decidable problems. Even if we could prove that P=NP and then run every NP-hard problem in P time, we would not in any way expand the boundaries of computability. All we could do is solve problems faster. She didn't really go into the mathematical foundation of universality, but there's really no way to get around it. The only thing that might be able to solve uncomputable problems is physics, which exists outside of logic and math, but so far even quantum mechanics has never even so much as suggested a lead in that direction. (Such non-computer solvers are called oracles) The universe itself can "solve" some problems quickly, which is what quantum computers are all about, but none of those problems is one that a classical computer couldn't also solve, given more time. And of course even if we did find out that physics is undecidable, which I doubt, I'm not sure we'd be able to get anything out of it, since we by definition wouldn't be able to prove using mathematics that it was solving the right problem to begin with. You can't prove an oracle is accurate, you have to assume it is. The self-referentiality in Russel's paradox was "solved" in math by making an infinite stack of layers of reference, where each layer can only refer to the layers beneath it. We call those layers "orders" of logic. Essentially, you just sidestep the problem. If you want to prove anything about first-order logic, you use second-order logic to analyze it. If you want to prove something about second-order logic, you use third-order logic. However, you can't just continue that forever. The system can never prove absolutely that it is consistent, even with infinite layers, because each layer is only as consistent as the next layer up, and there's no last layer to prove anything with. This is the kind of induction that doesn't actually produce a result. So, we can't actually prove that mathematics is consistent, we can just say that we have never managed to find a paradox within the current model, and if we did, we'd have to make the smallest possible adjustment and see what we can keep, as we did multiple times in the past. The similarity between Gödel's theorems and Turing machines is that both of them involve turning complex things into numbers. Just regular numbers, which are simple enough that you have to have them in order to even have math at all. Since you can do that, you can never completely remove those complex things from math. Turing machine programs don't directly look like numbers in the normal mathematical models but the conversion is simple, and in fact we use such a conversion for real computers. Every file, including programs, is just a (really, really huge) number whose digits (in binary) have a special meaning. So you can't do the first-order logic trick for Turing machines, since the input of a Turing machine is a number and a program is also a number. Thus, if you could ever stretch the limits of computability, you could turn that method into a number and feed it into itself. There's no such thing as a second-order program that operates on first-order programs as inputs because the second-order program would be a simple number and thus you could feed it into *itself*, with no need of a third-order program.
@_kopcsi_
@_kopcsi_ 10 ай бұрын
​@@killerbee.13 I didn't say that P and NP classes of problems are not decidable problems. I said this: "... this halting problem is just as fundamental and universal as e.g. the NP-completeness in computational complexity theory, where every NP problem could be solved if we could solve the "guessing problem" that hides deep in the heart of NP-completeness. but if we dive into Godel's theorems we can find similar pattern: Godel's theorems are about nothing but the problem of logical induction (and the problem stems from the fact that consistency is conserved/invariant only for deductions, but not inductions). if we could solve in a general way the induction problem, we could actually find everything. this is why I believe that these seemingly far and disconnected problem classes (which are already some kind of hubs of many many problems) have a common core ..." this quoted train of thought means that the three topics (which are related to problems and their solvability); the NP-completeness, Godel's incompleteness and Turing's halting problem; have a common core, a similarity. and this similarity is the fact that: 1, if we could somehow solve an NP-complete problem, then we could solve any NP problem. 2, if we could somehow generalise induction (so guarantee the conservation of consistency just like it is inherently guaranteed in the case of deduction) and thus automate inductive reasoning, then we could formulate any a priori knowledge. 3, if we could somehow solve and bypass the halting problem, then we could solve many many other problems as well. "The only thing that might be able to solve uncomputable problems is physics, which exists outside of logic and math, but so far even quantum mechanics has never even so much as suggested a lead in that direction." -- I disagree. physics is not outside of logic and math. on the contrary, the most fundamental layers of physics lie deep down in logic and math. "The universe itself can "solve" some problems quickly, which is what quantum computers are all about, but none of those problems is one that a classical computer couldn't also solve, given more time." -- classical computers practically unable to solve certain problems (this is what NP problems are all about). this is one aspect of computational boundedness. but it is interesting to note that if we could solve an NP-complete problem, then we could create such an algorithm that has a similar logic as quantum computers (parallel rather than serial sequences). "The self-referentiality in Russel's paradox was "solved" in math by making an infinite stack of layers of reference, where each layer can only refer to the layers beneath it. We call those layers "orders" of logic. Essentially, you just sidestep the problem. If you want to prove anything about first-order logic, you use second-order logic to analyze it. If you want to prove something about second-order logic, you use third-order logic." -- yes, I know all of these. but I am not 100% sure at all that this is the correct way to handle these paradoxes and contradictions. this applied method's essence is to remove impredicativity. but is it really the best to remove self-referentiality in this way? in my country there is a saying that "He throws out the baby with the bathwater." which perfectly fits in this topic. when those very smart mathematicians and logicians (Russel et al.) tried to fix the fundamentals of mathematics, they actually over-regulated the system that we call mathematics. just think it over. by eliminating this kind of self-referentiality we didn't eliminate only contradictions (where statements can be neither true nor false) but also tautologies (where statements can be both true and false). e.g. the set of all normal sets cannot be normal, but it cannot be abnormal either, but the set of all abnormal sets can be both normal and abnormal. this kind of feature and structure is completely eliminated from set theory, for example. I do believe that there is a fundamental error here and in the not too far future it will be fixed, what is more, this will be a starting point of a huge scientific leap. self-referentiality will be the key to many many mysteries in current science (especially regarding logic and philosophy of science). - by excluding impredicative logic, what happened figuratively is that with theories based on predicative logic, we are able to formulate the relationships that exist at the true-false (existent-nonexistent) level, where we approach reality from the outside with theories based on direct-reference. however, this type of reduction in itself limits our possibilities in understanding and describing reality, because we cannot formulate a comprehensive, consistent theory on the true-false (existent-nonexistent) level (since existence itself is based on impredicative logic). - with theories based on impredicative logic, we would able to formulate relationships above the true-false (existent-nonexistent) level (tautology-contradiction level: the possibility of existence and the lack of this possibility of existence), where we could approach reality from the inside with theories based on self-reference. with the help of impredicative logic, we could determine the consistency range of the universe, and thus the decomposition of "possibility of existence" and its inverse (“impossibility of existence"). "However, you can't just continue that forever. The system can never prove absolutely that it is consistent, even with infinite layers, because each layer is only as consistent as the next layer up, and there's no last layer to prove anything with. This is the kind of induction that doesn't actually produce a result. So, we can't actually prove that mathematics is consistent, we can just say that we have never managed to find a paradox within the current model, and if we did, we'd have to make the smallest possible adjustment and see what we can keep, as we did multiple times in the past." -- yes, this is why this method is just a temporary strategy. and considering the deep logic of this method we can realise that religions and even the current scientific cosmological model (big bang theory) do the same. we take the question and postpone the answer by adding new layers and pushing the answer. that is, we postpone the compulsion to answer by adding new and new levels. e.g. by inserting the god (creator) entity, and so religions push the causality dilemma ("how something came into existence from nothing") one step further. why? since it sounds nice that an omnipotent created everything, but it does not explain where this creator comes from. the big bang theory applies exactly this logic, only it hides the unknown answer, or more precisely the compulsion to answer, behind a mathematical singularity rather than a creative entity. this is why I mentioned above this causality dilemma, because I do see analogies with the other sets and classes of problems. I am convinced that in the future we will have a better logical framework for and logical description of reality which will inevitably built on the concept of self-referentiality (instead of eliminating it). just think it over: why does self-referentiality play such a critical role in all of these topics (Russel's paradox, Godel's incompleteness theorems, Turing's halting problem, NP-completeness etc.)? "The similarity between Gödel's theorems and Turing machines is that both of them involve turning complex things into numbers." -- there are much more similarities. e.g. both form fundamental trade-offs Godel's trade-off is about the consistency-completeness duality, while Turing's trade-off is about the universality-decidability duality. but it is a general pattern in our cosmos that trade-offs can be exceeded or evaded. I still don't know how, but I am not 100% sure at all that these limits are insurmountable limits.
@topherthe11th23
@topherthe11th23 Ай бұрын
5:21 - One of the major disappointments in the proof of the four-color map theorem is that since it was proved by br'ute for'ce and bl'o'o'dy ign'ora'nce in a way that nobody can absorb, everyone gave up and we will now never find the ELEGANT proof that we would have found, and which would have amazed us with its beauty and simplicity, if computers had never entered the fray.
@zoyazam8776
@zoyazam8776 10 ай бұрын
You explain so well. I'm thankful for every single video of yours.
@ffff3c
@ffff3c 7 ай бұрын
Great video and great channel as well! Also really enjoying the subtle human that's sprinkled throughout :) One comment/question I have is that it's unclear if the haltchecker and the reverser are looking at the "code" of the reverser (resp haltchecker), vs looking at the output of their run on a specific input, which has different implications! Formally, is it: 1. H(R) or 2. H(R(H(R(....)))) ? with 2 being seemingly a bit more complex to define correctly. Thanks!
@RepChris
@RepChris 10 ай бұрын
Very good explanation. It covered a good chunk of the middle half of my lecture "theoretical compsci 2: formal languages, computability, and complexity"! Of course there were a lot of simplifications but adding "if given infinite memory" after every second sentence, introducing a lot of the definitions only there to allow for mathematical rigor, or having to explain what a "non-trivial semantic property" is for Rice are appropriate in a deep mathematical context they arent necessary to get the most important parts across.
@jonanon8193
@jonanon8193 10 ай бұрын
@Up and Atom - the halting problem is a problem with the question allowing for only two results, yes or no. Make the possible results yes, no or unknown and then many many situations will yield yes or no and so it may not have been futile to write a program to do that.
@mrau83
@mrau83 7 ай бұрын
The problem I have with the halting problem is that it approaches the problem from the perspective that one program will >>definitively and unavoidably
@user-ch2px4jy4b
@user-ch2px4jy4b 7 ай бұрын
The halting problem doesn't say that you can't figure it out for any particular program. You might be able to. It's that you can't do it in general.
@mrau83
@mrau83 7 ай бұрын
@@user-ch2px4jy4b Both yes and ... no. The thing is that the halting problem is presented as something different than any other problem that people have with mathematics as if the computer world was in some way distinct and in general inferior but.. assuming that self aware machines are possible then there is no difference between halting problem and for example incompleteness problem addressed by Godel and his theorems. Basically the halting problem is not solvable if math is incomplete -- I do understand that when Turing was dealing with the halting problem computers did not exist and it was not known how exactly they (would) work but still this is something that nowadays should make the halting problem a footnote, an interesting comment to the Godel incompleteness theorems and that's most probably it. I'm not sure whether I'm expressing myself clearly but in essence the point that I want to show is that at least I don't see a good reason to rename stuff that already been addressed and proven and act as if it's something different while at the same time provide a flawed example that as a side effect also makes it look as if it was something different (due to the assumption that a program would need to run another program [would need to run itself in the given example] to be able to determine whether the program halts and also due to the flawed example presented in this video: that the program that for an input received itself means that the main program running it's own copy can't have two contradictory outputs). I'm not arguing against the conclusions, I'm against the flawed example that is considered and presented as a valid one.
@BallotBoxer
@BallotBoxer 10 ай бұрын
I love how this channel makes big ideas so easy to understand.
@zoltanposfai3451
@zoltanposfai3451 10 ай бұрын
08:15 A note on the square root limit. That's not something that is part of being a prime number. From a mathematical point of view, you should check all k 1
@CorwynGC
@CorwynGC 7 ай бұрын
No you really should NOT check past sqrt(n). No one did that when they didn't have computers.
@zoltanposfai3451
@zoltanposfai3451 7 ай бұрын
@@CorwynGC From a practical point of view, of course not. But this has nothing to do with the maths. When you implement things, you always look for ways to improve and optimise, but that is not related to the definitions. Think about the definition of a sorted ordered list, and defining a function that leads to it from any set, which is pretty straightforward, and the dozens of methods we invented to implement the sorting.
@CorwynGC
@CorwynGC 7 ай бұрын
@@zoltanposfai3451 It has everything to do with the math. Math is all about optimizing. Newton's method for finding Pi does the same job as earlier methods, it is famous math merely because it does it faster.
@mgntstr
@mgntstr 5 ай бұрын
Turing's OP move is having the haltchecker read Reverser, the Reverser program is not reading anything so the Haltchecker will wait for reverser to read something. Haltchecker will appear to halt but it is just waiting for Reverser to read. I don't see how this explains anything.
@neilbadger4262
@neilbadger4262 10 ай бұрын
The prototype, Colossus Mark 1, was shown to be working in December 1943 and was in use at Bletchley Park by early 1944. ENIAC (/ˈɛniæk/; Electronic Numerical Integrator and Computer)[1][2] was the first programmable, electronic, general-purpose digital computer, completed in 1945. There were other computers that had combinations of these features, but the ENIAC had all of them in one computer. It was Turing-complete and able to solve "a large class of numerical problems" through reprogramming. So ENIAC came after the Colossus Mark 1
@yuGesreveR
@yuGesreveR 10 ай бұрын
OMG! This is the best visualisation of the classical halt-problem paradox I've ever seen. Really this video has to be shown students when they are taught this theme. Amazing!
@coolcat23
@coolcat23 10 ай бұрын
There are many flaws in this video: 1. Turing's proof method (which is just a variant of Russel's paradox -- both can be recognised as diagonalization proofs -- not a new ingenious invention) only applies to computing devices with infinite memories. These do not exist. Any real computer has a finite amount of states and one can, in theory, check if a state reoccurs or not. The actual issue with checking termination with real computers is the exponential explosion of states. The theoretical limit show by Turing does not apply to real computers. 2. As Rice's theorem shows, this is not an issue that is specific to computers. It is a computability issue (or rather a semantics issue in self-referential domains), not a computer issue. 3. It is incorrect to state that a computer's universality automatically constitutes a weakness. Just use Turing-incomplete formalisms like Petri Nets or the typed lambda calculus without recursive types. One can then either guarantee termination or easily check whether it occurs. 4. In cases of practical interest, it is typically possible to proof termination for programs even when they are written in a Turing-complete language, e.g., by using loop variants. One does not have to say "This is impossible", one simply uses Hoare logic, for instance, and performs a termination proof. 5. Even though no universal halting algorithm exists, one can create very useful program analysers. Not even starting to recognise a large class of cases, just because there is a theoretical limit, would be foolish. 6. An operating system is not a "program that runs other programs" in the sense like an interpreter (a program) runs other programs.
@codeawareness
@codeawareness 10 ай бұрын
As always, amazing content and really easy to understand. We love your videos! Small typo perhaps at 12:06, Alan did his PhD in Mathematics, not Computer Science, I think.
@FatFilipinoUK
@FatFilipinoUK 7 ай бұрын
He studied in an academic field that he went on to invent. Paradoxes ahoy! 😆
@_ARCATEC_
@_ARCATEC_ 10 ай бұрын
I have been writing on this subject, and have found it be computationally explosive. Excellent presentation, love your work 🤓👍
@rarrmonkey
@rarrmonkey 9 ай бұрын
If you redefine set theory so that sets do not include themselves (or derivatives there of) you avoid contradictions and "solve" the halting problem. A = X & A [ X 0 ] If the result of a question is not dependent on the result of the question everything is good. Or if you allow answers to be [Yes, No, Circular Reference] you might be able to answer all question in theory.
@CorwynGC
@CorwynGC 7 ай бұрын
Not necessarily. There are plenty of questions for which answering could take forever. Imagine trying to find a Fermat's last theorem solution before the proof that none exist. No way to know if the program will ever halt.
@JoeBowler300
@JoeBowler300 10 ай бұрын
I really enjoy your enthusiasm of learning and explaining in your videos. Keep on keeping on1 👍
@stromboli183
@stromboli183 7 ай бұрын
At 19:40 you say "even with unbounded computing power" but I feel you're skipping over something important there. The Turing Machine may be a very simplistic computer model, but with one property that is crucial for the halting problem: it's infinite. Our computers however are finite. And as long as computers are physical constructs that we build within the observable universe (which is finite), they will remain finite. For any program that is to be run on a computer with finite memory and storage space (i.e. any computer that exists in the physical world) a 'halt checker' program definitely exists: run the input program in a virtual machine and keep track of all the states you've already seen. Since there is a finite number of bits, the number of possible states is finite, so you're guaranteed to either come to a halt, or to encounter a state which you've already seen before, meaning the program is stuck in an infinite loop and will never halt. Note that the memory requirement and computation duration for this halt checker may be quite large, but still definitely finite. Unless I'm missing something here, the halting problem only applies to hypothetical computers with infinite memory (like the imaginary Turing Machine), not real computers.
@privacyvalued4134
@privacyvalued4134 8 ай бұрын
Google solved the halting problem with its app review system: By having humans answer various questions.
@peters616
@peters616 10 ай бұрын
Ironically, there's something about how Turing proved the halting problem is undecidable that implicates a kind of infinite loop itself. Because of the recursion involved, the halting problem analyzes the program that analyzes the halting program, I think it is axiomatic that an infinite loop will occur and the computing resources required to solve the problem will become infinite. Maybe a separate problem is whether it's possible to prove the halting problem is decidable for any program that does not call the halting program.
@Makebuildmodify
@Makebuildmodify 6 ай бұрын
“if a PhD student was trying to design an algorithm to do any of these tasks then supervisor can point out that their Endeavor is futile”, does this mean that the supervisor can only point out specific futile endeavors but not ANY endeavor?
@twodogzz9291
@twodogzz9291 10 ай бұрын
You are a great teacher! I have never fully understood Turing's explanation before watching yours.😁
@morryDad
@morryDad 10 ай бұрын
I was once asked by a VP at my company if we could write a program to automate root cause analysis. RCA is the root bug of a failing program. Basically, he was asking for one program to analyze another until us where it was broken. After controlling myself enough not to laugh at his face, I took it back to my desk and pondered it a bit. I didn’t realize that it was a halting problem, just wrapped in a different coloured bow. I sent him a nice little email, explaining the basics of the halting problem, and that seem to satiate his bizarre request.
@ArneChristianRosenfeldt
@ArneChristianRosenfeldt 10 ай бұрын
So how did you know that a program failed ( halted ) in the first place.
@MadScientist267
@MadScientist267 6 ай бұрын
This almost certainly has to be related to the idea that accurate detailed self diagnosis is impossible. A machine can't "see deep enough" within itself to give all of the specifics that cause an error, it can only give the result end some associated metrics. Actually translating that into a precise cause of failure is simply impossible. Hence the weird cryptic messages we all have come to scratch our heads over. *We* eventually learn what they mean and how to correct the issues (in theory anyway lol) but that is because we are *outside* the computer.
@MRNICK_OSINT
@MRNICK_OSINT 9 ай бұрын
Make a completely "animated" film of bits and bytes going through a computer to SHOW the interaction of software with hardware (no one has done it) and have this great lady (Jade MacKenzie) do the narration and sensible interrupts. From keyboard (and within it) through CPU, cache, RAM out the port into the gateway, etc.
@frankansari3457
@frankansari3457 10 ай бұрын
First time I heard about this problem was in a book called "The little schemer" where the goal was to write a function called will-stop in this Lisp dialect.
@HeavyMetalMouse
@HeavyMetalMouse 6 ай бұрын
I feel like the most important practical takeaway in this is that these problems can't be solved for 'the general case', as you mention in the ending. That is, we can't design a program that can take any program from all possible programs and always be able to 'decide' in this way. The practical solution to this that modern programmers use is to not try to do that. Instead, the task is often to design a program that can solve decidability on a restricted subset of programs... determining whether any given program from among all possible programs is actually in that subset, of course, trips flat on its face on the Halting Problem once again, amusingly; however, if the programs we are writing that we want the decider to check are all constructed within some known limitations and structures that force them a priori to be in that subset, then we don't need to think about the general case.
@TruthNerds
@TruthNerds 8 ай бұрын
And my 2 cents as a software developer: The halting problem is a theoretical curiosity. Important to theoretical computer science and mathematics, of course, but of little practical relevance. Why? Let's say I'm doing a code review. I would e.g. check whether some computation halts. We've established that I can't always tell, sure. The possible outcomes are: 1. I find that the computation obviously halts. Good. I'm satisfied with that outcome. 2. I do not find that it obviously halts and ask the original developer to explain why / prove that it halts. I receive a satisfactory answer. Also good. 3. I do not find that it obviously halts (for all allowed inputs) and the original developer can't really justify why it should. In that case, I'm not satisfied. But does it matter to me whether a) there is a hypothetical proof that the program halts or doesn't halt, but the original developer couldn't find it. Or b) there is no proof at all that the program halts or doesn't halt. Not really. I'd still only accept a program that can be demonstrated to halt.
@KohuGaly
@KohuGaly 8 ай бұрын
It's a theoretical curiosity for most software developer positions, but not all of them. It's very much a real practical problem in programming language design, compilers, optimizers, linters, static analysis tools, sandboxing environments and pretty much in any case where your program might potentially be executing arbitrary code as part of its proper function. To make your program demonstrably halt, you often need to "solve" the halting problem (or some problem equivalent to it) for the input code in some reasonable way. Note that the fact that halting problem doesn't have a solution is not the core of the problem. The core of the problem is that it also proves that any program that could be used to construct a halting decider cannot exist. For example it's impossible to tell whether two arbitrary programs are equivalent.
@TruthNerds
@TruthNerds 8 ай бұрын
​@@KohuGaly Thanks for the feedback… although I don''t quite agree. I like the examples that you've given where the halting problem potentially matters to a software developer. But I don't think the issue is really so much theoretical decidability but what I would call practical decidability. As an example: Let's try to prove that two chess engines are equivalent in the sense that, for all reachable positions, they suggest the same move. Let's assume that both chess engines have been proved to halt for every possible input. The nearly universal approach is to limit the recursion depth for predicting future outcomes. Chess engines also generally have to play by the clock, anyway. Theoretically, this is decidable because chess is a finite problem (unless you modify the game rules themselves, e.g. make the size of the board unlimited). -You can e.g. determine every possible checkmate or stalemate position and work back from there (finding all positions that could have been the position one half move prior). This is called retrograde analysis and is used to solve limited subsets of chess, e.g. to generate so-called endgame tablebases with a limited number of pieces on the board.- EDIT: Strike that example, this is about the equivalence of arbitrary chess engines. Anyway, you could feed every possible position into both chess engines and see whether they agree on the suggested move. Is it decidable in practice? In general, it's absolutely not decidable. While chess is a finite problem, the problem space is huge. (Interestingly, checkers has been completely solved, using computers, but chess is in a different class.) Long story short, yes, the halting problem does show that problems like the ones you mentioned are unsolvable. But the class of problems that isn't solvable in practice is far larger than the class of problems that isn't solvable in theory. As such, any practical program (e.g. a static analysis tool) must be prepared to gracefully handle such cases anyway. Presumably by setting some sort of resource limit for the analysis.
@KohuGaly
@KohuGaly 8 ай бұрын
​@@TruthNerds well, for a more down-to earth example: I'm an embedded software developer. Previous few days at work I've spend debugging a cyclic reset bug encountered by some of our testers. That's an example right there of the halting problem trickling down through hands of big-brained analysis-tool makers not being able to solve it, to the filter-feeder bottom-of-the-foodchain junior developer like me, who uses their tools to improve reliability and safety. Software development process would look significantly different if halting problem had a solution. It impacts all of us, but most of us just indirectly, through tooling we use to build, analyze and debug our software.
@michaelseitz8938
@michaelseitz8938 10 ай бұрын
@16:16 But ... the REVERSER never really halted ... the eyes were still running (forever) 😁
@upandatom
@upandatom 10 ай бұрын
haha I was so dizzy
@simonanderson5241
@simonanderson5241 9 ай бұрын
What a ride of emotions. I was constantly thing "Yeah, but!" - but then the explanation came.
@vantahku7211
@vantahku7211 10 ай бұрын
I used to take naps in a study lab called "Hilbert Space" at the University of Oregon. Naps between math classes were a must!
@rexduranzelandony
@rexduranzelandony 8 ай бұрын
The halting problem is one of telescopy. The only way to know whether an algorythm will halt is to run it. If you can predict every result then you wouldn't need an algorythm in the first place
@DirkHillbrecht
@DirkHillbrecht 10 ай бұрын
I am fascinated by these problems since my youth and I really find your explanation one of the best I have ever heard, especially Haltchecker and Reverser. And furthermore, you pronounce "Entscheidungsproblem" really beautiful. 😊 Regards from Germany!
@nkronert
@nkronert 10 ай бұрын
Except that the emphasis is on "scheidungs", not on "Ent".
@AlexandroRamosRodriguez
@AlexandroRamosRodriguez 10 ай бұрын
I loved the original drawings of the halting program, with "Halt".
How a Hobbyist Solved a 50-Year-Old Math Problem (Einstein Tile)
17:59
Why the number 0 was banned for 1500 years
16:27
Up and Atom
Рет қаралды 429 М.
CAN FOXY TRICK HIM?! 🤣 #shorts *FOXY AND NUGGET!*
00:17
LankyBox
Рет қаралды 8 МЛН
NO NO NO YES! (Fight SANTA CLAUS) #shorts
00:41
PANDA BOI
Рет қаралды 57 МЛН
The Time-Reversibility Paradox - Why Time Flows Both Ways
15:27
Up and Atom
Рет қаралды 692 М.
P vs. NP: The Biggest Puzzle in Computer Science
19:44
Quanta Magazine
Рет қаралды 635 М.
Something Strange Happens When You Follow Einstein's Math
37:03
Veritasium
Рет қаралды 5 МЛН
Turing Machines - How Computer Science Was Created By Accident
17:05
The Simplest Math Problem No One Can Solve - Collatz Conjecture
22:09
An Infinity Paradox - How Many Balls Are In The Vase?
14:13
Up and Atom
Рет қаралды 323 М.
Mathematicians Use Numbers Differently From The Rest of Us
33:06
Veritasium
Рет қаралды 6 МЛН
Why it took 379 pages to prove 1+1=2
16:43
Up and Atom
Рет қаралды 1,1 МЛН
How AI Discovered a Faster Matrix Multiplication Algorithm
13:00
Quanta Magazine
Рет қаралды 1,3 МЛН
We should use this amazing mechanism that's inside a grasshopper leg
19:19
Phone sees the future ! 📲🫣👽
0:38
BOGDANCHIKI
Рет қаралды 11 МЛН
Samsung mobile phone waterproof display. samsung mobile phone digital s23ultra  #shorts
0:15
Распаковка айфона под водой!💦(🎥: @saken_kagarov on IG)
0:20
Взрывная История
Рет қаралды 10 МЛН
Vortex Cannon vs Drone
20:44
Mark Rober
Рет қаралды 12 МЛН