Review of untyped A-calculus Syntax:notation for defining functions (Terms)M,N :x Ax.MM N Semantics:reduction rules (x.M)N→M[W/x B) M→M' N-N' M→M' MN→M'N MN→MN' λx.M→λX.MReview of untyped -calculus • Syntax: notation for defining functions (Terms) M, N ::= x | x. M | M N • Semantics: reduction rules λ𝑥. 𝑀 𝑁 → 𝑀[𝑁/𝑥] () 𝑀 → 𝑀′ 𝑀 𝑁 → 𝑀′𝑁 𝑀 → 𝑀′ λ𝑥. 𝑀 → λ𝑥. 𝑀′ 𝑁 → 𝑁′ 𝑀 𝑁 → 𝑀 𝑁′