CSE 130 Lecture Notes - Lecture 4: Lambda Calculus, Syntactic Sugar, Fixed-Point Combinator

16 views3 pages
19 Jan 2018
School
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
Unlock document

This preview shows page 1 of the document.
Unlock all 3 pages and 3 million more documents.

Already have an account? Log in

Get OneClass Notes+

Unlimited access to class notes and textbook notes.

YearlyBest Value
75% OFF
$8 USD/m
Monthly
$30 USD/m
You will be charged $96 USD upfront and auto renewed at the end of each cycle. You may cancel anytime under Payment Settings. For more information, see our Terms and Privacy.
Payments are encrypted using 256-bit SSL. Powered by Stripe.