CSE 130 Lecture Notes - Lecture 4: Lambda Calculus, Syntactic Sugar, Fixed-Point Combinator
16 views3 pages
19 Jan 2018
School
Department
Course
Professor
More Lambda Calculus
ƛy.ƛx.(((x x) (ƛz.y)) ƛw.w)
^ - first unmatched parentheses
Back to substitution:
(ƛx. (ƛa.x + a) 7) (a + 5)
→ (ƛa. (a + 5) + a) 7
→ 7 + 5 + 4
→ 19 → Wrong! (a is captured when it should NOT be)
Syntactic sugar: let x = e1 in e2 → (ƛx.e2) e1
Let x = a + 5 in let x = a + 5 in
Let a = 7 in → let a = 7 in
X + a (a + 5) + a
Fixing the Problem
1. Rename vars!
Let x = a + 5 in
Let a55 = 7 in → (a + 5) + a55
X + a55
Def: var x is bound to ƛx.(x+y)
- We can ALWAYS rename bound vars because they are within the scope and we have
FULL control over it
- Bound vars are just “placeholders”
-ƛx.(x+y) → a ƛz.(z+y)
- Avoids “capturing” vars when substituting
Can we rename y in ƛx.(x+y)? No - y could be defined somewhere else!
Intuition:
- sum(i = 55) ( sum(i n = 1 to 10) xi + yj )
Def: free variables - NOT bound by a ƛ
-is x free in ƛx.(x+y)? NO
-y is free
Compute the free vars of any term:
- FV(x) = { x }
- FV(ƛx.e) = FV(e) \ { x }
- FV(e1 e2) = FV(e1) ∪ FV(e2)
Def: Capture-avoiding substitution
-x[x:=e] = e
-y[x:=e] = y