CSE 130 Lecture Notes - Lecture 4: Lambda Calculus, Syntactic Sugar, Fixed-Point Combinator
19 Jan 2018
School
Department
Course
Professor
Document Summary
Back to substitution: ( x. ( a. x + a) 7) (a + 5) ( a. (a + 5) + a) 7. 19 wrong! (a is captured when it should not be) Syntactic sugar: let x = e1 in e2 ( x. e2) e1. Def: var x is bound to x. (x+y) (a + 5) + a55 let x = a + 5 in let a = 7 in (a + 5) + a. We can always rename bound vars because they are within the scope and we have. No - y could be defined somewhere else! Intuition: sum(i = 55) ( sum( i n = 1 to 10) x i + y j ) Def: free variables - not bound by a . ( x. e1)[x := e] = x. e1 x is bound! E. e1 5 + 7 => e1 not the right syntax! X. 5 + 7 wrong except for y fv(e2) ( y. e1)[x := e2] = y. (e1[x := e2] )
