Cheatsheet
A one-page reference for the λ-calculus and the visualizer.
Syntax
x | variable |
λx. M | abstraction (function of x) |
\x. M | same — ASCII alternative |
M N | application (left-associative) |
λx y z. M | = λx. λy. λz. M |
let x = e1 in e2 | = (λx. e2) e1 |
let x = e1; y = e2 in e3 | chained let |
# comment | line comment to end-of-line |
Reduction rules
| α (rename) |
λx. x ≡ λy. y |
| β (apply) |
(λx. M) N → M[x := N] |
| η (extensional) |
λx. f x ≡ f (if x not free in f) |
Strategies
| normal | leftmost-outermost first; finds normal form if it exists |
| applicative | arguments first; can loop where normal terminates |
| cbn | like normal but stops at λ-bodies |
| cbv | like applicative but stops at λ-bodies |
Combinators
I | λx. x | identity |
K | λx y. x | constant (= true) |
S | λx y z. x z (y z) | "apply, then weave" |
B | λf g x. f (g x) | compose |
C | λf x y. f y x | flip args |
W | λf x. f x x | duplicate arg |
Y | λf. (λx. f (x x)) (λx. f (x x)) | fixed point (lazy) |
Z | λf. (λx. f (λv. x x v)) (λx. f (λv. x x v)) | fixed point (strict) |
ω | (λx. x x) (λx. x x) | diverges |
Booleans
true | λx y. x |
false | λx y. y |
if | λp a b. p a b |
not | λb. b false true |
and | λp q. p q p |
or | λp q. p p q |
xor | λp q. p (not q) q |
Pairs
pair | λx y s. s x y |
fst | λp. p true |
snd | λp. p false |
Church numerals
0 | λf x. x |
1 | λf x. f x |
n | λf x. fⁿ x (apply f n times) |
succ | λn f x. f (n f x) |
plus | λm n f x. m f (n f x) |
mult | λm n f. m (n f) |
pow | λm n. n m (yes, just n m) |
pred | λn f x. n (λg h. h (g f)) (λu. x) (λu. u) |
iszero | λn. n (λx. false) true |
sub | λm n. n pred m |
leq | λm n. iszero (sub m n) |
eq | λm n. and (leq m n) (leq n m) |
Lists (Church-encoded right fold)
A list folds with a cons-style function c over a base case n:
[x₁, x₂, x₃] = λc n. c x₁ (c x₂ (c x₃ n))
nil | λc n. n |
cons | λh t c n. c h (t c n) |
isnil | λl. l (λh t. false) true |
length | λl. l (λh r. succ r) 0 |
head | λl. l (λh t. h) nil |
map | λf l. l (λh t. cons (f h) t) nil |
append | λxs ys. xs cons ys |
sum | λl. l plus 0 |
Scott-encoded lists
Scott encoding pattern-matches directly: scons h t = λn c. c h t.
Easier head/tail but no fold-by-default.
snil | λn c. n |
scons | λh t n c. c h t |
shead | λl. l nil (λh t. h) |
stail | λl. l snil (λh t. t) |
Binary Lambda Calculus
Tromp's tiny binary encoding of closed λ-terms (de Bruijn indices):
00 M | λ M (abstraction) |
01 M N | application |
1ⁿ⁺¹ 0 | variable with de Bruijn index n |
E.g. I = λx. x = 0010.
Toggle BLC in the visualizer to see any term as a bit string.
Visualizer shortcuts
| Ctrl+Enter | draw current expression |
| Tab | accept autocomplete |
| Ctrl+F | find / replace |
| ? | show all keyboard shortcuts |
| Esc | close popup / exit fullscreen / exit presentation |
Presentation mode
| Space / → | step |
| ← | step back |
| R | run |
| P | pause / resume |
| 0 | reset |
| F | fit to viewport |
| H | hide HUD |
Tree mode
| Space / → | step the tree |
| R | run / pause |
| S | reset (re-parse and replay) |
| F | fit tree to view |
| M | toggle minimap |