# 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