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.

  • $\begingroup$ Why was this post voted down? $\endgroup$ – Trylks Sep 19 '11 at 17:52
  • $\begingroup$ 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$ $\endgroup$ – Peter Taylor Nov 18 '11 at 22:29

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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