Bla blah. This is a collection of notes with lambda calculus stuff. The posts tend to come with a kind of live lambda calculus environment where we can run examples or play around.
The ones called “How/What do the lambdas?” are more introductiony than the others, with stuff about syntax and semantics and how the editors work and such.
Some numbery functions
How do the lambdas?
What do the lambdas?
Some booly functions
Pairs
Successor
A design pattern?
Also a lambda playground:
| ctrl+l inserts λ
| ctrl+d inserts ≜
| ctrl+enter does one step of evaluation or define/undefine
| ctrl+r rewrites stuff and replaces names defined elsewhere with their definitions
| shift+enter does lots of evaluation
| right-click and Show definitions to list the available definitions
| e.g.
| put cursor on line below and ctrl+enter
0 ≜ λf.λx.x
| put cursor on line below and ctrl+enter
S ≜ λn.λf.λx.f (n f x)
| put cursor on line below and ctrl+enter
2 ≜ S (S 0)
| put cursor on line below and ctrl+enter
+ ≜ λa.λb.a S b
| put cursor on line below and ctrl+enter
6 ≜ + 2 (+ 2 2)
| put cursor on line below and ctrl+r, then shift+enter
+ 6 6