Exp u ::= | x | variable |
λx.u | abstraction | |
u1 u2 | application |
replace references to parameter with argument
(λa.λb.λc.c a b) foo bar quux
(λb.λc.c foo b) bar quux
(λc.c foo bar) quux
quux foo bar
this slide is wide :)
0 is λf.λx.x
1 is λf.λx.f x
2 is λf.λx.f (f x)
3 is λf.λx.f (f (f x))
5 is λf.λx.f (f (f (f (f x))))
and so on
+ is λa.λb.λf.λx.a f (b f x)
(f applied a times to f applied b times to x)
* is λa.λb.λf.λx.a (b f) x
(f applied b times a times to x)
λy.(λx.λy.x) y
λy.(λx.λy.x) y
λy.λy.y
oh no
λy.(λx.λy.x) y
rename inner y before reducing
Exp u ::= | n | variable |
λu | abstraction | |
u1 u2 | application |
λz.(λy.y (λx. x)) (λx.z x)
0 is λλ1
1 is λλ2 1
2 is λλ2 (2 1)
3 is λλ2 (2 (2 1))
5 is λλ2 (2 (2 (2 (2 1))))
and so on
+ is λλλλ4 2 (3 2 1)
(um)
* is λλλλ4 (3 2) 1
(uh)
+ is λa.λb.λf.λx.a f (b f x)
(f applied a times to f applied b times to x)
* is λa.λb.λf.λx.a (b f) x
(f applied b times a times to x)
(λλλλ4 2 (3 2 1)) (λλ2 (2 1)) (λλ2 (2 (2 1)))
(λλλ(λλ2 (2 1)) 2 (3 2 1)) (λλ2 (2 (2 1)))
λλ(λλ2 (2 1)) 2 ((λλ2 (2 (2 1))) 2 1)
λλ(λ3 (3 1)) ((λλ2 (2 (2 1))) 2 1)
λλ2 (2 ((λλ2 (2 (2 1))) 2 1))
λλ2 (2 ((λ3 (3 (3 1))) 1))
λλ2 (2 (2 (2 (2 1))))
(λλλλ4 (3 2) 1) (λλ2 (2 1)) (λλ2 (2 (2 1)))
(λλλ(λλ2 (2 1)) (3 2) 1) (λλ2 (2 (2 1)))
λλ(λλ2 (2 1)) ((λλ2 (2 (2 1))) 2) 1
λλ(λ(λλ2 (2 (2 1))) 3 ((λλ2 (2 (2 1))) 3 1)) 1
λλ(λλ2 (2 (2 1))) 2 ((λλ2 (2 (2 1))) 2 1)
λλ(λ3 (3 (3 1))) ((λλ2 (2 (2 1))) 2 1)
λλ2 (2 (2 ((λλ2 (2 (2 1))) 2 1)))
λλ2 (2 (2 ((λ3 (3 (3 1))) 1)))
λλ2 (2 (2 (2 (2 (2 1)))))
λy.(λx.λy.x) y
λ(λλ2) 1
λ(λλ2) 1
λλ2
Exp u ::= | boop b | variable |
beep u | abstraction | |
pling u1 u2 | application |
Boops b ::= | bap | bap |
boop b | boop |
nice
0 is beep beep boop bap
1 is beep beep pling boop boop bap boop bap
2 is beep beep pling boop boop bap pling boop boop bap boop bap
3 is beep beep pling boop boop bap pling boop boop bap pling boop boop bap boop bap
5 is beep beep pling boop boop bap pling boop boop bap pling boop boop bap pling boop boop bap pling boop boop bap boop bap
and so on
+ is beep beep beep beep pling pling boop boop boop boop bap boop boop bap pling pling boop boop boop bap boop boop bap boop bap
* is beep beep beep beep pling pling boop boop boop boop bap pling boop boop boop bap boop boop bap boop bap
pling pling beep beep beep beep pling pling boop boop boop boop bap boop boop bap pling pling boop boop boop bap boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap pling boop boop bap boop bap
we can try
for keyboard: a = beep, s = boop d = bap, f = pling, backspace = undo, space = "next"
with tree
lambdatree!
more lambdaer
so uh what else?
I mean, there's fish?
Einar always has some fish
maybe more legible
omega!