Formal definitions about free and bound variables Recall M,n: =X nX.M MN fVM: the set of free variables in m x is a free variable in M":X E fv(M) ·“ x is a bound variable in m":? a-equivalence: Ax. M=ny. 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: =X XM 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 reductⅰon · Basic rule isβB- reduction (入x.M)N→>M[N/×]( Substitution) Repeatedly apply reduction rule to any sub-term Example (λf.X.f(fx)(y.y+1)5 →>(x(y+1)(x.y+1x)5 →>(x、(y+1)(x+1)5 →>(入X.(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
Substitutⅰon MIN/x]: replace x by n in m Defined by induction on terms X[Nx]≡N yNx]≡y (MPN×]≡(M[N/x])(PN/×] (λxM)N/x]≡AXM( Only replace free variables! (yM)[Nx]≡? 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:(λ.X-y){/y] Substitute "blindly: 2Xx-X Problem: unintended name capture! Solution rename bound variables before substitution (xx-y)[X/y (2z. 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