Next Previous

Point 2: A bit of λ calculus

---

Some abstract syntax and semantics
1. x: variable
2. M N: application
3. λ.M: abstraction
Operational semantics for beta-reduction:
(λx.M)N → [N/x]M Quick example: (λx. λy.x)zw → (λy.z)w → z