Introduction to Combinatory Logic -

  Рет қаралды 17,433

Malta Mathematical Society

Malta Mathematical Society

Күн бұрын

This is Alexander Farrugia's and Giorgio Grigolo's submission to the second 3blue1brown Summer of Math Exposition.
#some2 #mathematics #combinators #logic
Music: Icelandic Arpeggios - DivKid

Пікірлер: 98
@charlesrosenbauer3135
@charlesrosenbauer3135 9 ай бұрын
As far as displaying large combinator systems goes, it would probably be easier to appreciate their structure if drawn as a tree as opposed to with tons of nested parentheses.
@jackozeehakkjuz
@jackozeehakkjuz 3 ай бұрын
It would be nice to see it in action in a similar way to the legendary post "to dissect a mockingjay".
@Godfather-qr6ej
@Godfather-qr6ej Ай бұрын
​@@jackozeehakkjuz I could not find that post? Are you referring to the book, to mock a mockingbird?
@jackozeehakkjuz
@jackozeehakkjuz Ай бұрын
@@Godfather-qr6ej Sorry, yes. To mock a mockingjay is a 1985 book by Raymond Smullyan. However, my intention was to point to the 1996 post by David Keenan called "To dissect a mockingjay", which is partly based on Smullyan's book. I hope you can find it now. I already edited my original comment to fix this mistake.
@jackozeehakkjuz
@jackozeehakkjuz Ай бұрын
@@Godfather-qr6ej I tried to post the link here a couple of times but I think youtube keeps deleting it.
@Godfather-qr6ej
@Godfather-qr6ej Ай бұрын
@@jackozeehakkjuz yes I found "To dissect a mockingjay" can I ask you a question? where are combinators usefull? I've heard about them from people in lambda calculus as a way to make a tiny turing complete machine. and from APL users who use combinators in some practical way I dont know how?
@paskoolio
@paskoolio 6 ай бұрын
The single combinator from which S and K can be defined goes well beyond Baker. I was a student of Corrado Boehm in 1985 (from Boehm trees in lambda calculus) and he taught us about the single combinator in 1985... This video reminded me of his fantastic lectures on combinatory logic, thank you.
@caselbravo
@caselbravo Жыл бұрын
Fantastic work thanks to everyone involved ! 🕊️
@r4fa3l59
@r4fa3l59 9 ай бұрын
Oh my god! This is spectacular!
@GuyMichaely
@GuyMichaely Жыл бұрын
9:30 Why does [I]_x become KI and not K? the second bullet applies and it does not say to append I
@xactxx
@xactxx Жыл бұрын
Whoops, that's a mistake from our part. That should be [f]_x = Kf, if f does not contain x. Apologies.
@manawa3832
@manawa3832 2 ай бұрын
@@xactxx what is your opinion of concatenative calculus? i tried to understand the contribution but could not. it just seems like a style change and an implementation detail of adding a fictitious data structure like a stack to create a context for the program. for a calculus that is supposed to be context-free like combinatorial logic, concatenative calculus proposes a big ol context underpinning it.
@jonaskoelker
@jonaskoelker Жыл бұрын
Very nice presentation, thank you. A suggestion for future videos: when you show some kind of process, e.g. the SKIBC rewrite/translation, it would be really nice if all previous steps were shown along with the current step, e.g. with an additive/accumulative animation. That way, I could compare steps n and n+1 which would help me understand what the rules mean and how to apply them.
@xactxx
@xactxx Жыл бұрын
You're welcome! Thank you very much for your kind comment. We'll take your suggestion for future videos!
@khaliliskarous2225
@khaliliskarous2225 4 ай бұрын
This is really beautifully done!
@NoNTr1v1aL
@NoNTr1v1aL Жыл бұрын
Absolutely amazing video! Subscribed.
@xactxx
@xactxx Жыл бұрын
Thank you very much for your encouraging comment!
@msolec2000
@msolec2000 Жыл бұрын
Nice. I had this book by R. Smullyan that explained this with birds. It was cool. This is a very explanation of the subject. Trying to find out how to get [OR]xy, [AND]xy. And maybe others, but with either of those you get NOR or NAND, and those are universal.
@xactxx
@xactxx Жыл бұрын
Yes, 'To Mock a Mockingbird and Other Logic Puzzles'. :) We tried to keep the same letters that Smullyan used. The only exception is the N combinator, which Smullyan simply leaves as KI. Otherwise all the other combinators have the same letter as in Smullyan's book. Regarding AND and OR, do you want a hint? :)
@msolec2000
@msolec2000 Жыл бұрын
@@xactxx I think it would be something like [First]xy[True]y for OR and [First]xyy[False] for AND. I think. And yes, that's the book I was talking about! :)
@xactxx
@xactxx Жыл бұрын
@@msolec2000 Here's a hint. [And]xy = xy[false]. Now try [Or] yourself. :) Also, try to 'compile' this [And] definition to obtain a combinator expression for it.
@klevisimeri607
@klevisimeri607 Жыл бұрын
We love it!
@itsmeagain1415
@itsmeagain1415 Жыл бұрын
I can realise how much you have put your hearts and souls in this video, truly a hidden gem that should get millions of people to watch!
@xactxx
@xactxx Жыл бұрын
We are humbled by this comment. Thank you very much for your appreciation!
@lexinwonderland5741
@lexinwonderland5741 Жыл бұрын
yeah, this went WAY over my head, but it gets an upvote anyway cuz it's awesome and obviously brilliant. great job on the video!
@xactxx
@xactxx Жыл бұрын
Thank you!
@user-tx4wj7qk4t
@user-tx4wj7qk4t 2 ай бұрын
That's because it's explained in the most complicated way possible. If he just wrote the lambda calculus notation it would be really simple
@Asterism_Desmos
@Asterism_Desmos Жыл бұрын
I am your 250th subscriber
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
Excellent! Do you have something new in the works? In one of the comments you mention "to mock a mockingbird" which is the classic book about combinators, but your presentation seems more modern and focused on the application to computation. It would be nice to know what references you used... it would be also nice to see how this compares to the lambda calculus, or how combinators and lambda calculus are the same... Also the argument is that any computation can be done using combinatory logic but the proof is not obvious (although the result is believable as yet one more example of the church turing thesis)... the fact that one can achieve turing completeness with such simple systems make one wonder whether this has something to do with the basic structures of life. Perhaps the laws of physics build simple systems like combinators, which evolve into what we call life...
@sabriath
@sabriath Жыл бұрын
That bonus bit reminds me of whitespace programming language
@uku4171
@uku4171 6 ай бұрын
I wonder what was in Schõnfinkel's lost texts
@skilz8098
@skilz8098 Жыл бұрын
Next up, an FFT and its Inverse Algorithm using only Combinatory Logic followed by The Wave Collapse Function.
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
hahaha... this brings an important point that is often left out in these type of results... many things are turing complete but computer languages are not only about producing computations but about making it easy for humans to express those computations... combiators are interesting for what they say about the nature of formal languages but they are probably not going to replace any real world programming language any time soon (though functional programming is valid and useful but even pure programming language go beyond implementing combinators)
@user-of9sr8bm9i
@user-of9sr8bm9i Жыл бұрын
But why a slash in the iota combinator only mode?
@MaltaMathematicalSociety
@MaltaMathematicalSociety Жыл бұрын
Good catch! Unfortunately that ioughtta be a typo...
@xactxx
@xactxx Жыл бұрын
Good to see that someone caught the mistake! :)
@MagicGonads
@MagicGonads 3 ай бұрын
Since you only need one symbol (iota) coupled with two grouping symbols (parentheses), you can represent a program using instructions that only take two bits each, with a value left over. Then if you want to support side-effects, do a UTF inspired 'if the chunk is 11 then load another chunk to extend the code' for whatever side effects you wanna add to your architecture/CPU. Though maybe we need a proper padding instruction (usually nop or int 3)
@eugenemosh3658
@eugenemosh3658 10 ай бұрын
27:43 -- impressive!! Only two symbols and () and Fibonachi encoded!
@yuzhang1366
@yuzhang1366 8 күн бұрын
7:56 should be C=S(BBS)(KK)
@imrematajz1624
@imrematajz1624 6 ай бұрын
Is this a roundabout way to introduce Lambda calculus?
@synaestheziac
@synaestheziac Жыл бұрын
0:52 did I see a subliminal Hilbert in there?
@quentincarver926
@quentincarver926 Жыл бұрын
might've been cut content. Hilbert proof systems have a correspondence with combinatory logic (curry-howard correspondance)
@theunknown4834
@theunknown4834 Жыл бұрын
How do you represent decimals in this form?
@xactxx
@xactxx Жыл бұрын
One would first need to represent integers (for example, as a pair of naturals with appropriately defined operations), then move on to define rationals, as pairs of integers. Then reals could be defined using infinite lists. This video did not define lists (we didn't need them for our Fibonacci program) but lists may also be defined in terms of combinatory logic.
@theunknown4834
@theunknown4834 Жыл бұрын
@@xactxx This topic is scary lol, still won't stop me from writing it in python
@xactxx
@xactxx Жыл бұрын
@@theunknown4834 I have a working implementation of the constructs in this video. It works, though very slowly, as is expected. But it works.
@bartvanpelt588
@bartvanpelt588 Жыл бұрын
@@theunknown4834 writing this in python seems like a nice challenge, if you want a language that can evaluate these combinators with less of a hassle (and builtin lazy evaluation!) I would highly recommend Haskell.
@mching4473
@mching4473 Жыл бұрын
Love this video, esp how you keep the properties at the bottom. Feels like a power up for understanding @code_report's APL solution videos.
@DerMathematicker
@DerMathematicker 4 ай бұрын
8:58 Is it realy [f]_x -> K or is it [f]_x -> kf?
@antoniolewis1016
@antoniolewis1016 Жыл бұрын
It would have helped a lot if you had parentheses to see which things the K and the I were acting on. It's very confusing.
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@antoniolewis1016 Same opinion here... it would have been nice if they had mentioned that combinators associate by default to the left, so KIxy is shortcut for ((KI)x)y
@johnchessant3012
@johnchessant3012 Жыл бұрын
interesting
@alexanderfarrugia9299
@alexanderfarrugia9299 Жыл бұрын
Thank you for your encouraging comment!
@theunknown4834
@theunknown4834 Жыл бұрын
Is there any way to discuss this? (discord, reddit etc.)
@alexanderfarrugia9299
@alexanderfarrugia9299 Жыл бұрын
Are you in the SoMe2 Discord? We could discuss there.
@theunknown4834
@theunknown4834 Жыл бұрын
​@@alexanderfarrugia9299 Yes, will be trying to contact you soon
@alexanderfarrugia9299
@alexanderfarrugia9299 Жыл бұрын
@@theunknown4834 I am farrugiamaths there. Message me even if I'm offline and I'll get back to you when I am. :)
@theunknown4834
@theunknown4834 Жыл бұрын
@@alexanderfarrugia9299 Already did :>
@theunknown4834
@theunknown4834 Жыл бұрын
@@alexanderfarrugia9299 I finished my implementation and uploaded it on GitHub and sent it to you :)
@MrRyanroberson1
@MrRyanroberson1 Жыл бұрын
the real challenge: can you make a proper combinator (a combinator which could be written as a function of N arguments that returns a pure juxtaposition of those arguments) that can compute everything? i'm pretty sure it's impossible. It has been proven that there exists a proper combinator X such that X and I=SKK together can compute everything, but one truly universal proper combinator has yet to be found.
@olekkatan6614
@olekkatan6614 Жыл бұрын
24:32 there is an odd number of parentheses
@user-tk2jy8xr8b
@user-tk2jy8xr8b Жыл бұрын
Unfortunate naming for C params, btw, better use Cfxy -> fyx, otherwise the second arg is expected to be used as a function (f, g, and h are usual names for functions, whereas x, y, and z - for values (I know functions are values, it's about their intended usage, not the type)), which is not the case
@xactxx
@xactxx Жыл бұрын
g could be a function though. Nothing wrong with being so.
@user-tk2jy8xr8b
@user-tk2jy8xr8b Жыл бұрын
@@xactxx everything is a function in combinator logic. The naming is about the intended usage
@xactxx
@xactxx Жыл бұрын
@@user-tk2jy8xr8b and what is the intended usage?
@user-tk2jy8xr8b
@user-tk2jy8xr8b Жыл бұрын
@@xactxx to be applied to anything or not on the right-hand side of the definition
@xactxx
@xactxx Жыл бұрын
@@user-tk2jy8xr8b fair enough. The reason why we used fgx is for consistency with the variables used for B and S. Essentially, B and C are the two halves of S, and using the same variables for S, B and C drives home this point.
@unixux
@unixux 3 ай бұрын
KIxy should be K[Ix,y] = K(x,y) = x ? Or KIxy=(KIx)y=Iy ?
@yuzhang1366
@yuzhang1366 8 күн бұрын
KIxy=(KIx)y=Iy=y
@samernoureddine
@samernoureddine Жыл бұрын
I am not sure I follow why you can write any program using S and K. Why is this true?
@lukewatson8848
@lukewatson8848 6 ай бұрын
It is because other combinators can be expressed in terms of S and K alone, for example: I = SKK (1) B = S(KS)K C = S(BBS)KK where C can be written using (1) as C = S((S(KS)K)(S(KS)K)S)KK and so on...
@r75shell
@r75shell Жыл бұрын
At least first 14 minutes doesn't tell how to verify that stuff works. For example 1:51 in video says KIxy reduces to y. Can I verify it? Or is it just by definition? Why it's not K(Ix)y -> Kxy -> x? At time 3:00 "we have written program" what it does? "This is how combinators logic avoids variables altogether". We write x, y everywhere, isn't it variables? "Our program is simply string of combinators" Well, isn't Ix reduces into x? Isn't program "x" then? Summary: in my opinion this video is very.... very confusing.
@mching4473
@mching4473 Жыл бұрын
Not an expert in this either but it's a mix of both. The first few stuff tells us how notations work. Kinda like the PEMDAS of combinatory logic. So if you have KIxy, it is a signal for you to evaluate it as K(I, x) then y K(I, x) -> I. Then I(y) since I takes in one argument.
@padawanrl8834
@padawanrl8834 6 ай бұрын
Agree. I don't get how KIxy reduces to Iy. It would help if precedence/order is shown. My initial understanding was: KIxy K(Ix, y) K(x, y) y But apparently it should be Iy?
@DeclanMBrennan
@DeclanMBrennan 7 ай бұрын
So iota is Turing complete? Mind blown. 🙂
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@DeclanMBrennan The iota combiator together with the machinery to interpret it is turing complete (this is like saying that not only you need a program but also a compiler that runs the program)... that sounds mind blowing but then you realize that there are a bunch of things that are turing complete...I believe that so far, the smallest turing complete machine Wolfram 2-state 3-symbol turing machine... this is interesting because it kind of hints that we can get that type of computation with very simple systems, which kind of leads to how intelligence and life are plausible (the argument is that something as simple as the wolfram 2-state 3 symbol machine is simple enough that it could have happened by chance without any intelligent designer)
@DeclanMBrennan
@DeclanMBrennan 6 ай бұрын
@@academyofuselessideasI was using "Turing complete" in the sense of a "Turing complete language" but that's a fair point. Thanks for mentioning the Wolfram TM- looking forward to reading up on it. I believe Conway's Game of Life may be Turing complete as well and somebody with way too much free time made hardware within Game of Life to execute its own Game of Life - a cool example of a simulation within a simulation.
@DeclanMBrennan
@DeclanMBrennan 6 ай бұрын
@@academyofuselessideas I just had a quick look at your wonderful channel which I didn't know existed. I feel like a kid in a mathematical sweet shop. 🙂
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@@DeclanMBrennan Game of life inside game of life sounds pretty cool... The observation that there are many simple turing complete machines is also part of Wolfram's argument that all physics are automatas (kind of like what we observe is some sort of emergent phenomena caused by very tiny automatas)... I like the philosophy behind some of those ideas but I don't know enough about them to give an informed opinion though
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@@DeclanMBrennan I am glad to have you on board!
@doc7115
@doc7115 2 күн бұрын
🤯🤯🤯🤯🤯🤯
@theunknown4834
@theunknown4834 Жыл бұрын
this video is pretty good, however, I do not think the software used here is helping in understanding as it scrambles all the lines
@epgui
@epgui 6 ай бұрын
You lost me around the two-minute mark. If Kxy -> x and Ix -> x, doesn't KIxy -> Kxy -> x ?
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@epgui Part of the confusion arises because they didn't explain how combinators associate... so, it is not clear if one should think of KIxy as (((KI)x)y) or as K(I(x(y)). The way you associate things in this context matters... When working with combinators, the convention is to associate to the left, so Kxy->x would be more pedantically be written as ((Kx)y)->x... Based on that observation KIxy = (((KI)x)y) -> Iy -> y... A fun book about this is "to mock a mockingbird" by Smullyan... they mention that book in one of the comments... Working with combinators take some practice
@Bobby_101
@Bobby_101 5 ай бұрын
In simple words, the First symbol is applied first always (lazy evaluation). And since K takes the 2 objects in front of it and becomes the first one, ignoring anything else (KIx -> I)..So KIxy -> Iy -> y.
@academyofuselessideas
@academyofuselessideas 5 ай бұрын
@@Bobby_101 Nice explanation!
@epgui
@epgui 5 ай бұрын
​@@Bobby_101 In other words, everything is implicitly left-associative, and symbols representing functions are treated the same way as symbols representing values? That seems a bit weird syntactically, but if that's the rule then that makes sense.
@Bobby_101
@Bobby_101 5 ай бұрын
​@@academyofuselessideas Thanks. @epgui Yah it's a bit odd at first, just roll with it to see what results it brings.
@samytamim2603
@samytamim2603 Жыл бұрын
honestly i feel dumb
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@samytamim2603 @samytamim2603 awww... that happens with some math explanations... in my experience, it is best not to think to much about the math that makes you feel dumb and instead focus on the math that you enjoy and understand... even professional mathematicians have no idea of what other mathematicians are doing in a different field... Combinators can be fun but they are somehow esoteric anyways... just do what you find fun!
@samytamim2603
@samytamim2603 6 ай бұрын
@@academyofuselessideas I actually got the Ahaaa moments, then got shocked knowing I was missing out these stuff. It was a bit sarcastic xD
@academyofuselessideas
@academyofuselessideas 6 ай бұрын
@@samytamim2603 now I feel dumb 🙃
@samytamim2603
@samytamim2603 6 ай бұрын
@@academyofuselessideas 😆
@malikwaddy6897
@malikwaddy6897 Жыл бұрын
The first 2 mins don't make sense at all
@buraianmath
@buraianmath 10 ай бұрын
same..
@cmilkau
@cmilkau 5 ай бұрын
You really only need S and K, which correspond to the two THEN axioms of intuitionistic logic. There is a straightforward way to turn any lambda into a combination of just these two, exploiting the special case I = SKK (Note that the other axioms of intuitionistic logic are just definitions of AND, OR, and FALSE.) If you want to know how, just keep replacing expressions like this: λx. fg →S (λx.f) (λx.g) λx. x → SKK λx. y → Ky Where x,y are variables and f,g are expressions.
How to unify logic & arithmetic
20:14
All Angles
Рет қаралды 44 М.
ШЕЛБИЛАР | bayGUYS
24:45
bayGUYS
Рет қаралды 480 М.
原来小女孩在求救#海贼王  #路飞
00:32
路飞与唐舞桐
Рет қаралды 46 МЛН
Introduction To Symbolic Dynamics #SoME2
18:09
SyllabusGames
Рет қаралды 25 М.
The Shadowy World of Umbral Calculus
15:01
Supware
Рет қаралды 118 М.
This Is the Calculus They Won't Teach You
30:17
A Well-Rested Dog
Рет қаралды 2,9 МЛН
Lambda Calculus - Computerphile
12:40
Computerphile
Рет қаралды 996 М.
A Sensible Introduction to Category Theory
26:20
Oliver Lugg
Рет қаралды 414 М.
Teleporting Ants & Dynamic Programming #SoME2
12:42
A Bit Wiser
Рет қаралды 165 М.
Мужчина ходит по облакам😱
0:18
Astronaut-Stories
Рет қаралды 6 МЛН
Фокусы оператора 😀 с канцелярской резинкой. Он в кадре.
0:41
Polinka_girla (Полинка и Оператор)
Рет қаралды 2,6 МЛН
Загадочная коробка!
0:36
ТРЕНДИ ШОРТС
Рет қаралды 7 МЛН
БАССЕЙН (смешное видео, юмор, приколы, поржать)
1:00
Натурал Альбертович
Рет қаралды 2,8 МЛН