Lambda Calculus vs. Turing Machines (Theory of Computation)

  Рет қаралды 13,945

Advait Shinde

Advait Shinde

4 жыл бұрын

Advait Shinde discusses the history of the theory of computation, delving into axiomatic thinking, Peano axioms, Turing Machines, Lambda Calculus, the Y Combinator, and the Von Neumann Model.
Brilliant explanation about the Y Combinator: mvanier.livejournal.com/2897....
Advait is the CEO of GoGuardian - a K12 education software company in Los Angeles: www.goguardian.com/

Пікірлер: 39
@orki974
@orki974 4 жыл бұрын
Thank you very much for this amazing sum up of computing history, the picture is clearer for me and this is invaluable! But I would like to ask you something more. I would like to really see and understand the "reduction" of lambda calculus to Turing machine and vice versa. Do you have a good resource (book, article, courses, anything...) on this topic? The best would be (I guess) a rewrite of the original proof in modern terms :)
@AdvaitShinde
@AdvaitShinde 4 жыл бұрын
Thanks orki! I'm assuming you want more of an intuitive bridge than a formal proof. If so, consider that what you describe as "reduction" can instead be done as a "emulation". Instead of translating the representations, you can simply write a Turing machine emulator in lambda calculus and a lambda calculus evaluator as a Turing machine. Once this is done, any program in one tower can be run via the other tower. I find the above approach more satisfying than the formal proof which doesn't help my intuition.
@orki974
@orki974 4 жыл бұрын
@@AdvaitShinde thank you for the hint, you completely change my mindset about this question 🙂
@zyansheep
@zyansheep 2 жыл бұрын
@@AdvaitShinde for efficiency purposes though, wouldn't it be better to directly translate between the two?
@AdvaitShinde
@AdvaitShinde 2 жыл бұрын
​@@zyansheep there's two questions here: 1. Are Turing Machines and Lambda Calculus equivalently expressive (i.e. are there ideas in one that can't be expressed in another)? 2. What's the most efficient way to run a TM in LC or vice versa? #1 is addressed by emulation as discussed above (they're equivalently expressive - i.e. "Turing Complete"). #2 is more complicated. What does "efficient" mean? In what sense can you compare two TMs or LC programs and say one is more efficient than the other? Is it program size? Is it number of runtime steps? Is it amount of Turing Tape consumed (memory usage)? Is it runtime duration on an x86 machine (which is further just emulating a TM or LC interpreter)? Based on your definition of efficiency you get into all kinds of interesting sub-problems related to program optimization. In fact, this whole field of thinking is basically what you'd consider "compiler design". A complier is simply a program that converts code in one language into code in another language. As you can imagine, compiler optimization is a really deep topic that's outside the scope of this conversation but still completely understandable if you're interested. I would check out the many videos about it on KZbin! All things considered, I'd encourage you to look beyond the idea that "efficiency" is a single/simple construct.
@Danhec95
@Danhec95 3 жыл бұрын
Great presentation! Something I would nitpick is that a system is "Turing complete" if it is proven to be equivalent to a "Universal" TM, not just any TM. I agree that Lambda calculus is the "traditional" mathematical approach to computation. It's really elegant and mind-blowing that it can achieve general computation (especially the way recursion comes out of nowhere). However, the model defined by TM's are so intuitive and have such "low-level" concepts that makes 1) "easy" to implement in hardware and 2) convince you that algorithms and computation can really be described entirely by it. Amazing title LOL
@user-pl5ko9kb9f
@user-pl5ko9kb9f 13 күн бұрын
Very interesting Talk... recommend it for every programmer
3 жыл бұрын
Best explanation I ever saw about the subject. I really appreciate the way it links to something I actually used like jQuery.
@tazuarce7814
@tazuarce7814 4 күн бұрын
excelent talk; greetings from argentina
@gongfei
@gongfei 3 жыл бұрын
Great talk! Thank you!
@lil_peepka
@lil_peepka 9 ай бұрын
This is pure gold
@Supakills101
@Supakills101 2 жыл бұрын
One of the best talks I've ever seen.
@AdvaitShinde
@AdvaitShinde 2 жыл бұрын
Thanks Yui!
@kiranmnrao1914
@kiranmnrao1914 9 ай бұрын
Really a great talk @advait.
@anieldev
@anieldev 2 жыл бұрын
thank you! elite presentation.
@anieldev
@anieldev 2 жыл бұрын
6 months later and i have finally internalized all that was said in this talk. now i’m neck deep in combinators due to a motivation in further reducing the axiomatic assumptions. So far, as far as i know, the most simplistic combinatory logic system can be built with the SK combinators which is a reduced version of the untyped lambda calculus. Thanks to this talk I was able to come at this with a conceptual map to orient my understanding! so thanks again!
@eugenemosh3658
@eugenemosh3658 Жыл бұрын
Thnx!!
@polymloth
@polymloth Ай бұрын
Great talk! But I gotta say, I don’t like how unstable the tower visualisation looks. ‘:D
@AdvaitShinde
@AdvaitShinde Ай бұрын
😂 I was hoping to not-so-subtly imply that the functional tower is better than the imperative one :)
@jgcooper
@jgcooper 2 жыл бұрын
Do you have any book recommendations on the subject?
@nikhilsulghur7589
@nikhilsulghur7589 9 ай бұрын
Introduction to the Theory of Computation Textbook by Michael Sipser
@ahbarahad3203
@ahbarahad3203 Ай бұрын
@@nikhilsulghur7589 It doesnt talk about Lambda Calculus though
@erikawwad7653
@erikawwad7653 3 жыл бұрын
omg how have you not blown up yet
@v_donets
@v_donets Жыл бұрын
Cheers Mr Advait Shinde! My team have been working on an modifying Reduction Strategies, applying some reduction extensions and we got stack in the idea of existing an optimal strategy, with which we would be able to compare our strategy. Is it exist any works or do you have any ideas about a fact that there are no optimal Reduction Strategy? Thanks for your attention! Sincerely, V. Donets.
@AdvaitShinde
@AdvaitShinde Жыл бұрын
Hello! Perhaps you can send me more info about the problem you are facing?
@v_donets
@v_donets Жыл бұрын
@@AdvaitShinde so we develop two sorts of modifications for default Reduction Strategies (like the Left outer (Normal strategy) and the Right inner (reduce by data)): in the first sort we try to make reduction step by some assumption about depth of the redex in the tree term tree and the second one using reinforcement learning. And for some generated terms we couldn't see a much impact of the reduction strategy on the count of reductions (yeah, there are other metrics for measuring effectiveness, but it going to be the next step), so we suppose that there is no the universal optimal strategy (which give a minimal count of reductions for the all possible terms) with which we can compare an effectiveness of our algorithm and suppose expediency of all this modifications. So in other words our current problem: we couldn't find works (theoretical or practical) which prove that it is impossible or possible to create some sort of universal strategy which give the minimum count of reductions for any possible term.
@AdvaitShinde
@AdvaitShinde Жыл бұрын
@@v_donets Extremely interesting! Can you send me an email about your specific reduction strategies? I think I may have a proof for you to consider. Email is in my YT channel about page.
@ujjawalsinha8968
@ujjawalsinha8968 3 жыл бұрын
"Axioms are arbitrary but some axiom towers are useful" "All Models are Wrong, but Some are useful"
@Anon.G
@Anon.G Жыл бұрын
Nothing wrong with the models
@RockAristote
@RockAristote 3 жыл бұрын
If a human can produce a Turing machine, does it mean that a human is, at least, a Turing machine ? What about DNA, RNA, proteins... the universe ?
@AdvaitShinde
@AdvaitShinde 3 жыл бұрын
There's a very interesting distinction here between a theoretical universal computer vs. an actual computer. Consider that the theoretical universal computers we discussed had no limits on input size (i.e. Lambda Calculus can handle arbitrarily long programs and Turning machines have an arbitrarily large tape). However, once we go and implement real computers, physical constraints impose limitations on our capacity to compute. Given any physical computer (arbitrarily large/complicated), there will always exist a finite limit with regards to its capacity to compute because of its physical limitations. Therefore, you can argue that any physical machine is not actually a universal computer because of these limits! Given this, humans aren't Turning machines. Moreover we've never actually built a Turing machine because Turning machines are entirely theoretical and are not buildable in the physical finite universe. All of this said, your question can be slightly rephrased and answered usefully: if you're ok with physical limitations on computation how can we judge humans and DNA/RNA with regards to their computational capability? It should be obvious that humans are general computers (within extremely modest constraints). These researches have gone on to describe (infinitely many) ways we can use DNA/RNA to compute things: arxiv.org/ftp/arxiv/papers/2008/2008.08814.pdf Considering the simplicity of lambda calculus (or even SK calculus which is mentioned in the paper and is even more simple) it shouldn't be too surprising that we can build physical and biological machines that are "universal" computers within their physical limitations. The fact that universal computation, at its most fundamental level, is actually extremely simple is perhaps the core thesis of this talk and an idea that continues to blow my mind every day.
@RockAristote
@RockAristote 3 жыл бұрын
@@AdvaitShinde Thank you ! It is very interesting indeed ! Have you read The revolutionary phenotype ? It’s about how the phenotype could become a replicator and subjugate the DNA.
@jmhimara
@jmhimara 2 жыл бұрын
hmm, I thought you could do loops in Lambda calculus -- using a construct similar to the y-combinator...
@AdvaitShinde
@AdvaitShinde 2 жыл бұрын
Loops are an imperative construct and do not exist in the lambda world. Instead, anything that you would use a loop for can instead be expressed with recursion. As we discussed in the video, recursion can be obtained using the Y Combinator. So in a sense we can get loop-like functionality with Y but I wouldn’t describe that as “doing loops in Lambda calculus”. Hope that helps!
@subramaniannk3364
@subramaniannk3364 3 жыл бұрын
Enjoyed your video very much! I am a novice here. Would it be correct to say that Lambda calculus focuses more on the syntax and less on the semantics? I ask this because you defined "True" and "False" as functions in the video. If this question does not make sense, please do ignore. . . Secondly, would you happen to know the contributions of Claude Shannon to computing? Reading Shannon's Wikipedia page, I understand that he showed the Boolean algebra could be implemented with electrical circuits. What I do not understand is why Shannon is not viewed as a great figure in computing like Turing? Digital computing is, I think, Shannon's idea
@AdvaitShinde
@AdvaitShinde 3 жыл бұрын
I think your judgement of LC focusing on syntax over semantics is misguided. Think about LC from an axiomatic context where nothing is available for use without being explicitly denoted as an axiom. Here, LC has no concept of numbers or booleans - it *only* has functions. This might seem limiting but it turns out that booleans and the natural numbers can be defined in terms of functions! We don't need separate axiomatic structures for these concepts. This is similar to the fact that Peano didn't need to explicitly define the number 7 as it was defined as syntactic sugar for "S(S(S(S(S(S(S(0)))))))". Don't think about whether this is practically useful - nobody programs computers in LC. Instead think about LC as the minimum axiomatic definition for computing and consider how tiny of a definition it is for such a powerful concept! Finally I would absolutely include Shannon on a list with Turing, Godel, and Von Neumann!
@aMulliganStew
@aMulliganStew 2 ай бұрын
10:03 -- Hey, that's cute!
@henriquekleinpedroso2029
@henriquekleinpedroso2029 29 күн бұрын
I was excited because I have been capable to learn Turing's work but was never capable to understand the real meaning of Church's lambda calculus. This teacher is so incompetent that not only I remained ignorant on Church's work but also I almost forgot the knowledge I have hardly acquired about Turing machines... big fraudster...
The Boundary of Computation
12:59
Mutual Information
Рет қаралды 905 М.
Қайрат Нұртас & ИРИНА КАЙРАТОВНА - Түн
03:41
RAKHMONOV ENTERTAINMENT
Рет қаралды 1,8 МЛН
ISSEI funny story😂😂😂Strange World | Pink with inoCat
00:36
ISSEI / いっせい
Рет қаралды 16 МЛН
Lambda Calculus - Computerphile
12:40
Computerphile
Рет қаралды 996 М.
Turing Machines - How Computer Science Was Created By Accident
17:05
The Most Difficult Program to Compute? - Computerphile
14:55
Computerphile
Рет қаралды 1,3 МЛН
"Propositions as Types" by Philip Wadler
42:43
Strange Loop Conference
Рет қаралды 123 М.
Making a computer Turing complete
18:20
Ben Eater
Рет қаралды 532 М.
What is a Monad? - Computerphile
21:50
Computerphile
Рет қаралды 588 М.
A Sensible Introduction to Category Theory
26:20
Oliver Lugg
Рет қаралды 414 М.
Essentials: Functional Programming's Y Combinator - Computerphile
13:26
The PA042 SAMSUNG S24 Ultra phone cage turns your phone into a pro camera!
0:24
Добавления ключа в домофон ДомРу
0:18
Я Создал Новый Айфон!
0:59
FLV
Рет қаралды 2,7 МЛН