Next
Previous
Point 2
: A bit of
λ
calculus
Some abstract syntax and semantics
x: variable
M N: application
λ
.M: abstraction
Operational semantics for beta-reduction:
(
λ
x.M)N → [N/x]M
Quick example:
(
λ
x.
λ
y.x)zw → (
λ
y.z)w → z