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:
- $(\lambda l.l(\lambda a b.true)false)(\lambda fx.x)=_{ \alpha }$
- $ =_{ \alpha }(\lambda l.l(\lambda a b.\lambda a b.a)\lambda ab.b)(\lambda fx.x)=_{\beta}$
- $=_{\beta}(\lambda l.l(\lambda a b.\lambda a b.a)\lambda ab.b)[l:=(\lambda fx.x)]=_S$
- $=_S(\lambda fx.x)(\lambda a b.\lambda a b.a)\lambda ab.b= _{\beta}$
- $= _{\beta}(\lambda x.x)(\lambda a b.\lambda a b.a)[f:=\lambda ab.b]= _S$
- $= _S (\lambda x.x)\lambda ab.b= _{\beta}$
- $= _{\beta} x[x:=\lambda ab.b]= _S$
- $= _S \lambda ab.b =_{\alpha}$
- $=_{\alpha} false$
So the empty list is not empty...
question 2: What's wrong here?
Thank you very much.