Update, 2024-10-11: Man, this is a garbage post. I was trying to get my thoughts out, but I have next to no clue what I was doing and don’t really understand it. You want to learn about Lambda Calculus? Go anywhere else. Sorry. >.<
I’m playing around in Minetest, and I have an idea. In order to execute this idea, I’m going to need a simple programming language. Asking Google… implementing a simple programming language…
7 lines of code, 3 minutes: Implement a programming language from scratch
Sounds good! Ridiculously simple, fast, and gives us a fully usable language. (I would’ve understood brainfuck better..) Let’s see what this language looks like:
(λ v . e) anonymous function with argument v and returning e
(f v) call function f with argument v
(λ a . a) example: identity function (returns its argument)
And the scary one:
(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b))Seems okay until I get to understanding that last example. If you’re curious about the steps I went through before I finally figured it out, here are my notes. I’m gonna skip to the good part:
(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b))
two identity functions, let's name them I, & remove excess parenthesis
(λ f . (λ x . (f x))) I I
the syntax is still confusing me, let's make an "F" function
F(x) -> return (λ x . (f x))
F I I equivalent to ((F I) I)
substituting the function (identity) into our definition gives us
(λ x . (I x)) which..is actually the same as the identity function
I(I) ..it all comes to returning the identity function
λ x . xNow, at this point I’ve learned a few small tricks for my understanding, as well as how lambda calculus works in general.
Reduction
Solving a lambda calculus program is made of three (or 2.5) steps called reductions:
- η-conversion (eta): Replace equivalent functions with simpler forms (λ x . f x) -> f
- β-reduction (beta): Substitution (λ a . a) x -> x (essentially, THIS is solving it)
- α-conversion (alpha): Rename conflicting names (λ a . a b) (λ a . a) -> (λ a . a b) (λ c . c)
References
This is where my journey ends for now. I started studying lambda calculus because of a desire to implement a simple programming language, but this will likely not satisfy my needs..at least not in this form. (Note: All resources are archived using the services linked to on Archives & Sources.)
- Lambda calculus on Wikipedia
- What does (((λ f . (λ x . (f x))) (λ a . a)) (λ b . b)) mean? (literally googled this after solving it, because I couldn’t believe I spent hours solving for a series of identity functions)
- Lambda Calculus Reduction steps on Stack Overflow