RC25. A quick one on lambda multiplication
Daily dispatches from my 12 weeks at the Recurse Center in Summer 2023
Clearly I’m a sucker for pain, because today one of the things I did was work through more brain-bending lambda calculus. This is a short one, though, since I’m still depleted from last time.
My groupmate posted the following solution to multiplication in lambda calculus:
(define (mult a)
(lambda (b)
(lambda (f)
(lambda (x) ((a (b f)) x)))))
Just the usual mis-en-abyme of procedures nested to oblivion.
But this time I come equipped with a little confidence, so let’s start expanding to see how this works:
First, some “numbers” and an increment procedure:
(define (two f)
(lambda (f)
(lambda (x) (f (f x)))))
(define (three f)
(lambda (f)
(lambda (x) (f (f (f x))))))
(define (inc x) (+ x 1))
My plan now is to expand the mult
procedure one argument at a time:
; expand `(mult two)`
(mult two)
(lambda (b) (lambda (x) ((two (b f)) x)))
; expand `((mult two) three)`
((mult two) three)
(lambda (f) (lambda (x) ((two (three f)) x)))
; expand `(((mult two) three) inc)`
(((mult two) three) inc)
(lambda (x) ((two (three inc)) x))
(lambda (x) ((two (lambda (y) (inc (inc (inc y))))) x)) ; expansion of `(three inc)`
(lambda (x) ((lambda (z) ((inc (inc (inc (inc (inc (inc z)))))))) x)) ; expansion of `(two ...)`
(lambda (x) ((inc (inc (inc (inc (inc (inc x))))))
; expand `((((mult two) three) inc) 2)`
((((mult two) three) inc) 2)
((two (three inc)) 2)
((two (lambda (x) (inc (inc (inc x))))) 2)
((lambda (x) (inc (inc (inc (inc (inc (inc x))))))) 2)
(inc (inc (inc (inc (inc (inc 2))))))
=> 8 ; finally, an evaluation! Terra firma
After going through this series of expansions, it becomes a little more intuitive, for instance, ((mult two) three)
returns a procedure that applies a procedure f
to term x
three times, which it does two times. Hence, it applies f
to x
\(2 \cdot 3 = 6\) times.
And that’s about all I wanted to say about that.
Other things that came to pass
Weekend
- Wrote blog post about how my head exploded because of lambda calculus
- Put together a walkthrough of CTCI linked-listed problem
Monday/Yesterday (home with sick child but still got a few things done)
- got my memory system coded up for nand2tetris and started work on the CPU
- Paired more on bitwise ops (ostensibly this was a C-related project but we just did it in a Python REPL)
- unsuccessful squinted at binary and assembly language for hours trying to figure out why my nand2tetris CPU was failing.