"Because I allow running these rules in both directions, I actually need the opposite as well, which appears to spell moron... but we're not morons; we're doing logic, and this is smart." Please do more like this.
Having watched all your other videos 100 times each, I finally, FINALLY, watched this one that I have been avoiding for 5 years. And by God, I actually understood it, and even enjoyed it! What a fun little cellular-automaton-like system you ended up creating while mapping Turing machines to keming machines.
Hey, he hasn't uploaded in 5 months. Do you have maybe, dunno, a secret video link or so. I just need 5 minutes, man. Just 5 minutes.. Starting to itch here, man. ... c'mon, just 5 minutes!
Had to chuckle again at your comment at the end of the video that nobody would watch this. This was at least the 4th time I've watched this whole video in the last 5 years. Every so often, UA-cam randomly recommends this video to me and I think to myself, "yeah, this was fun and interesting, don't remember exactly how the proof went, let's watch it again" ^^
I am one more of those three people and also loved it. I'm confused about the part where you said you hadn't actually proved the kerning problem unsolvable. If you proved an entire class of problems unsolvable (the kerning contains the desired substring), doesn't that imply that any set of problems which are a subset of that class (the kerning contains the desired substring AND nothing else) are also unsolvable?
Thanks! If I'm understanding your question correctly: The difference is who gets to choose w3 (i.e., the leftover substring). If I'm given w1, w2, and w3 along with the rules, and simply need to decide whether w1 is kernable to w3, this would imply the exact problem (in fact it's equivalent to the exact problem; w2 is irrelevant). However, the thing I proved undecidable was: I'm given rules, w1 and w2, and I decide whether there exists some w3 such that w1 kerns to w3 and w2 is a substring. I can't just choose w3 to be the empty string always, for example, because then I might incorrectly say "no" when there is indeed some other substring that exists. So this problem doesn't seem to be equivalent or imply the other (or be implied by it), although there may be a simple proof of that I'm just missing.
couldnt you construct a set of rules to clear the trace but without replacing the left side cursor, so that the trace can only be cleared as a final move. this would not allow any relevant states of W as the encoding of Tn includes a cursor (the encoding would need to be changed so that only the right side of the cursor was encoded, or some similiar variant. This then proves for any finite set of 1s on the original tape (which im not sure is an assumption of turing machines)
This prevents the keming machine from wiping out the trace and then forming a cursor from which incorrect rules could then be applied, but it does not prevent the keming machine from wiping out the trace, unwiping a different trace, and then reaching an illegal tape by reverse-executing those actions.
Tom, this video was absolutely fantastic (commenting due to the note at the end). I'm a CS undergrad without experience related to proofs or logic, and although I wasn't able to wrap my head around some parts in realtime, I definitely feel like this video is an approachable (and most importantly, interesting) introduction to some great topics. I would love to see more videos of this type (and all other types) from you in the future. It seems like the best content occurs when you discover something that has obviously interested you and decide to share it with the UA-cam audience.
If you enjoy Tom's humor and Tom's subject matter, I'd suggest checking out the book by Neal Stephenson titled cryptonomicon, it actually has a lot to do with these subjects
It's a serious book but its very comical in a genius sort of way, I would think that Neal's work has been consumed by Tom and has influenced him a good bit but that's just speculating
I saw a video on the Halting Problem once and I never understood why it was significant. Thanks for making this concise, clear & accessible video. As someone with a casual interest in math/computer science, a whole lot of things “clicked” after watching this.
I happened to watch this video a few times: before, during, and after my undergrad in computer science, and it's really interesting to have developed from not knowing anything you were talking about, to sorta knowing some of the concepts, to easily following along the whole time. You're one of the most interesting people on this platform, so some other late night I'll probably come watch this again and dust off my reduction proof skills!
That’s cool! I think it’s one of the best things about learning technical topics: being able to appreciate neat thoughts (or “jokes” as I sometimes think of them) that would otherwise be inaccessible. Thanks for watching!
I would really appreciate more of this, it's exactly the kind of content I go to your channel for (brilliant insights born from genuine interest) while providing more tools and perspective to think about these ideas on your own. I find it unfortunate you consider it so unlikely that you will do this again.
Thank you for the encouragement! I do like doing it, but it's just a lot of work to present this way. Maybe I can experiment with something more efficient :)
Hey again - I'm also one of those 3 people who made it through! (judging by the comments, you greatly underestimated your viewers ;)) I must admit that I didn't fully understand everything... but I really like your way of explaining things. I wouldn't mind more videos like this.
This is brilliant! I know I'm late to this, but I love this kind of stuff. Even though you swore to keep it "boring", it's still easy to see your personality shine through and it honestly makes this video really enjoyable.
Funnily enough, after I had gone back and watched about 75% of your videos last year after Harder Drive then forgot to do the rest, UA-cam recommended me this video following-up on this year's. It didn't recommend me the shorter one, so thanks for saying it at the start, because that prompted me to go watch it first. I've done those things with words and letters for almost my whole life as a kind of autistic stim, one I could do without getting into trouble for moving at school. So I think it's really cool that you've taken this vague but fairly structured game and properly formalised it! I must admit I zoned out a bit in your explanations for the Oracle and Logics parts respectively, but that's only because I knew them already so I couldn't be a great judge of your teaching either way! You definitely seemed to describe them in a more streamlined and easier-to-grasp way than my teachers for uni-level maths, but I can't really judge if you took them all the way or not. Judging by other comments which say they had to go through college and then come back to fully appreciate the video, I would say they're a better judge of how well you introduced a beginner to it than I! ANYWAY, my brain just spat that out because of your little aside wondering how good of a job you did. So now onto the main thrust of my comment: this is actually super cool, I hadn't considered reformulating this little visual word game in those logic terms! Knowing one could theoretically program a computer to work them out, akin to sudoku or picross solvers, is pretty satisfying. Albeit a second-hand satisfaction, so I'm sure your own eureka moments were orders of magnitude more exciting! Thanks for putting this all together. The holistic, generalist, connecting-disparate-fields weirdo nerds like me really appreciate it.
Another name for the generalized anagraph problem is "the word problem for commutative monoids", and the generalized keming problem is "the word problem for monoids". A "monoid" is (roughly) just a bunch of possible strings plus substition rules, and a "commutative monoid" is the same with reorderable strings ("bags"). The "word problem" means deciding if two words / bags are the same. Great video :)
You just tricked a graphic designer into watching an introduction to linear logic and the halting problem. Righteous! I like your more accessible videos but this was fascinating too. It helped that you started with a more or less straightforward 'joke problem" because it gave context to the symbol manipulation- i dont think i could have digested it without pondering the vanillavideo first but i stuck with it.
Hi Tom, I never comment on videos, but just wanted to let you know I just found your channel and immensely enjoyed your videos, and this one in particular! Both funny(even if you claim otherwise!) and very interesting. If you are willing, I'm sure a lot of people would love more videos like this!
You took an unexpected (for me) direction in this proof. Although you can reduce to Turing machines, with the accompanying sticky bit about traces, it seems like it would be easier to reduce to the word problem for groups instead. In fact, there is almost no reduction to be done - a keming machine is almost exactly the problem of determining equality of words in a free group quotient by some congruence rules. More formally, suppose you could solve the (exact) kerning problem. Now given an alphabet Sigma = {a,b,...} and a finite set of pairs in the free group like aba^-1 = c, we can make additional letters a^-1 for each a in Sigma and add relations aa^-1 = empty, a^-1a = empty, to make this a word problem in the free monoid, and then if we interpret these equalities as rewrite rules of a keming machine, a given word is rewritable to the empty word iff the original word is equal to the identity element. There is a proof of this latter fact in the Wikipedia article, and it is worth a read since it is not (easily seen as) a diagonalization argument, like most undecidability proofs.
"There is a proof of this latter fact in the Wikipedia article" but which article are you referring to? Is it en.wikipedia.org/wiki/Word_problem_(mathematics)
@@ere4t4t4rrrrr4 I mean the word problem for groups: en.wikipedia.org/wiki/Word_problem_for_groups#Unsolvability_of_the_uniform_word_problem (no promises that this is the same proof I was referring to when I looked at wikipedia 3 years ago but it looks about right)
in order to prove that the word problem for groups is undecidable then you need to go through a process similar to this one to reduce to turing machines anyway
okay, that was pretty freaking neat. I haven't seen many other videos at this level of mathematic complexity on youtube that were also as entertaining as this one was. It's pretty awesome. Frick, if you do any other videos this mathematically complex, I'm totally up for it.
One of the "three" people here, I thoroughly enjoyed the video. I've always been interested in computability theory, but never dug very deep. Your video was exactly the perfect level of deep in a peace that I could follow. You really have a talent for teaching, whether it be impractical, or practical stuff :)
Clearly many others have already come up with solutions to the exact match problem, but I wasn't able to find this one mentioned so far, so here it goes: Instead of the oracle problem, the halting problem can be used. Take an arbitrary halting problem. Translate its instruction table into a kerning rule set, and its initial tape into an initial word as described in the video. Include an additional symbol H. Extending the existing translation rules, translate any instruction that causes a halt given current machine state x and tape reading Y into the rule: [Y]x H Include the additional rules: *H H H* H for every word symbol * Iff the initial word is kernable using the given rule set into the word "H", the turing machine halts. The **H, H** H rules can obviously be backtracked to produce whatever garbage one may desire, but crucially only when an H symbol is already present. H can only exist in the word when a halt has occurred, and as such these rules are only reachable when that condition is met. This is a crude way of erasing the rest of the word, but it should work just fine.
Can’t the oracle problem be used in the exact same way? The desired state τ could have a rule of its own, with the following rule: {τ} F (where τ represents the kerning word that corresponds to the desired Turing machine state) And also the same *F F rules (where * just has to be a character used in the trace) as in your halting variation. There’s no need for the mirror, since there’s nothing to the right of the } that became F. There’s a slight issue that there are infinite ways to represent a state as a word, since {τ} is the same as {0τ000}, but that can be easily fixed by changing the way the infinite tape problem is solved: instead of adding a third case for each rule in a word boundary, you can just add two rules: } 0} { {0 That lets our “window” into the tape expand and contract as needed (as long as it’s empty), without the cursor being there. Maybe there’s always a way to get to the final state without getting extra zeroes on either end, but I’m not sure and this simplifies the keming machine anyway, so I’m leaving it.
Made it all the way through! Very cool! Thanks for reminding me why I like computer science, it's easy to get bogged down in the linear algebra and despair
Here is a technique for extending the proof to the exact matching case. The main obstacle, basically, is that you can only perform reversible operations. Any irreversible operations allow invalid historical information to be made up when going backwards. The solution to this problem is to gate the irreversible operations so that they can only apply after you have reached the target state, because then we don't care if solutions are being invented. Once you've seen the target state, you can freely erase information. TracedExecution -> NoticeCorrectState -> EraseEverything -> SuccessHalt So. Take the Turing machine provided by the adversary, and rewrite it. It needs to check after every (unrewritten) step whether or not the tape is in the desired state (drop marker, go to start of tape, compare tape against goal using hardcoded state transitions, return to marker on failure). When it does find that the tape is in the desired state, the Turing machine should transition into "hide the bodies" mode, where it puts (and keeps) a success marker at the start of the tape, then erases everything else, then returns to the origin and goes into the halt state on top of the success marker. The key idea here is to only allow irreversible operations within accepting executions.
I think that still doesn’t work, though, because “hide the bodies” is the wiping Turing machine - which means for that stage to be reversible you now need a trace of how you removed the bodies, and everyone knows a paper trail gets you arrested. That’s really good terminology, though
Used this video twice as a sleep aid, third time I couldn't help myself and watched the whole thing, and I am grateful for that. Keep being yourself Tom
This was a great watch! I haven’t done much of this sort of proof since my CS degree, and it made me realise that I do miss it. Thank you for making this lesson!
This was one of the best videos I've seen in a while. Having been incredibly into programming language theory in college and loving typing judgements, and in general loving random tangents, this was a fascinating watch. Your explanations were clear, easy to follow, and the topic was fascinating to me. Awesome work :)
Ow please do these kind of things again! :-) It has been "only" 23 years ago since I had logic lectured to me in university, and I'll never mind the kind of refresher you provide.
36:22 Add another set of rules that are activated after reaching the halting state h: *h -> h h* -> h So, the question would be: can you make { word representing the starting tape } into h ? So, basically, it's like, after finding out that the machine halts, it halts and catches fire and burns up the whole thing, leaving only h. It's possible to reverse the burn to get some other trace of the turing machine, traces of computation paths it never took. However this isn't a problem, since to do that it has to reach halting state first. In order to reach h by some "unintended" way, it first has to do it in the intended way.
I would totally watch more of this. Computational proof stuff in particular is my jam, but anything in the general vicinity of "math and computer science" would be just as excellent, especially if it's something you're interested in/excited about. You do a good job of explaining things, and also have a wonderful voice, which means that your lectures would be both informative and enjoyable to watch :P
Thanks on all counts! Already the pain of a full day of recording and editing is but a distant memory, so I'll probably find another topic to give this kind of treatment to in the future. :)
Brilliant video and I was pleasantly surprised to see a number of things pop up I've recently learned about in my hobbyist playing with formal logic. I was also pleased I spotted the infinite Turing tape and rule direction issues before "checking the answers". Also thanks for the laughs!
Wow this is really exciting I actually love arcane ways to create turing complete systems - turing tarpits, like languages with a single operation [MOV, SUBLEQ - these are fun to work through and create common primitives like function calls, arithmetic, etc. Bitwise operations are surpsingly tricky]. And I like reducing things to NP complete (or NP-hard) problems like TSP & SAT. Recently, I've seen a really awesome proof showing that generalized Mario and Pokemon is NP complete Notes and mistakes: 9:14 - you changed the state incorrectly, but you pointed that out 11:50 - let me have a go at the proof Assume we have a procedure O(T, Tx) that solves the oracle problem for a turing machine T and eventual state Tx Consider a turing machine T: - if O(T, T2) is true, halt in state T1, otherwise halt in state T2 If O(T, T2) is true, T will never reach state T2, but if O(T, T2) is false, T will halt in state T2, therefore O cannot exist. QED 17:30 - A turing machine can only go one way in time, but the keming machine can "reverse" a state. On your example, a turing machine can only go 10[0]a10111 => 101[1]a0111, but your keming machine can go in reverse In fact, there is another problem, the * that you placed there Let's expand the keming machine rules to include that * Consider a TM with one state a, that always writes 1 and goes right. The keming machine rules are: [0]a1 1[1]a, [0]a0 1[0]a, [1]a1 1[1]a, [1]a0 1[0]a These rules are in fact legal according to your KM definition, but we can already see a few problems The machine can write an arbitrary binary string to the right of the starting point (actually the beginning of the string of ones) by backtracking, so O("[0]a0", "[1]a0") is false, but it's trivially true for your KM 20:11 - The infinite tape issue is trivially solvable, add < and > markers for the end of the tape, and add rules 21:07 - This is a problem, if the tape can only be extended/shrunk when our marker is near it, equivalent TMs may not be reachable. Say that the only rule I have is [0]a1 0[1]a The state {00[0]a100} is not reachable from {0[0]a10}, even though they are equivalent (doesn't work for arbitrary match ranges, and rule count grows exponentially with match range) On another hand, we can remove this issue if we just do linear time preprocessing, so I guess it doesn't matter 34:55 - Now we have an issue, if we come back to the oracle problem, we need to be able to convert the final TM state to our final word. In order to do that, we must know the order of execution of the turing machine! We need a way to eat our execution trace, but that's impossible without destroying information, which means the reverse rule can create bogus information. We need another set of rules, and encode the "current state is the same as the final state" into our rules to destroy all information in our word. So, our initial word is the output of some function on the T1 and Tx, and our final word is some destroying character that eats the entire word, say #. Creating bogus information here doesn't matter, since we already found the state Tx reachable from T1 We can do something terribly inefficient, but that doesn't matter cause it's a decidability proof. Assume we execute these rules while the tape looks something like áååć{101010[1]a010}010a]1[010101^ When the > returns to our pointer, we can either continue execution, or send a signal to the right side. We can write a rule that duplicates the string at the end, safely storing one copy behind the caret, then turns the } into a !. When we see 0!0, 1!1, a!a, ]!«, etc. we erase the characters on the sides. If ! reaches {, it becomes a # and eats everything, reaching the final word which is just #. Unless I missed something, this should work - we can't continue execution until the }! and ^ return to their place and all data matches (the copy safely stored behind the caret must match before we send the signal back to continue execution) 36:33 - oh, I was overthinking it, but I guess the above is a "proof" if it happens to work 42:50 - The \Rightarrow symbol is confusing to me, cause I was taught it means "implies", we don't use the ightarrow symbol in Poland [when it comes to logic - we use it for functions] 44:01 - OOOH, sweet! This looks basically exactly the same as linear type systems, each object must be used exactly once, which is useful for things like lock guards, channels, tokens that can only be used once, tokens that imply ownership of a resource, etc. 47:35 - Yeah... You can't use these rules as assumptions, as that means you can only use them once, and must use them once, which fails even in this example. You must keep these rules as separate axioms/sequents - ...Okay. ! works, feels like a hack
Right, to clarify a few things - In the oracle proof I said that O cannot exist - that's not true - O cannot be implemented on a TM, not sure how hypercomputation plays into this, or if it does at all. - In the decidability "proof", I made a few typos, ! can eat characters if the ones on its side are the same, so [![ !, and I omitted some information. We must not allow execution while ! is free, so the [] will be changed to something else or reordered. Reordering is enough, as even if ! writes it's own functional execution pointer, the shuttle will block it from being useful. [EDIT: Actually that's false, ! can write one on the left, but I'm not sure if that's useful either] I also intentionally omitted the signaling method and duplication procedure - creating it is error prone, but it's definitely possible as it can be implemented easily with other computing methods, to which a TM (which our KM is) is equivalent. I also omitted a note as to why it's okay to only reverse the Tx comparison string without additional encoding, but I felt it was obvious
@@animowany111 Since you like obscure Turing machines, you may be interested to know that Magic: the Gathering is proven to be Turing complete by constructing a Turing machine with the rules of the game.
Hi Tom I'm one of the 3 people who got through it and I thought it was well explained and insightful. I think I get why regex search and replace is turing complete now! You could use similar method as you explained at 22:21, you wouldn't even need the trace because search and replace is unidirectional.
Definietly liked it, one of the most clear and concise mathematical explanations I've seen on youtube. The reduction proof is elegant, especially the part with encoding a trace. The linear logic proof was also nice, simple in a way but never a connection I would've thought of myself.
This is absolutely amazing. I understand that it's a lot of work to put together but, if inspiration strikes, I would gladly drop everything to watch another through. Really fascinating stuff: it's inspired me to take a deep dive. Thanks, and keep it up!
I absolutely loved this by the way. I thought that it was going to be boring at the beginning but it ended up interesting to think through why some of the things you were saying had to work. Thanks Tom!
This was actually super informative and interesting! I ddin't understand the part on linear logic too well, but that was the most coherent explanation of a turing machine I've ever heard, and your explanation of everything related to the kerning problem was crystal clear!
This video is awesome. Honestly, I'd love to see one about the lambda or combinator calculus in this style, or your usual style, if you ever felt like making one.
came for the goofy engineering projects, stayed for the pure maths (CS and pure maths are cousins and good friends, anyway). Thanks, Dr. Tom Vii! I think I've binged nearly your entire channel at this point, it's absolutely fantastic, PLEASE keep up the good work! (since youtube is so unreliable nowadays, i bookmarked your webpage like its 2008 or something.... bizarre to think of the internet as still full of addresses and websites instead of Five Platforms All Sharing Content From The Other Four)
I am a recent fan of your channel and a student learning computer science in high school and your channel is one of the most entertaining and interesting channels i have seen on youtube. This video was very informative and entertaining, more videos like this should be published to this site.
Hey there! I'm the other one of the 3 people who watched through. It's really cool seeing these kinds of proofs on UA-cam, so even if you don't make any more, I appreciated and enjoyed watching this video!
I love this video! Not sure whether anyone’s mentioned this, but this is equivalent to the Word Problem in group theory. If you let the rules for kerning strings be the relations in the presentation of a group, then the strings become elements of the group, and the question of whether one string can be transformed into another by repeated application of the rules becomes the question of whether two elements are equal.
Hey there! Mathematics master student here, working on logic (studying "propositions as types" correspondence righ now). I didn't expect to bump into linear logic while watching this but it was a nice surprise. I loved the shuttle idea for TM encoding. As others have pointed out you can remove the states trace prefix, when in the final configuration, adding some rewriting rules that involve the final configuration. But if the Touring machine has a final state (or many accepting states) you could also change it in a special eraser shuttle that slides left until it reaches the trace then it deletes the state symbols; this way there is no need to name the desired final state in the rewriting roules. Something like this, where f is the final state and « is the eraser shuttle: [0]f «0 [1]f «1 0« «0 1« «1 *{« {«
This is a fantastic video. I'm a CS&Philosophy undergrad at Oxford, and found this video awesome (in particular, I now get linear logic, which I tried unsuccessfully to grok via the wikipedia page before). I might spread this as entertaining revision for our models of computation course. Thanks for taking the time to make this, and I'd totally watch more Tom Academy!
I just wanted you to know I love your stuff. Please keep doing this. I'm in engineering, but I do these kinds of "Recreational maths" kind of stuff all the time, and I love seeing other people do the same. ^-^
This was a really good explaination. I would never have guessed that kerning is so closely related to the halting problem but logic manages to surprise me all the time. Should you ever feel the urge to make something like this again, please do!
I'm a huge fan of the mathematical side of computation and vice versa, and I've been learning category theory on my own and that has exposed me to so many different branches of mathematics, including the different flavors of logic. I really enjoyed the concrete example of linear logic!
I'd love a video in this format on the P vs NP problem, in particular reducing problems to ones whose complexity we know like 3-sat etc. I never quite understood why finding a hamiltonian path can be reduced in this way, or perhaps I'm totally misunderstanding the whole thing. Augh!! For reference I study pure maths and just finished my second year, and I found this crystal clear and very interesting, and I now may consider computer science as an option. Great video :)
i work at the math tutoring center at my university and a cs student came and asked me "do you know languages and words in computer science?" and I had no idea what he was talking about... I was able to read his lecture notes and figure it out and interpret it for him, turns out it was the stuff you explained in the beginning! would have been much quicker tutoring session if i had seen this video sooner lol
I loved this! I've been studying IT at university for 1 year now, where I took an optional logic course that introduced me to some variation of a few of the concepts and techniques used in this video. Anyway, I thoroughly enjoyed that course and it left me desperately wanting more. I was also very curious to know exactly how such tools could be used in more "practical" situations (as opposed to simple practice exercises such as proving DeMorgan's law with sequents), and your video has provided that. Thank you!
Fascinating update: MELL decidability is once again an open problem, due to the fundamental issues with proof-based math discussed by Tom in this very video. Link: hal.inria.fr/hal-01870148/document
Thank you! This has taught me so much! I heard about Turing machines, lambda calculus and linear logic in context of type theory of programming languages, but this is the first time I see them applied in math. This is very beautiful stuff :)
The first time I tried to watch this I didn’t really understand but a while later I came back and it was really entertaining this time and I think I understood most of the things Thank you Tom
As an undergrad cs student taking a computational theory class this video was a delight. This ties together the 2 main focuses of the course (sequent calculus and languages/Turing machines) in a fun way. Make Than Academy real please
I’ve watched this video a few times and every time I do I always force myself to think about how to “fix” the keming problem so that you can ask the question of if you can translate w1 to w2 and not some wacky w3, but this time I was making pasta and the solution finally came to me The idea is that once you have some w3 which contains w2, it doesn’t really matter what you do with your keming machine, so long as your rules don’t create w2s where they never were That said, you can add some clearing rules to the machine that look like this: *w2 w2 w2* w2 This does some funky things to the machine - once you’ve achieved a state with w2 in it, for instance, you can use this rules to get any string that contains w2 from it. That doesn’t matter though, because the answer to “can you get w2” is always yes *only if you can naturally get w2*, and no only if you can never reach w2 This shows that the keming problem proper is also undecidable, and also shows that I am far more deserving of a PhD than Tom 7 is. I will be sending my results to your institution and we’ll see how it goes In all seriousness Tom, this video in particular kinda set my brain on fire when I was a high school student and didn’t really know any of this theory of CS nonsense, now I’ve graduated undergrad as a CS/math major with a very special interest in this stuff, and a lot of my initial inspiration started with this, I’m really happy in my own knowledge and never want to stop learning about this, and I hope that serves me well in grad school :)
Oh also, I understand why this apparently simple fix didn’t come to you (assuming it’s even right, I’m still making the pasta); there’s a parsing tree hiding underneath this, whereas a Turing machine is a deterministic machine, and there are no branches in the path in the states allowed to produce, and you’d want your simulation of a Turing machine to also be deterministic - these rules I added are exactly the type that forced you to change it originally, but it’s fine because it’s only nondeterministic when there’s a w2 to be found, and there’s a path along that massive series of branching that ends at w2
That's such a neat proof... I'd watch you teaching serious stuff more often! Not a lot of views, but you've blown my mind at that's got to be worth something.
36:20 Unsure if anyone has pointed this out, but there's a relatively straightforward way to generalize your solution to get the exact Kerning problem; you just have to include the specific T_F as part of the kerning rules, which lets you delete the trace once the keming machine has reached a state corresponding to T_F. Deleting the trace means that we sort of break the symmetry you carefully built, so the KM states are no longer one-to-one with the TM states. Critically though, these extra states can only be accessed after the KM has already reached a state corresponding to T_F, so we are still in the situation where "the TM can reach the state T_F if and only if the KM can reach the word W_F". As for the formal implementation, you would add some rules to the KM that let you lengthen and shorten the tape arbitrarily, so "{0" equals "{", and likewise "0}" equals "}". After that, you would define the word W_F to be encoded like "{T_F}", and given the previous rules it doesn't really matter where exactly we cut off the infinite zeros of the T_F state. You also need a way to delete the machine head from the KM word, so add a schema of rules to the KM which runs over all the words which are identical to W_F except for the presence of a machine head, and sends you to the word W_F. Finally, you would add a schema of rules which basically says "*W_F" equals "W_F" where the symbol * varies over all the (finitely many) symbols which can appear in the trace. So, in the case that the TM never reaches the T_F state, and the KM is currently in a state reachable by the TM (with a trace corresponding to a valid history of the TM), then necessarily that state doesn't correspond to T_F. It follows that the KM cannot delete the machine head, and it cannot erroneously delete the trace, so the only words it can access are corresponding to other states reachable by the TM. It then follows by induction that, after any finite number of steps, the KM word will always correspond to a state reachable by the TM. Conversely if the TM does reach the T_F state, it's trivial to prove that the KM can reach the W_F word by just following the corresponding rules. It follows that the KM can reach the W_F word if and only if the TM reaches the T_F state. So, suppose (!) you have a general procedure such that, given any KM and any words W_1, W_F, your procedure can decide whether the KM can turn the word W_1 into the word W_F. Then, given any turing machine and tape states T_1, T_F, we can construct a corresponding KM and words W_1 and W_F such that the KM converts W_1 into W_F if and only if the turning machine reaches state T_F when initialized on the input tape T_1. We can generate that KM problem procedurally, and then apply the KM solving procedure to solve the corresponding oracle problem (contradiction!), QED Kerning is undecidable.
Hey dude! That was awesome! I wish teachers at my University explained things at you did. Already knew all the theory but the fact of seeing it applied was amazing.
This was amazing. :) Topics that are certainly over my head academically, but you explained them in a way that I was able to grasp the necessary bits for your proofs to work. I'd personally love to see more like this.
Very cool, thanks! Although natural, I wasn't expecting MELL to show up. Linear logic's greatly interesting. A funny thing about it: exponentials aren't determined up to equivalence by their introduction and elimination rules, so you can have multiple exponentials pairs (! , ?) and iirc if you have enough of them it makes MELL (MEEEEELL?) undecidable. Don't quote me on that tho
Idea for exact matching: Target word is w_2. Add a rule for every alphabet element * like this: w_2* w_2 *w_2 w_2 Essentially, as soon as you have w_2, delete everything around it. If the Keming machine you presented can find a way to transform w_1 into sth with w_2 as a substring, the altered KM with these two sets of rules can obviously transform w_1 into w_2 by doing the same transformations as the KM and then applying these deletion rules over and over. Also the deletion rules (in particular the reverse case) does not add any new possibilities to go from w_1 to w_2 where we shouldn't be able to. Intuitively, the reverse way could only be applied when w_2 is already there in our transformed word. However, if w_2 is already in the transformed word then this means the KM without deletion rules would answer yes, so in all cases where we are able to apply any direction of the deletion rules we know that both the KM with and without deletion rules will answer "yes". We can write all kinds of gibberish into the word of course once we created w_2, but that doesn't matter at that point anymore. More formally you can probably do a proof by structural induction, but I think the idea is better grasped by an intuitive explanation.
I enjoyed the video. Regarding 36:23: "I couldn't think of any way to work around this problem": that is because it is impossible. Note that when I use 'tape', that includes the pointer and Turning machine internal state. Important for this proof: a start tape and an end tape can have different representations. We use start(A) to represent the representation of a start tape A, and end(B) to represent the representation of an end tape B. This proof works for any representation of the start and end tapes, so no kerning rules exist which can solve this problem where the full word is w_f, not just where w_f is a substring of the word. Proof sketch: Q-S->T means that word Q can be transformed to word T via the sequence of kerning rules S. 0 is the tape with a single 0, and 1 is the tape with a single 1. We use the eraser Turing machine mentioned in the video. We use proof by contradiction, so we assume that each Turing machine has a kerning ruleset which accepts all pairs of start and end tape for which the Turing machine can reach the end tape from the start tape. We now prove that this ruleset must have rules that would permit a sequence REVERSE which leads the kerning ruleset to accept start(0)-REVERSE->end(1). 1. There must be a sequence of kerning rules ERASE that would have it accept start(1)-ERASE->end(0), because the eraser can actually do that. 2. Similarly, there must be a sequence of rules ID that accepts start(A)-ID->end(A), again because the eraser can do that (it can reach the tape A from tape A by doing nothing). 3. Because all kerning rules are bidirectional, we can apply the rules in any sequence S that accepts Q->T in the opposite order to get a sequence of rules called !S that accepts T->Q. In particular, given a rule S which accepts start(A)-S->end(B), we can use !S to accepts end(B)-!S->start(A). 4. The sequence REVERSE=[ID, !ERASE, ID]. This transforms the sequence as follows: start(0)-ID->end(0)-!ERASE->start(1)-ID->end(1) This proves that any kerning ruleset would have a sequence of rules which can be applied to make it accept that the reverser would reach tape 1 from tape 0. This is false, so the assumption that such a kerning ruleset exists must be false. QED.
I know you've probably already decided what kind of creative endeavors you'll be persuing since this video was released, but I for one was really interested to hear you explain interesting concepts through this silly problem and would love to see more stuff like it!
OMG this is perfect. Thanks, now I actually understand what linear (and ordered) logics are about. I heard about it from Robert Harper's lectures on Homotopy Type Theory but never got to see it working until now.
This is a great video! I have a thought though, I think there's a shorter path to show the kerning problem is undecidable. The question of whether an unrestricted grammar can generate a particular string is already known to be undecidable, so it would suffice to show that a keming machine is equivalent to a UG. So to turn a set of rules, w1 and w2 into a UG I do the following: 1) define a rule from the start symbol to w1 : S -> w1. e.g. "S -> cool". 2) the keming rules just become production rules as-is. 3) define an ending rule: w2 -> epsilon (just some special terminal symbol that's not in w1 or w2). 4) show that this grammar is a UG (Chomsky type 0) by showing it is more general than a context-sensitive grammar(type 1): this part is easy, a CSG cannot have any rules that produce a shorter output than input, so no "r n -> m" which is obv allowed by a keming machine. So a KM is a UG, QED. (Quote Ehren Dabout decidability)
Clever idea, but this is a reduction in the wrong direction - if you show that KMs are UGs, then decidability of UGs implies decidability of KMs, not the other way around. You would have to find some way to (computably) transform an arbitrary grammar into a Keming Machine. I do recognize that you have a step where you show that the grammars you end up with are not inside some known class of decidable grammars, but there are many possible grammars that generate the same language. Yes, the grammar you end up with via this reduction is not context-sensitive, but that does not mean there does not exist a context-sensitive grammar that generates the same language.
Wait: I got it!! To show the kerning problem undecidable, you just need to translate what you would use as your final state to another rule (and add another symbol: E). You would say final state becomes E, and (any trace)E becomes E. Then, ask if you will ever end up with plain E. Even tho you might be able to reach any state be un deleting trace, it won’t matter because you would have to reach the final state first. Thus, the kerning problem is undecidable.
I often watch your videos more than once cause they are information rich (this is probably gonna be one of them). The paper video was super juicy too! Keep'em coming!
Really enjoyed the video! As someone who has only had one course in formal computation theory, this really makes me want to study it further! Thanks for the quality content!
36:00 Couldn't you make an symbol END which matches T_f and also itself plus any history symbol to the left? Then once the tape reaches T_f, END is substituted and it can start eating the history to the left of it. w_f is just END. Reversibility wouldn't be a problem, since END would only be possible iff the desired tape state was reachable in the first place.
Dude look a tree I’m very sleep deprived and idk if this works but can’t you take the END and create any trace with it? Any bidirectional rule where many inputs lead to the same output causes the same problem, I think
That only matters if the thing you're looking for (i.e. T_f) is all 1s. So you're saying that if you can get to all 1s with a trace then you can get to all 1s. Which... doesn't actually matter.
@@powerjbn9283 user "Dude look a tree " already said reversibility wouldn't be a problem. after END writes whatever it wants, it can't just destroy itself without a trace. Even if you have 2 ENDs, there'd still be 1 END left after one destroys the other. END could be used to create stuff, but by the time you create END, you've already managed to halt, and just need to delete stuff until destination word of lone END is reached. It's like a catch 22
Awesome video, I'm going to share this with the professor I had for a Computational Models class. The anagraphing part of it though leaves me wanting more. I'm familiar with showing using reduction to show that some problems are impossible to make a program for, like showing that two turing machines having the same language implies you can solve the halting problem. For the Linear Logic part of the video though, I need to see why provability in linear logic is decidable before I'm fully satisfied.
i feel like i would have enjoyed the mathematics far more during my comp sci degree if I'd had a lecturer as interesting as yourself, I'd love to see more
I believe that generalized kerning should be possible in the form of x -> y, but not x -> blahyblah. All it really depends on is if you allow for a rule that transforms into an empty string, or not. If you allow for it then you've made it into unrestricted grammar, which is undecidable because it is a TM. If you don't allow for it, which I think makes more sense when you think of real life kerning, then you are restricted to context sensitive grammar which does let you generalize the kerning problem. Also, no I am not 5 years late, I just thought I should get a CS degree first to make sure before I commented.
This is so much easier to understand than the wikipedia article for linear logic. The article just throws a bunch of symbols at you and asks you to invent your own intuitions. The video throws them at you one at a time, and explains some possible intuitions. I should study more maths.
"No jokes. This is serious and boring." "...So I like to think of Skeletor throwing words at us."
hey skeletor is a pretty serious guy
I was basically _expecting_ jokes after hearing him say this.
He's just a funny guy, he can't help it
"Because I allow running these rules in both directions, I actually need the opposite as well, which appears to spell moron... but we're not morons; we're doing logic, and this is smart."
Please do more like this.
*"this is not a joke"*
timestamp: 46:55
31:30 "And I just applied that rule... that I wisely deleted from the screen" God I wish all instructors could be more like Tom
Very nice explanation. The 'Shuttle' thing is super cute
Having watched all your other videos 100 times each, I finally, FINALLY, watched this one that I have been avoiding for 5 years. And by God, I actually understood it, and even enjoyed it! What a fun little cellular-automaton-like system you ended up creating while mapping Turing machines to keming machines.
Hey, he hasn't uploaded in 5 months. Do you have maybe, dunno, a secret video link or so. I just need 5 minutes, man. Just 5 minutes.. Starting to itch here, man. ... c'mon, just 5 minutes!
Had to chuckle again at your comment at the end of the video that nobody would watch this. This was at least the 4th time I've watched this whole video in the last 5 years. Every so often, UA-cam randomly recommends this video to me and I think to myself, "yeah, this was fun and interesting, don't remember exactly how the proof went, let's watch it again" ^^
Whoa, maybe you are all three people!
You're the Bob Ross of mathematical proofs.
Hey I'm one of the 3 people! I loved it! Also please do more Tom Academy!
Oh, thanks! And congrats! (:
I am one more of those three people and also loved it.
I'm confused about the part where you said you hadn't actually proved the kerning problem unsolvable. If you proved an entire class of problems unsolvable (the kerning contains the desired substring), doesn't that imply that any set of problems which are a subset of that class (the kerning contains the desired substring AND nothing else) are also unsolvable?
Thanks! If I'm understanding your question correctly: The difference is who gets to choose w3 (i.e., the leftover substring). If I'm given w1, w2, and w3 along with the rules, and simply need to decide whether w1 is kernable to w3, this would imply the exact problem (in fact it's equivalent to the exact problem; w2 is irrelevant). However, the thing I proved undecidable was: I'm given rules, w1 and w2, and I decide whether there exists some w3 such that w1 kerns to w3 and w2 is a substring. I can't just choose w3 to be the empty string always, for example, because then I might incorrectly say "no" when there is indeed some other substring that exists. So this problem doesn't seem to be equivalent or imply the other (or be implied by it), although there may be a simple proof of that I'm just missing.
couldnt you construct a set of rules to clear the trace but without replacing the left side cursor, so that the trace can only be cleared as a final move. this would not allow any relevant states of W as the encoding of Tn includes a cursor (the encoding would need to be changed so that only the right side of the cursor was encoded, or some similiar variant. This then proves for any finite set of 1s on the original tape (which im not sure is an assumption of turing machines)
This prevents the keming machine from wiping out the trace and then forming a cursor from which incorrect rules could then be applied, but it does not prevent the keming machine from wiping out the trace, unwiping a different trace, and then reaching an illegal tape by reverse-executing those actions.
Seriously missed opportunity to call them "ligaturing machines"!
Kerning machines also works though
Kerning machines is better, because kerning already sounds like a verb.
but he must strictly follow the "no jokes" rule.
@@Jivvi kerning literally is a verb
@@kornsuwin And Turing, as in Turing machine, is _not_ a verb...
Tom, this video was absolutely fantastic (commenting due to the note at the end). I'm a CS undergrad without experience related to proofs or logic, and although I wasn't able to wrap my head around some parts in realtime, I definitely feel like this video is an approachable (and most importantly, interesting) introduction to some great topics.
I would love to see more videos of this type (and all other types) from you in the future. It seems like the best content occurs when you discover something that has obviously interested you and decide to share it with the UA-cam audience.
Thanks, I'm glad you liked it :)
If you enjoy Tom's humor and Tom's subject matter, I'd suggest checking out the book by Neal Stephenson titled cryptonomicon, it actually has a lot to do with these subjects
It's a serious book but its very comical in a genius sort of way, I would think that Neal's work has been consumed by Tom and has influenced him a good bit but that's just speculating
I saw a video on the Halting Problem once and I never understood why it was significant. Thanks for making this concise, clear & accessible video.
As someone with a casual interest in math/computer science, a whole lot of things “clicked” after watching this.
I happened to watch this video a few times: before, during, and after my undergrad in computer science, and it's really interesting to have developed from not knowing anything you were talking about, to sorta knowing some of the concepts, to easily following along the whole time. You're one of the most interesting people on this platform, so some other late night I'll probably come watch this again and dust off my reduction proof skills!
That’s cool! I think it’s one of the best things about learning technical topics: being able to appreciate neat thoughts (or “jokes” as I sometimes think of them) that would otherwise be inaccessible. Thanks for watching!
I would really appreciate more of this, it's exactly the kind of content I go to your channel for (brilliant insights born from genuine interest) while providing more tools and perspective to think about these ideas on your own. I find it unfortunate you consider it so unlikely that you will do this again.
Thank you for the encouragement! I do like doing it, but it's just a lot of work to present this way. Maybe I can experiment with something more efficient :)
Hey again - I'm also one of those 3 people who made it through! (judging by the comments, you greatly underestimated your viewers ;)) I must admit that I didn't fully understand everything... but I really like your way of explaining things. I wouldn't mind more videos like this.
actually audibly gasped when i realized how you were turning ligatures into turing machines
I am going into academia and skeletor is now my default teaching device.
Epsilon-delta argument? It's just proving you can always beat skeletor. Ez.
This is brilliant! I know I'm late to this, but I love this kind of stuff. Even though you swore to keep it "boring", it's still easy to see your personality shine through and it honestly makes this video really enjoyable.
Funnily enough, after I had gone back and watched about 75% of your videos last year after Harder Drive then forgot to do the rest, UA-cam recommended me this video following-up on this year's. It didn't recommend me the shorter one, so thanks for saying it at the start, because that prompted me to go watch it first.
I've done those things with words and letters for almost my whole life as a kind of autistic stim, one I could do without getting into trouble for moving at school. So I think it's really cool that you've taken this vague but fairly structured game and properly formalised it!
I must admit I zoned out a bit in your explanations for the Oracle and Logics parts respectively, but that's only because I knew them already so I couldn't be a great judge of your teaching either way! You definitely seemed to describe them in a more streamlined and easier-to-grasp way than my teachers for uni-level maths, but I can't really judge if you took them all the way or not. Judging by other comments which say they had to go through college and then come back to fully appreciate the video, I would say they're a better judge of how well you introduced a beginner to it than I!
ANYWAY, my brain just spat that out because of your little aside wondering how good of a job you did. So now onto the main thrust of my comment: this is actually super cool, I hadn't considered reformulating this little visual word game in those logic terms! Knowing one could theoretically program a computer to work them out, akin to sudoku or picross solvers, is pretty satisfying. Albeit a second-hand satisfaction, so I'm sure your own eureka moments were orders of magnitude more exciting!
Thanks for putting this all together. The holistic, generalist, connecting-disparate-fields weirdo nerds like me really appreciate it.
I am joining you in calling myself a holistic generalist connecting-disparate-fields weirdo nerd. tom7 is amazing for us.
Another name for the generalized anagraph problem is "the word problem for commutative monoids", and the generalized keming problem is "the word problem for monoids". A "monoid" is (roughly) just a bunch of possible strings plus substition rules, and a "commutative monoid" is the same with reorderable strings ("bags"). The "word problem" means deciding if two words / bags are the same. Great video :)
You just tricked a graphic designer into watching an introduction to linear logic and the halting problem. Righteous! I like your more accessible videos but this was fascinating too. It helped that you started with a more or less straightforward 'joke problem" because it gave context to the symbol manipulation- i dont think i could have digested it without pondering the vanillavideo first but i stuck with it.
Looks like my work here is done! (:
Hi Tom, I never comment on videos, but just wanted to let you know I just found your channel and immensely enjoyed your videos, and this one in particular! Both funny(even if you claim otherwise!) and very interesting.
If you are willing, I'm sure a lot of people would love more videos like this!
You took an unexpected (for me) direction in this proof. Although you can reduce to Turing machines, with the accompanying sticky bit about traces, it seems like it would be easier to reduce to the word problem for groups instead. In fact, there is almost no reduction to be done - a keming machine is almost exactly the problem of determining equality of words in a free group quotient by some congruence rules.
More formally, suppose you could solve the (exact) kerning problem. Now given an alphabet Sigma = {a,b,...} and a finite set of pairs in the free group like aba^-1 = c, we can make additional letters a^-1 for each a in Sigma and add relations aa^-1 = empty, a^-1a = empty, to make this a word problem in the free monoid, and then if we interpret these equalities as rewrite rules of a keming machine, a given word is rewritable to the empty word iff the original word is equal to the identity element.
There is a proof of this latter fact in the Wikipedia article, and it is worth a read since it is not (easily seen as) a diagonalization argument, like most undecidability proofs.
Yeah, I was thinking isn't this just a semi-thue system
Yeah but my Computer Science program only goes as far as turing machines so I'm glad he helped me study for my exam lol
"There is a proof of this latter fact in the Wikipedia article" but which article are you referring to? Is it en.wikipedia.org/wiki/Word_problem_(mathematics)
@@ere4t4t4rrrrr4 I mean the word problem for groups: en.wikipedia.org/wiki/Word_problem_for_groups#Unsolvability_of_the_uniform_word_problem (no promises that this is the same proof I was referring to when I looked at wikipedia 3 years ago but it looks about right)
in order to prove that the word problem for groups is undecidable then you need to go through a process similar to this one to reduce to turing machines anyway
okay, that was pretty freaking neat. I haven't seen many other videos at this level of mathematic complexity on youtube that were also as entertaining as this one was. It's pretty awesome.
Frick, if you do any other videos this mathematically complex, I'm totally up for it.
One of the "three" people here, I thoroughly enjoyed the video. I've always been interested in computability theory, but never dug very deep. Your video was exactly the perfect level of deep in a peace that I could follow. You really have a talent for teaching, whether it be impractical, or practical stuff :)
Clearly many others have already come up with solutions to the exact match problem, but I wasn't able to find this one mentioned so far, so here it goes:
Instead of the oracle problem, the halting problem can be used. Take an arbitrary halting problem. Translate its instruction table into a kerning rule set, and its initial tape into an initial word as described in the video. Include an additional symbol H. Extending the existing translation rules, translate any instruction that causes a halt given current machine state x and tape reading Y into the rule:
[Y]x H
Include the additional rules:
*H H
H* H
for every word symbol *
Iff the initial word is kernable using the given rule set into the word "H", the turing machine halts.
The **H, H** H rules can obviously be backtracked to produce whatever garbage one may desire, but crucially only when an H symbol is already present. H can only exist in the word when a halt has occurred, and as such these rules are only reachable when that condition is met. This is a crude way of erasing the rest of the word, but it should work just fine.
This seems to me like it would work. Pretty brilliant
Can’t the oracle problem be used in the exact same way? The desired state τ could have a rule of its own, with the following rule:
{τ} F (where τ represents the kerning word that corresponds to the desired Turing machine state)
And also the same *F F rules (where * just has to be a character used in the trace) as in your halting variation. There’s no need for the mirror, since there’s nothing to the right of the } that became F.
There’s a slight issue that there are infinite ways to represent a state as a word, since {τ} is the same as {0τ000}, but that can be easily fixed by changing the way the infinite tape problem is solved: instead of adding a third case for each rule in a word boundary, you can just add two rules:
} 0}
{ {0
That lets our “window” into the tape expand and contract as needed (as long as it’s empty), without the cursor being there. Maybe there’s always a way to get to the final state without getting extra zeroes on either end, but I’m not sure and this simplifies the keming machine anyway, so I’m leaving it.
Made it all the way through! Very cool! Thanks for reminding me why I like computer science, it's easy to get bogged down in the linear algebra and despair
Here is a technique for extending the proof to the exact matching case. The main obstacle, basically, is that you can only perform reversible operations. Any irreversible operations allow invalid historical information to be made up when going backwards. The solution to this problem is to gate the irreversible operations so that they can only apply after you have reached the target state, because then we don't care if solutions are being invented. Once you've seen the target state, you can freely erase information.
TracedExecution -> NoticeCorrectState -> EraseEverything -> SuccessHalt
So. Take the Turing machine provided by the adversary, and rewrite it. It needs to check after every (unrewritten) step whether or not the tape is in the desired state (drop marker, go to start of tape, compare tape against goal using hardcoded state transitions, return to marker on failure). When it does find that the tape is in the desired state, the Turing machine should transition into "hide the bodies" mode, where it puts (and keeps) a success marker at the start of the tape, then erases everything else, then returns to the origin and goes into the halt state on top of the success marker.
The key idea here is to only allow irreversible operations within accepting executions.
I think that still doesn’t work, though, because “hide the bodies” is the wiping Turing machine - which means for that stage to be reversible you now need a trace of how you removed the bodies, and everyone knows a paper trail gets you arrested. That’s really good terminology, though
My brain grew three sizes today.
Seriously though, I wish I had you as my teacher for Formal Languages and Automata in college.
Used this video twice as a sleep aid, third time I couldn't help myself and watched the whole thing, and I am grateful for that.
Keep being yourself Tom
This was a great watch! I haven’t done much of this sort of proof since my CS degree, and it made me realise that I do miss it. Thank you for making this lesson!
I'm a big fan of your general clownery, but this was a really great video too. I'll definitely watch if you decide to do more like it.
This was one of the best videos I've seen in a while. Having been incredibly into programming language theory in college and loving typing judgements, and in general loving random tangents, this was a fascinating watch. Your explanations were clear, easy to follow, and the topic was fascinating to me. Awesome work :)
Thanks! I'm glad you found it and liked it :)
Found this from via your deconstruct talk, is relevant to a turning machine project I'm working on and helped me understand it better!
I liked this! Your dry sort of wit makes a lot of your educational stuff really enjoyable, when when it's not coupled as tightly with games etc.
Ow please do these kind of things again! :-) It has been "only" 23 years ago since I had logic lectured to me in university, and I'll never mind the kind of refresher you provide.
36:22 Add another set of rules that are activated after reaching the halting state h:
*h -> h
h* -> h
So, the question would be: can you make
{ word representing the starting tape }
into
h
?
So, basically, it's like, after finding out that the machine halts, it halts and catches fire and burns up the whole thing, leaving only h.
It's possible to reverse the burn to get some other trace of the turing machine, traces of computation paths it never took. However this isn't a problem, since to do that it has to reach halting state first. In order to reach h by some "unintended" way, it first has to do it in the intended way.
I would totally watch more of this. Computational proof stuff in particular is my jam, but anything in the general vicinity of "math and computer science" would be just as excellent, especially if it's something you're interested in/excited about. You do a good job of explaining things, and also have a wonderful voice, which means that your lectures would be both informative and enjoyable to watch :P
Thanks on all counts! Already the pain of a full day of recording and editing is but a distant memory, so I'll probably find another topic to give this kind of treatment to in the future. :)
Well that was a recommendation rabbit hole I didn't expect to go down, but i liked it.
Brilliant video and I was pleasantly surprised to see a number of things pop up I've recently learned about in my hobbyist playing with formal logic. I was also pleased I spotted the infinite Turing tape and rule direction issues before "checking the answers". Also thanks for the laughs!
Wow this is really exciting
I actually love arcane ways to create turing complete systems - turing tarpits, like languages with a single operation [MOV, SUBLEQ - these are fun to work through and create common primitives like function calls, arithmetic, etc. Bitwise operations are surpsingly tricky]. And I like reducing things to NP complete (or NP-hard) problems like TSP & SAT. Recently, I've seen a really awesome proof showing that generalized Mario and Pokemon is NP complete
Notes and mistakes:
9:14 - you changed the state incorrectly, but you pointed that out
11:50 - let me have a go at the proof
Assume we have a procedure O(T, Tx) that solves the oracle problem for a turing machine T and eventual state Tx
Consider a turing machine T:
- if O(T, T2) is true, halt in state T1, otherwise halt in state T2
If O(T, T2) is true, T will never reach state T2, but if O(T, T2) is false, T will halt in state T2, therefore O cannot exist. QED
17:30 - A turing machine can only go one way in time, but the keming machine can "reverse" a state.
On your example, a turing machine can only go 10[0]a10111 => 101[1]a0111, but your keming machine can go in reverse
In fact, there is another problem, the * that you placed there
Let's expand the keming machine rules to include that *
Consider a TM with one state a, that always writes 1 and goes right.
The keming machine rules are:
[0]a1 1[1]a,
[0]a0 1[0]a,
[1]a1 1[1]a,
[1]a0 1[0]a
These rules are in fact legal according to your KM definition, but we can already see a few problems
The machine can write an arbitrary binary string to the right of the starting point (actually the beginning of the string of ones) by backtracking, so O("[0]a0", "[1]a0") is false, but it's trivially true for your KM
20:11 - The infinite tape issue is trivially solvable, add < and > markers for the end of the tape, and add rules
21:07 - This is a problem, if the tape can only be extended/shrunk when our marker is near it, equivalent TMs may not be reachable.
Say that the only rule I have is [0]a1 0[1]a
The state {00[0]a100} is not reachable from {0[0]a10}, even though they are equivalent (doesn't work for arbitrary match ranges, and rule count grows exponentially with match range)
On another hand, we can remove this issue if we just do linear time preprocessing, so I guess it doesn't matter
34:55 - Now we have an issue, if we come back to the oracle problem, we need to be able to convert the final TM state to our final word. In order to do that, we must know the order of execution of the turing machine!
We need a way to eat our execution trace, but that's impossible without destroying information, which means the reverse rule can create bogus information.
We need another set of rules, and encode the "current state is the same as the final state" into our rules to destroy all information in our word. So, our initial word is the output of some function on the T1 and Tx, and our final word is some destroying character that eats the entire word, say #.
Creating bogus information here doesn't matter, since we already found the state Tx reachable from T1
We can do something terribly inefficient, but that doesn't matter cause it's a decidability proof.
Assume we execute these rules while the tape looks something like áååć{101010[1]a010}010a]1[010101^
When the > returns to our pointer, we can either continue execution, or send a signal to the right side.
We can write a rule that duplicates the string at the end, safely storing one copy behind the caret, then turns the } into a !.
When we see 0!0, 1!1, a!a, ]!«, etc. we erase the characters on the sides.
If ! reaches {, it becomes a # and eats everything, reaching the final word which is just #.
Unless I missed something, this should work - we can't continue execution until the }! and ^ return to their place and all data matches (the copy safely stored behind the caret must match before we send the signal back to continue execution)
36:33 - oh, I was overthinking it, but I guess the above is a "proof" if it happens to work
42:50 - The \Rightarrow symbol is confusing to me, cause I was taught it means "implies", we don't use the
ightarrow symbol in Poland [when it comes to logic - we use it for functions]
44:01 - OOOH, sweet! This looks basically exactly the same as linear type systems, each object must be used exactly once, which is useful for things like lock guards, channels, tokens that can only be used once, tokens that imply ownership of a resource, etc.
47:35 - Yeah... You can't use these rules as assumptions, as that means you can only use them once, and must use them once, which fails even in this example. You must keep these rules as separate axioms/sequents
- ...Okay. ! works, feels like a hack
Seems you followed along quite well! :) Indeed linear type systems come from linear logic (e.g. via Curry-Howard).
Right, to clarify a few things
- In the oracle proof I said that O cannot exist - that's not true - O cannot be implemented on a TM, not sure how hypercomputation plays into this, or if it does at all.
- In the decidability "proof", I made a few typos, ! can eat characters if the ones on its side are the same, so [![ !, and I omitted some information. We must not allow execution while ! is free, so the [] will be changed to something else or reordered. Reordering is enough, as even if ! writes it's own functional execution pointer, the shuttle will block it from being useful. [EDIT: Actually that's false, ! can write one on the left, but I'm not sure if that's useful either]
I also intentionally omitted the signaling method and duplication procedure - creating it is error prone, but it's definitely possible as it can be implemented easily with other computing methods, to which a TM (which our KM is) is equivalent.
I also omitted a note as to why it's okay to only reverse the Tx comparison string without additional encoding, but I felt it was obvious
@@animowany111 Since you like obscure Turing machines, you may be interested to know that Magic: the Gathering is proven to be Turing complete by constructing a Turing machine with the rules of the game.
Hi Tom I'm one of the 3 people who got through it and I thought it was well explained and insightful. I think I get why regex search and replace is turing complete now! You could use similar method as you explained at 22:21, you wouldn't even need the trace because search and replace is unidirectional.
Definietly liked it, one of the most clear and concise mathematical explanations I've seen on youtube. The reduction proof is elegant, especially the part with encoding a trace. The linear logic proof was also nice, simple in a way but never a connection I would've thought of myself.
This is absolutely amazing. I understand that it's a lot of work to put together but, if inspiration strikes, I would gladly drop everything to watch another through. Really fascinating stuff: it's inspired me to take a deep dive. Thanks, and keep it up!
Thank you for the encouragement! :)
I absolutely loved this by the way. I thought that it was going to be boring at the beginning but it ended up interesting to think through why some of the things you were saying had to work. Thanks Tom!
This was actually super informative and interesting!
I ddin't understand the part on linear logic too well, but that was the most coherent explanation of a turing machine I've ever heard, and your explanation of everything related to the kerning problem was crystal clear!
This video is awesome. Honestly, I'd love to see one about the lambda or combinator calculus in this style, or your usual style, if you ever felt like making one.
came for the goofy engineering projects, stayed for the pure maths (CS and pure maths are cousins and good friends, anyway). Thanks, Dr. Tom Vii! I think I've binged nearly your entire channel at this point, it's absolutely fantastic, PLEASE keep up the good work! (since youtube is so unreliable nowadays, i bookmarked your webpage like its 2008 or something.... bizarre to think of the internet as still full of addresses and websites instead of Five Platforms All Sharing Content From The Other Four)
I love this. High-level attention-grabbing videos that draw you into these intense learning sessions are fantastic.
Stumbled upon this, after watching one of Micheal Stevens videos, and absolutely loved watching this
Rewatched this beauty again. Great stuff
I am a recent fan of your channel and a student learning computer science in high school and your channel is one of the most entertaining and interesting channels i have seen on youtube. This video was very informative and entertaining, more videos like this should be published to this site.
Thanks for watching and for the encouragement :) If you can follow this in high school, you're off to a great start!
This is good. More please.
Hey there! I'm the other one of the 3 people who watched through. It's really cool seeing these kinds of proofs on UA-cam, so even if you don't make any more, I appreciated and enjoyed watching this video!
I love this video!
Not sure whether anyone’s mentioned this, but this is equivalent to the Word Problem in group theory. If you let the rules for kerning strings be the relations in the presentation of a group, then the strings become elements of the group, and the question of whether one string can be transformed into another by repeated application of the rules becomes the question of whether two elements are equal.
Hey there!
Mathematics master student here, working on logic (studying "propositions as types" correspondence righ now).
I didn't expect to bump into linear logic while watching this but it was a nice surprise.
I loved the shuttle idea for TM encoding. As others have pointed out you can remove the states trace prefix, when in the final configuration, adding some rewriting rules that involve the final configuration.
But if the Touring machine has a final state (or many accepting states) you could also change it in a special eraser shuttle that slides left until it reaches the trace then it deletes the state symbols; this way there is no need to name the desired final state in the rewriting roules.
Something like this, where f is the final state and « is the eraser shuttle:
[0]f «0
[1]f «1
0« «0
1« «1
*{« {«
This is a fantastic video. I'm a CS&Philosophy undergrad at Oxford, and found this video awesome (in particular, I now get linear logic, which I tried unsuccessfully to grok via the wikipedia page before). I might spread this as entertaining revision for our models of computation course. Thanks for taking the time to make this, and I'd totally watch more Tom Academy!
Aw thanks! :)
Thanks, that was great. I was avoiding this one for a long time, thought that was going to be boring.
It wasn't, it was great.
I just wanted you to know I love your stuff. Please keep doing this.
I'm in engineering, but I do these kinds of "Recreational maths" kind of stuff all the time, and I love seeing other people do the same. ^-^
Thanks for telling me, and thanks for watching :)
This was a really good explaination. I would never have guessed that kerning is so closely related to the halting problem but logic manages to surprise me all the time.
Should you ever feel the urge to make something like this again, please do!
I'm a huge fan of the mathematical side of computation and vice versa, and I've been learning category theory on my own and that has exposed me to so many different branches of mathematics, including the different flavors of logic. I really enjoyed the concrete example of linear logic!
I'd love a video in this format on the P vs NP problem, in particular reducing problems to ones whose complexity we know like 3-sat etc. I never quite understood why finding a hamiltonian path can be reduced in this way, or perhaps I'm totally misunderstanding the whole thing. Augh!!
For reference I study pure maths and just finished my second year, and I found this crystal clear and very interesting, and I now may consider computer science as an option. Great video :)
i work at the math tutoring center at my university and a cs student came and asked me "do you know languages and words in computer science?" and I had no idea what he was talking about... I was able to read his lecture notes and figure it out and interpret it for him, turns out it was the stuff you explained in the beginning! would have been much quicker tutoring session if i had seen this video sooner lol
can we have more tom academy, pretty please
Not sure how you ended up on my suggested videos, but boy am I glad you did. These math heavy videos in particular were really fun.
I loved this!
I've been studying IT at university for 1 year now, where I took an optional logic course that introduced me to some variation of a few of the concepts and techniques used in this video.
Anyway, I thoroughly enjoyed that course and it left me desperately wanting more.
I was also very curious to know exactly how such tools could be used in more "practical" situations (as opposed to simple practice exercises such as proving DeMorgan's law with sequents), and your video has provided that.
Thank you!
Fascinating update: MELL decidability is once again an open problem, due to the fundamental issues with proof-based math discussed by Tom in this very video.
Link: hal.inria.fr/hal-01870148/document
Thank you! This has taught me so much! I heard about Turing machines, lambda calculus and linear logic in context of type theory of programming languages, but this is the first time I see them applied in math. This is very beautiful stuff :)
The first time I tried to watch this I didn’t really understand but a while later I came back and it was really entertaining this time and I think I understood most of the things
Thank you Tom
That’s great! You’re welcome :)
As an undergrad cs student taking a computational theory class this video was a delight. This ties together the 2 main focuses of the course (sequent calculus and languages/Turing machines) in a fun way. Make Than Academy real please
I’ve watched this video a few times and every time I do I always force myself to think about how to “fix” the keming problem so that you can ask the question of if you can translate w1 to w2 and not some wacky w3, but this time I was making pasta and the solution finally came to me
The idea is that once you have some w3 which contains w2, it doesn’t really matter what you do with your keming machine, so long as your rules don’t create w2s where they never were
That said, you can add some clearing rules to the machine that look like this:
*w2 w2
w2* w2
This does some funky things to the machine - once you’ve achieved a state with w2 in it, for instance, you can use this rules to get any string that contains w2 from it. That doesn’t matter though, because the answer to “can you get w2” is always yes *only if you can naturally get w2*, and no only if you can never reach w2
This shows that the keming problem proper is also undecidable, and also shows that I am far more deserving of a PhD than Tom 7 is. I will be sending my results to your institution and we’ll see how it goes
In all seriousness Tom, this video in particular kinda set my brain on fire when I was a high school student and didn’t really know any of this theory of CS nonsense, now I’ve graduated undergrad as a CS/math major with a very special interest in this stuff, and a lot of my initial inspiration started with this, I’m really happy in my own knowledge and never want to stop learning about this, and I hope that serves me well in grad school :)
Oh also, I understand why this apparently simple fix didn’t come to you (assuming it’s even right, I’m still making the pasta); there’s a parsing tree hiding underneath this, whereas a Turing machine is a deterministic machine, and there are no branches in the path in the states allowed to produce, and you’d want your simulation of a Turing machine to also be deterministic - these rules I added are exactly the type that forced you to change it originally, but it’s fine because it’s only nondeterministic when there’s a w2 to be found, and there’s a path along that massive series of branching that ends at w2
I love linear (and other) logics and really enjoyed the video. If you ever feel like making another one of these, I'll be among the three!
That's such a neat proof... I'd watch you teaching serious stuff more often! Not a lot of views, but you've blown my mind at that's got to be worth something.
36:20 Unsure if anyone has pointed this out, but there's a relatively straightforward way to generalize your solution to get the exact Kerning problem; you just have to include the specific T_F as part of the kerning rules, which lets you delete the trace once the keming machine has reached a state corresponding to T_F. Deleting the trace means that we sort of break the symmetry you carefully built, so the KM states are no longer one-to-one with the TM states. Critically though, these extra states can only be accessed after the KM has already reached a state corresponding to T_F, so we are still in the situation where "the TM can reach the state T_F if and only if the KM can reach the word W_F".
As for the formal implementation, you would add some rules to the KM that let you lengthen and shorten the tape arbitrarily, so "{0" equals "{", and likewise "0}" equals "}". After that, you would define the word W_F to be encoded like "{T_F}", and given the previous rules it doesn't really matter where exactly we cut off the infinite zeros of the T_F state. You also need a way to delete the machine head from the KM word, so add a schema of rules to the KM which runs over all the words which are identical to W_F except for the presence of a machine head, and sends you to the word W_F. Finally, you would add a schema of rules which basically says "*W_F" equals "W_F" where the symbol * varies over all the (finitely many) symbols which can appear in the trace.
So, in the case that the TM never reaches the T_F state, and the KM is currently in a state reachable by the TM (with a trace corresponding to a valid history of the TM), then necessarily that state doesn't correspond to T_F. It follows that the KM cannot delete the machine head, and it cannot erroneously delete the trace, so the only words it can access are corresponding to other states reachable by the TM. It then follows by induction that, after any finite number of steps, the KM word will always correspond to a state reachable by the TM. Conversely if the TM does reach the T_F state, it's trivial to prove that the KM can reach the W_F word by just following the corresponding rules. It follows that the KM can reach the W_F word if and only if the TM reaches the T_F state.
So, suppose (!) you have a general procedure such that, given any KM and any words W_1, W_F, your procedure can decide whether the KM can turn the word W_1 into the word W_F. Then, given any turing machine and tape states T_1, T_F, we can construct a corresponding KM and words W_1 and W_F such that the KM converts W_1 into W_F if and only if the turning machine reaches state T_F when initialized on the input tape T_1. We can generate that KM problem procedurally, and then apply the KM solving procedure to solve the corresponding oracle problem (contradiction!), QED Kerning is undecidable.
Hey dude! That was awesome! I wish teachers at my University explained things at you did. Already knew all the theory but the fact of seeing it applied was amazing.
Great! Thanks for telling me :)
This is so cool!!! I’d love to hear more about linear logic! You’re a fantastic teacher :)
This is lovely! I believe this is equivalent to the word problem for groups - what a lovely framing! Great stuff :)
This was amazing. :) Topics that are certainly over my head academically, but you explained them in a way that I was able to grasp the necessary bits for your proofs to work. I'd personally love to see more like this.
Very cool, thanks! Although natural, I wasn't expecting MELL to show up. Linear logic's greatly interesting.
A funny thing about it: exponentials aren't determined up to equivalence by their introduction and elimination rules, so you can have multiple exponentials pairs (! , ?) and iirc if you have enough of them it makes MELL (MEEEEELL?) undecidable. Don't quote me on that tho
Idea for exact matching:
Target word is w_2. Add a rule for every alphabet element * like this:
w_2* w_2
*w_2 w_2
Essentially, as soon as you have w_2, delete everything around it. If the Keming machine you presented can find a way to transform w_1 into sth with w_2 as a substring, the altered KM with these two sets of rules can obviously transform w_1 into w_2 by doing the same transformations as the KM and then applying these deletion rules over and over.
Also the deletion rules (in particular the reverse case) does not add any new possibilities to go from w_1 to w_2 where we shouldn't be able to. Intuitively, the reverse way could only be applied when w_2 is already there in our transformed word. However, if w_2 is already in the transformed word then this means the KM without deletion rules would answer yes, so in all cases where we are able to apply any direction of the deletion rules we know that both the KM with and without deletion rules will answer "yes".
We can write all kinds of gibberish into the word of course once we created w_2, but that doesn't matter at that point anymore.
More formally you can probably do a proof by structural induction, but I think the idea is better grasped by an intuitive explanation.
Just wanted to say that you're awesome. I watched all the way through and this absolutely made my day.
I enjoyed the video.
Regarding 36:23: "I couldn't think of any way to work around this problem": that is because it is impossible.
Note that when I use 'tape', that includes the pointer and Turning machine internal state.
Important for this proof: a start tape and an end tape can have different representations. We use start(A) to represent the representation of a start tape A, and end(B) to represent the representation of an end tape B. This proof works for any representation of the start and end tapes, so no kerning rules exist which can solve this problem where the full word is w_f, not just where w_f is a substring of the word.
Proof sketch:
Q-S->T means that word Q can be transformed to word T via the sequence of kerning rules S.
0 is the tape with a single 0, and 1 is the tape with a single 1.
We use the eraser Turing machine mentioned in the video.
We use proof by contradiction, so we assume that each Turing machine has a kerning ruleset which accepts all pairs of start and end tape for which the Turing machine can reach the end tape from the start tape.
We now prove that this ruleset must have rules that would permit a sequence REVERSE which leads the kerning ruleset to accept start(0)-REVERSE->end(1).
1. There must be a sequence of kerning rules ERASE that would have it accept start(1)-ERASE->end(0), because the eraser can actually do that.
2. Similarly, there must be a sequence of rules ID that accepts start(A)-ID->end(A), again because the eraser can do that (it can reach the tape A from tape A by doing nothing).
3. Because all kerning rules are bidirectional, we can apply the rules in any sequence S that accepts Q->T in the opposite order to get a sequence of rules called !S that accepts T->Q. In particular, given a rule S which accepts start(A)-S->end(B), we can use !S to accepts end(B)-!S->start(A).
4. The sequence REVERSE=[ID, !ERASE, ID]. This transforms the sequence as follows: start(0)-ID->end(0)-!ERASE->start(1)-ID->end(1)
This proves that any kerning ruleset would have a sequence of rules which can be applied to make it accept that the reverser would reach tape 1 from tape 0. This is false, so the assumption that such a kerning ruleset exists must be false. QED.
he turned a word into a turing machine
funniest thing i've ever seen
I know you've probably already decided what kind of creative endeavors you'll be persuing since this video was released, but I for one was really interested to hear you explain interesting concepts through this silly problem and would love to see more stuff like it!
What is this? TWO videos!? AND IT'S NOT EVEN APRIL FOOLS DAY!?
OMG this is perfect. Thanks, now I actually understand what linear (and ordered) logics are about. I heard about it from Robert Harper's lectures on Homotopy Type Theory but never got to see it working until now.
This is a great video! I have a thought though, I think there's a shorter path to show the kerning problem is undecidable. The question of whether an unrestricted grammar can generate a particular string is already known to be undecidable, so it would suffice to show that a keming machine is equivalent to a UG. So to turn a set of rules, w1 and w2 into a UG I do the following: 1) define a rule from the start symbol to w1 : S -> w1. e.g. "S -> cool". 2) the keming rules just become production rules as-is. 3) define an ending rule: w2 -> epsilon (just some special terminal symbol that's not in w1 or w2). 4) show that this grammar is a UG (Chomsky type 0) by showing it is more general than a context-sensitive grammar(type 1): this part is easy, a CSG cannot have any rules that produce a shorter output than input, so no "r n -> m" which is obv allowed by a keming machine. So a KM is a UG, QED. (Quote Ehren Dabout decidability)
Clever idea, but this is a reduction in the wrong direction - if you show that KMs are UGs, then decidability of UGs implies decidability of KMs, not the other way around. You would have to find some way to (computably) transform an arbitrary grammar into a Keming Machine.
I do recognize that you have a step where you show that the grammars you end up with are not inside some known class of decidable grammars, but there are many possible grammars that generate the same language. Yes, the grammar you end up with via this reduction is not context-sensitive, but that does not mean there does not exist a context-sensitive grammar that generates the same language.
@@Your2ndPlanB Oh yeah! It seems so obvious that I missed that now that you point it out.
Wait: I got it!! To show the kerning problem undecidable, you just need to translate what you would use as your final state to another rule (and add another symbol: E). You would say final state becomes E, and (any trace)E becomes E. Then, ask if you will ever end up with plain E. Even tho you might be able to reach any state be un deleting trace, it won’t matter because you would have to reach the final state first. Thus, the kerning problem is undecidable.
I wouldn't mind a few more episodes of Tom Academy, this really makes me miss my logic courses in college
I often watch your videos more than once cause they are information rich (this is probably gonna be one of them). The paper video was super juicy too!
Keep'em coming!
Really enjoyed the video! As someone who has only had one course in formal computation theory, this really makes me want to study it further! Thanks for the quality content!
36:00 Couldn't you make an symbol END which matches T_f and also itself plus any history symbol to the left? Then once the tape reaches T_f, END is substituted and it can start eating the history to the left of it. w_f is just END. Reversibility wouldn't be a problem, since END would only be possible iff the desired tape state was reachable in the first place.
In fact, you don't even need an extra END symbol. You only need a new rule, equivalent to *{T_f} {T_f} .
Dude look a tree
I’m very sleep deprived and idk if this works but can’t you take the END and create any trace with it? Any bidirectional rule where many inputs lead to the same output causes the same problem, I think
Dominic Littlewood but then {T_f} *{T_f}. Just create whatever trace you want and you have permission to write the string all 1s again
That only matters if the thing you're looking for (i.e. T_f) is all 1s. So you're saying that if you can get to all 1s with a trace then you can get to all 1s. Which... doesn't actually matter.
@@powerjbn9283 user "Dude look a tree
" already said reversibility wouldn't be a problem. after END writes whatever it wants, it can't just destroy itself without a trace. Even if you have 2 ENDs, there'd still be 1 END left after one destroys the other. END could be used to create stuff, but by the time you create END, you've already managed to halt, and just need to delete stuff until destination word of lone END is reached. It's like a catch 22
I made it all the way through. Also I thoroughly enjoyed every minute of it.
Thank you!
Awesome video, I'm going to share this with the professor I had for a Computational Models class. The anagraphing part of it though leaves me wanting more. I'm familiar with showing using reduction to show that some problems are impossible to make a program for, like showing that two turing machines having the same language implies you can solve the halting problem. For the Linear Logic part of the video though, I need to see why provability in linear logic is decidable before I'm fully satisfied.
I really enjoyed the lesson! Would love to see you covering more topics you’re interested in.
Awesome video! I thoroughly enjoyed seeing logic applied in such a beautiful way
I’d love to see more content like this
i feel like i would have enjoyed the mathematics far more during my comp sci degree if I'd had a lecturer as interesting as yourself, I'd love to see more
I believe that generalized kerning should be possible in the form of x -> y, but not x -> blahyblah. All it really depends on is if you allow for a rule that transforms into an empty string, or not. If you allow for it then you've made it into unrestricted grammar, which is undecidable because it is a TM. If you don't allow for it, which I think makes more sense when you think of real life kerning, then you are restricted to context sensitive grammar which does let you generalize the kerning problem.
Also, no I am not 5 years late, I just thought I should get a CS degree first to make sure before I commented.
this was really good. i did this last year and it was good to re-visit and think about some different problems.
This is so much easier to understand than the wikipedia article for linear logic. The article just throws a bunch of symbols at you and asks you to invent your own intuitions. The video throws them at you one at a time, and explains some possible intuitions. I should study more maths.