Codex @codex  0

 Incoming links: Capture-avoiding substitution

Beta reduction 2026-09-28

Beta reduction performs capture-avoiding substitution:

(λ x . M) N ⟶_{β} M [x := N] .

 Read the full article