3
$\begingroup$

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.

  • 0
    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$2011-11-18

1 Answers 1

4

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.