λ-calculus quick reference

λ-calculus quick reference#

How to use this page

Keep it open in a tab next to the Lambda Lab. Every entry has a lab command you can paste. If a command is new to you, help <command> in the lab explains it with examples.

Syntax and reading conventions#

\[ t, u ::= x \;\mid\; \lam x.\,t \;\mid\; t\,u \]

Convention	Meaning	So this…	…reads as
Application associates left	\(f\,x\,y = (f\,x)\,y\)	`f x y`	`(f x) y`
λ-body extends right	\(\lam x.\,x\,y = \lam x.\,(x\,y)\)	`\x. x y`	`λx. (x y)` — not `(λx. x) y`
Nested λ collapse	\(\lam x.\lam y.\,t = \lam x\,y.\,t\)	`\x y. t`	`λx. λy. t`

Lab: lam \x y. x (y z) — parse anything and see its free variables before you reduce it.

The three conversions#

Rule	Statement	Side condition	Lab command
α (renaming)	\(\lam x.\,t \;\equiv_\alpha\; \lam y.\,t[x{:=}y]\)	\(y \notin \mathrm{FV}(t)\)	`alpha \x. x = \y. y`
β (computation)	\((\lam x.\,t)\,u \;\betared\; t[x{:=}u]\)	substitution must avoid capture	`reduce (\x. x x) (\y. y)`
η (extensionality)	\(\lam x.\,t\,x \;\to_\eta\; t\)	\(x \notin \mathrm{FV}(t)\)	`eta \x. f x`

A term with no β-redex is a β-normal form; by Church–Rosser it is unique up to α.
Normal order (leftmost-outermost, what reduce shows — highlighted) finds a normal form whenever one exists.
\(\Omega = (\lam x.\,x\,x)(\lam x.\,x\,x)\) has no normal form; the lab reports its limit honestly.

The capture trap — the one substitution mistake everyone makes once

\((\lam y.\,x)[x{:=}y] \ne \lam y.\,y\). The incoming free \(y\) would be captured. Rename first: \(\lam y.\,x \equiv_\alpha \lam y'.\,x\), then substitute: \(\lam y'.\,y\) — a constant function, not the identity. When in doubt: debruijn the term — nameless form makes capture impossible to miss.

Church encodings#

Concept	Definition	Try it
`TRUE`	\(\lam t\,f.\,t\)	`church TRUE`
`FALSE`	\(\lam t\,f.\,f\) — the same term as `0`	`decode FALSE`
`IF`	\(\lam b\,t\,f.\,b\,t\,f\)	`reduce IF TRUE a b`
`AND` / `OR` / `NOT`	\(\lam p\,q.\,p\,q\,p\) · \(\lam p\,q.\,p\,p\,q\) · \(\lam p.\,p\,\mathtt{FALSE}\,\mathtt{TRUE}\)	`equiv NAND TRUE TRUE = NOT TRUE`
`PAIR` / `FST` / `SND`	\(\lam a\,b\,f.\,f\,a\,b\) · \(\lam p.\,p\,\mathtt{TRUE}\) · \(\lam p.\,p\,\mathtt{FALSE}\)	`nf FST (PAIR a b)`
numeral \(\overline{n}\)	\(\lam f\,x.\,f^{\,n}\,x\)	`church 3` · `peano 3`
`SUCC`	\(\lam n\,f\,x.\,f\,(n\,f\,x)\)	`nf SUCC 2`
`PLUS` / `MULT`	\(\lam m\,n\,f\,x.\,m\,f\,(n\,f\,x)\) · \(\lam m\,n\,f.\,m\,(n\,f)\)	`nf PLUS 2 3`
`POW` (η-long)	\(\lam m\,n\,f\,x.\,n\,m\,f\,x\)	`nf POW 2 0` → `1`
`PRED` (Kleene)	\(\lam n\,f\,x.\,n\,(\lam g\,h.\,h\,(g\,f))\,(\lam u.\,x)\,(\lam u.\,u)\)	`nf PRED 3`
`ISZERO` / `LEQ` / `EQ`	via `PRED` and `SUB`	`nf EQ 2 2`

Build your own: let COMPOSE = \f g x. f (g x) — then nf COMPOSE SUCC SUCC 1. List with defs.

Combinators#

Name	Term	Fact	Try it
I	\(\lam x.\,x\)	identity; principal type \(\alpha\to\alpha\)	`ch term \x. x`
K	\(\lam x\,y.\,x\)	constant; type \(\alpha\to\beta\to\alpha\)	`ch term \x. \y. x`
S	\(\lam f\,g\,x.\,f\,x\,(g\,x)\)	with K generates everything; its type is a tautology	`ch term \f. \g. \x. f x (g x)`
Y	\(\lam f.(\lam x.f(x\,x))(\lam x.f(x\,x))\)	\(Y f \reduces f\,(Y f)\) — recursion from nothing	`church Y`
Ω	\((\lam x.\,x\,x)(\lam x.\,x\,x)\)	no normal form	`reduce OMEGA`

The typed layer at a glance#

Typing judgment \(\Gamma \proves t : A\); STLC rules: variable, abstraction (→-intro), application (→-elim). Well-typed ⇒ strongly normalizing ⇒ Y and Ω are untypable.
Principal type = the most general simple type; the lab’s ch term <t> runs Algorithm W.
Inhabitation = provability (intuitionistic, implicational): ch type (P -> Q) -> P -> P finds a witness; ch type ((P -> Q) -> P) -> P reports Peirce uninhabited.

Curry–Howard in one table#

Logic	Type	Proof term	Lab
\(A \To B\)	function	λ-abstraction	`prove P -> Q -> P`
\(A \land B\)	product	pair	— (implicational builder)
\(A \lor B\)	sum	tagged injection	see Lecture 3
\(\bot\)	empty type	(no intro)	`ch type P -> Q` (uninhabited)
proof normalization	β-reduction	`reduce` on the proof term	`qed` then `reduce` it

The full loop: prove (P -> Q) -> P -> Q → intro f → intro p → apply f → exact p → qed prints the λ-term and its principal type. That term is your proof.

Lab commands by intent#

I want to…	Command
watch a computation, redex by redex	`reduce <t>` (or just type the term)
get the answer only	`nf <t>` · `decode <t>`
see lazy evaluation stop early	`whnf <t>`
check “are these the same?”	`alpha <t> = <u>` (spelling) · `equiv <t> = <u>` (value)
understand a binder puzzle	`debruijn <t>` · `alligators <t>`
apply extensionality	`eta <t>`
name my own construction	`let NAME = <t>` · `defs`
infer / inhabit types	`ch term <t>` · `ch type <T>`
prove a proposition interactively	`prove <prop>` … `qed`
be taught step by step	`tutorial` · `tour` · `quiz`
look something up	`kb <topic>` · `kb search <text>` · `help <command>`
jump to real Lean	`lean <name>` → Live Lean link

Top five mistakes (all fixable in one command)#

Reading \x. x y as (λx. x) y. The body extends right. Check: lam \x. x y.
Substituting into a binder that captures. See the warning box above; check with debruijn.
Thinking alpha computes. It only renames. “Same value” is equiv.
Expecting FALSE ≠ 0. Untyped Church encoding makes them the same term: decode FALSE.
Expecting every term to finish. reduce OMEGA — divergence is a feature, and the lab says so honestly instead of freezing.