Lambda Calculus Pt. 2

19 Feb 2017

Example of Free Variables

• x is free in E if:
  • Rule 1 (E = x) ? yes, since there is no meta variable for x
  • Rule 2 (E = λy.E1) ? yes, if y != x
  • Rule 3 (E = E1 E2) ? yes, if either E1 or E2 is free
    • x free in xλx.x ? Yes, x(λx.x) where x is free in E1
    • x free in (λx.xy)x ? Yes, since E2 is free
    • x free in λx.yx ? No, λx.(yx)

Combinators

An expression is a combinator if it doesn’t have any free variables

• λx.λy.xyx combinator ? yes (The function takes x and y as parameters and do xyx)
• λx.x ? yes
• λz.λy.xyz ? no, since y is free

Bound Variables

• If a variable is not free then it is Bound
  • Bound Rule 1: If x is free in E then it is bound by λx in λx.E
  • Bound Rule 2: If x is bound by λx in E then x is bound by same inner most λx in λz.E
    • Even if z == x
    • λx.λx.x
      • Which lambda expression binds x? inner most λx
  • Bound Rule 3: If x is bound by λx in E1 then E1 is tied by same abstraction λx in E1 E2 and E2 E1. Think it easy as it said.

Examples

• (λx.x(λy.xyzy)x)xy
  • (λx.x(λy.xyzy)x)xy
• (λx.λy.xy)(λz.xz)
  • (λx.λy.xy)(λz.xz)
• (λx.xλx.zx)
  • (λx.xλx.zx)

Equivalence

• What does it mean for two functions to be equivalent?
  • λy.y = λx.x ? Same functions
  • λx.xy = λy.yx ?
  • λx.x = λx.x ? Same functions

α-Equivalence

When two functions vary only by names of bound variables E1 = αE2

• λx.xλy.xyz
  • Can we rename x to foo? yes
  • Can we rename y to bar? yes
  • Can we rename y to x? no, since it creates bound variable & changes the existing semantics
  • Can we rename z to x? no, since it creates bound variable & changes the existing semantics

Renaming Operation

E{y/x} = renaming x to y

• x{y/x} = y
• z{y/x} = z, if x != z
• (E1 E2) {y/x} = (E1{y/x})(E2{y/x})
• (λx.E){y/x} = (λy.E{y/x})
• (λz.E){y/x} = (λz.E{y/x}), if x != z

Examples

• (λx.x){foo/x} = (λfoo.(x){foo/x}) = (λfoo.(foo))

• ((λx.x(λy.xyzy)x)xy){bar/x} = (λx.x(λy.xyzy)x){bar/x}(x){bar/x}(y){bar/x} … = (λbar.(x(λy.xyzy)x){bar/x}) bar y = (λbar.(bar(λy.(bar y z y))bar)) bar y

α-Equivalence

• For all expressions E and all variables y that do not occur in E
  • λx.E = αy.(E{y/x})
• λy.y = λx.x ? yes
• ((λx.x(λy.xyzy)x)xy) = ((λy.y(λz.yzwz)y)yx) ? no
• (λx.x(λy.xyzy)x) = (λy.y(λz.yzwz)y) ? no, bound variables can be different name, but you shouldn’t change free variable such as z as it will change semantics

Substituion

(λx.+x 1)x -> (+ 1 2)

• Can we use renaming? no
• We need another operator, called substitution, to replace a variable by a lambda expression
  • E[x->N], where E and N are lambda expressions and x is a name
• (+ x 1)[x->2] = (+ 2 1)
• (λx.+ x 1)[x->2] = (λx.+ x 1) Nothing to change since the varialbe is bound
• (λx.yx)[y->λz.xz] != (λx.(λz.xz)x) = (λw.(λz.xz)w) See CSE 340 11-25-15 Lecture: “Lambda Calculus Pt. 2”