Introduction to Lambda Calculus

Return to List of Lectures

Previous Lecture

• Questions?
• Lambda Calculus Basics
  • Section 1 of Rojas
    • Recursive definition of lambda expressions, E
      • E can be a name (base case)
      • Or λ name . E₁ (abstraction, defines nameless function)
      • Or E₁ E₂ (application)
    • Free and bound variables
      • Roughly, bound if λ in front
      • Bound variables are dummies, can be renamed
      • Aren’t things like λx.(λy.x(λx.x)) confusing?
      • Yes, like ∃x: ∃y: ( p(x,y) and ∃x: q(y,x) )
      • Confusing uses are possible, so their meaning has to be clear
    • Free if not bound
  • Examples
    • Beta-Reduce...
      • (λx.(x λy.y)) z
        • = [z/x] (x λy.y) = z (λy.y)
      • (λx.((λy.y)x)) z
        • = (λy.y)z
        • = z
      • (λx.xx) ( (λy.(λz.y)) w )
        • = (λx.xx) (λz.w)
        • = (λz.w)(λz.w)
        • = w
      • Or
        • = ( (λy.(λz.y)) w ) ( (λy.(λz.y)) w )
        • = (λz.w) ( (λy.(λz.y)) w )
        • = w
    • Church-Rosser property: order of reduction doesn’t matter
    • What does λy.(λz.y) do?
      • Makes a function that returns a specified value
      • You can do this in programming languages that have a decent implementation of functions
        

        >> % @ in Matlab is roughly equivalent to lambda
        >> @(y) @(z)y
        ans = 
            @(y)@(z)y
        >> f=ans
        f = 
            @(y)@(z)y
        >> g=f(3)
        g = 
            @(z)y
        >> g(0)
        ans =
             3
        >> g(1)
        ans =
             3
        >> g(-1001)
        ans =
             3
        >> always3 = g
        always3 = 
            @(z)y
        >> always3(17)
        ans =
             3
        >> always5 = f(5)
        >> always5 = 
            @(z)y
        >> always5(1)
        ans =
             5

• Next
  • Arithmetic in Lambda Calculus
  • Read section 2 of Rojas

Next Lecture