Formal definitions about free and bound variables ·Recall M,N:=x|入x.M|MN fv(M):the set of free variables in M 。"x is a free variable in Mi":x∈fv(M) 。“x is a bound variable in M":? a-equivalence:x.M=Ay.(M[y/x] where y fresh Substitution(defined later)
Formal definitions about free and bound variables • Recall M, N ::= x | x. M | M N • fv(M): the set of free variables in M • “x is a free variable in M”: x fv(M) • “x is a bound variable in M”: ? • -equivalence: x. M = y. M[y/x], where y fresh Substitution (defined later)
Main points till now Syntax:notation for defining functions (Terms)M,N ::xx.M MN Next:semantics (reduction rules)
Main points till now • Syntax: notation for defining functions (Terms) M, N ::= x | x. M | M N • Next: semantics (reduction rules)
Overview of reduction Basic rule is B-reduction (x.M)N→M[N/X] (Substitution) Repeatedly apply reduction rule to any sub-term Example (2f.2x.f(fx)y.y+1)5 →(2x.(y.y+1)(2y.y+1x)5 →(x.(2y.y+1)(+1)5 →(2x.(x+1)+1)5 →5+1+1→7
Overview of reduction • Basic rule is -reduction (x. M) N → M[N/x] (Substitution) • Repeatedly apply reduction rule to any sub-term Example (f. x. f (f x)) (y. y+1) 5 → (x. (y. y+1) ((y. y+1) x)) 5 → (x. (y. y+1) (x+1)) 5 → (x. (x+1)+1) 5 → 5+1+1 → 7
Substitution M[N/x]:replace x by N in M Defined by induction on terms x[N/X]≡N y[N/x]y (M P)[N/x](M[N/x])(P[N/x]) (入x.M)[N/x]≡入x.M(Only replace free variables) (y.M)[N/X灯]≡？ Because names of bound variables do not matter
Substitution • M[N/x]: replace x by N in M • Defined by induction on terms x[N/x] N y[N/x] y (M P)[N/x] (M[N/x]) (P[N/x]) (x.M)[N/x] x.M (Only replace free variables!) (y.M)[N/x] ? Because names of bound variables do not matter
Substitution-avoid name capture Example:(7x.x-y)[x/y] Substitute“blindly":入x.x-x Problem:unintended name capture!! Solution:rename bound variables before substitution (2x.x-y)[x/y] =(入z.z-y)[x/y] =入z.Z-X
Substitution – avoid name capture • Example : (x. x - y)[x/y] Substitute “blindly”: x. x - x Problem: unintended name capture!! Solution: rename bound variables before substitution (x. x - y)[x/y] = (z. z - y)[x/y] = z. z - x