CODEWITHSUNDEEP
lambda-calculus
RiseWithMoon
RiseWithMoon

Reputation: 104

Reduce Lambda Term to Normal Form

I just learned about lambda calculus and I'm having issues trying to reduce 

    (λx. (λy. y x) (λz. x z)) (λy. y y)

to its normal form. I get to (λy. y (λy. y y) (λz. (λy. y y) z) then get kind of lost. I don't know where to go from here, or if it's even correct.

Upvotes: 0

Views: 1381

Answers (1)

Gabriel L.
Gabriel L.

Reputation: 1709

(λx. (λy. y x) (λz. x z)) (λy. y y)

As @ymonad notes, one of the y parameters needs to be renamed to avoid capture (conflating different variables that only coincidentally share the same name). Here I rename the latter instance (using α-equivalence):

(λx. (λy. y x) (λz. x z)) (λm. m m)

Next step is to β-reduce. In this expression we can do so in one of two places: we can either reduce the outermost application (λx) or the inner application (λy). I'm going to do the latter, mostly on arbitrary whim / because I thought ahead a little bit and think it will result in shorter intermediate expressions:

(λx. (λz. x z) x) (λm. m m)

Still more β-reduction to do. Again I'm going to choose the inner expression because I can see where this is going, but it doesn't actually matter in this case, I'll get the same final answer regardless:

(λx. x x) (λm. m m)

Side note: these two lambda expressions (which are also known as the "Mockingbird" (as per Raymond Smullyan)) are actually α-equivalent, and the entire expression is the (in)famous Ω-combinator. If we ignore all that however, and apply another β-reduction:

(λm. m m) (λm. m m)

Ah, that's still β-reducible. Or is it? This expression is α-equivalent to the previous. Oh dear, we appear to have found ourselves stuck in an infinite loop, as is always possible in Turing-complete (or should we say Lambda-complete?) languages. One might denote this as our original expression equalling "bottom" (in Haskell parlance), denoted ⊥:

(λx. (λy. y x) (λz. x z)) (λy. y y) = ⊥

Is this a mistake? Well, some good LC theory to know is:

  • if an expression has a β-normal form, then it will be the same β-normal form no matter what order of reductions was used to reach it, and
  • if an expression has a β-normal form, then normal order evaluation is guaranteed to find it.

So what is normal order? In short, it is β-reducing the outermost expression at every step. Let's take this expression for another spin!

(λx. (λy. y x) (λz. x z)) (λm. m m)
(λy. y (λm. m m)) (λz. (λm. m m) z)
(λz. (λm. m m) z) (λm. m m)
(λm. m m) (λm. m m)

Darn. Looks like this expression has no normal form – it diverges (doesn't terminate).

Upvotes: 2

Related Questions