Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I'm trying to remove many layers of dust from my knowledge about $\lambda$-calculus, without my notes from classes (several hundreds of km and 5 years away).

I was trying to understand the examples in the web, but, even if they explain how different values are expressed and how functions should look like, they never explain how $\beta$-reduction is used to apply those functions to those values, and every explanation I could find on the web, without that crucial part, feels quite pointless. So, question 1, any place to find those examples? guess not, but this could be a nice place.

So as a simple example, how to check that a list is empty? I'm following the examples from here (good rank in google). So let's apply the "isEmpty" function to the empty list, that should be simple:

  1. $(\lambda l.l(\lambda a b.true)false)(\lambda fx.x)=_{ \alpha }$
  2. $ =_{ \alpha }(\lambda l.l(\lambda a b.\lambda a b.a)\lambda ab.b)(\lambda fx.x)=_{\beta}$
  3. $=_{\beta}(\lambda l.l(\lambda a b.\lambda a b.a)\lambda ab.b)[l:=(\lambda fx.x)]=_S$
  4. $=_S(\lambda fx.x)(\lambda a b.\lambda a b.a)\lambda ab.b= _{\beta}$
  5. $= _{\beta}(\lambda x.x)(\lambda a b.\lambda a b.a)[f:=\lambda ab.b]= _S$
  6. $= _S (\lambda x.x)\lambda ab.b= _{\beta}$
  7. $= _{\beta} x[x:=\lambda ab.b]= _S$
  8. $= _S \lambda ab.b =_{\alpha}$
  9. $=_{\alpha} false$

So the empty list is not empty...

question 2: What's wrong here?

Thank you very much.

share|improve this question
Why was this post voted down? –  Trylks Sep 19 '11 at 17:52
You don't have to expand from the inside out. Here you can just say $(\lambda l.l(\lambda a b.true)false)(\lambda fx.x)=_{\beta}(\lambda fx.x)(\lambda a b.true)false=_{\beta}false$ –  Peter Taylor Nov 18 '11 at 22:29

1 Answer 1

up vote 4 down vote accepted

Your reduction sequence looks correct, but the function you're applying is not isEmpty, but isNonempty.

If we're using Church representation and the the empty list is represented as $\lambda fx.x$, then the convention apparently is that the first argument to the list representation says what to do with a nonempty list, and the second argument is for an empty list. Your function is $\lambda l.l(\lambda ab.T)F$ which gives the list $F$ as a second argument -- and therefore $F$ is what you'll get at the end of the reduction.

As for web resources, a comment to this answer at SO leads to a site where you can enter lambda terms (in Haskell syntax) and see them reduce interactively.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.