Results 1 to 4 of 4

Math Help - Lambda calculus

  1. #1
    Newbie
    Joined
    Oct 2007
    Posts
    14

    Lambda calculus

    Hey, not sure if this is even a good website to pose this question, but I thought I'd try it out.

    I'm trying to teach myself some programming language principles by going through various texts/problem sets I find online about lambda calculus. Haven't gotten too far and I'm still trying to work the whole thing out. One statement I'm confused by is this:
    If we assume λy.λx.x = λy.λx.yx then we can say that any two lambda terms are equal.

    I'm sort of scratching my head on why this is true. Any explanations or leading statements would be much appreciated.

    Thanks!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Newbie
    Joined
    Oct 2007
    Posts
    14
    Here is my current idea:

    Take two λ-terms: A,B

    (λy.λx.x)AB = B
    (λy.λx.yx)AB = AB

    Under our assumption B = AB, thus A is the identity function.

    (λy.λx.x)BA = A
    (λy.λx.yx)BA = BA

    Under our assumption A = BA, thus B is the identity function.

    Thus A = B.

    Does this proof sound reasonable? Is the identity function unique?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Oct 2007
    Posts
    14
    But any identity function must be unique, right?

    Let I, I' be identity functions in λ-calculus.

    II' = I
    II' = I'

    Thus I = I'

    Does this work in λ-calculus? Does anyone know?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Newbie
    Joined
    May 2008
    Posts
    16
    I'm assuming beta-equivalence is used here, so we have the reduction rule
    {M =_\beta M'}\over{MN =_\beta M'N}

    We can do
    (\lambda y.\lambda x.x)(\lambda x.M)N =_\beta N
    (\lambda y.\lambda x.yx)(\lambda x.M)N =_\beta M
    ergo M =_\beta N for all M,N.

    I don't know if all identities are beta-equivalent though, sorry :/
    Last edited by sleepingcat; February 13th 2009 at 10:07 PM. Reason: fixed xi rule
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 1
    Last Post: September 15th 2011, 08:35 AM
  2. Lambda Calculus: Bad Definition of Scope?
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: September 7th 2011, 12:20 PM
  3. [SOLVED] Eigenvalues of y''+2y'+\lambda y=0
    Posted in the Differential Equations Forum
    Replies: 11
    Last Post: February 26th 2011, 06:46 PM
  4. Show 1/lambda = eigenvalue of A^-1
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: February 9th 2011, 03:25 PM
  5. show that V(X) = lambda
    Posted in the Advanced Statistics Forum
    Replies: 3
    Last Post: January 11th 2009, 04:50 AM

Search Tags


/mathhelpforum @mathhelpforum