# Where to find $\lambda$-calculus examples? For instance, how to check if a list is empty?

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.

-
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

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.

-