[Haskell-cafe] Lambda Calculus: Bound and Free formal definitions

[Lauri Alanko]

On Thu, Dec 30, 2010 at 02:20:34PM +1030, Mark Spezzano wrote:
> 5.3 BOUND:
> =========
> If E1 = \x.xy then x is bound
> If E2 = \z.z then is not even mentioned
> 
> So E = E1 E2 = (\x.xy)(\z.z) = (\z.z)y -- Error: x is not bound but
> should be by the rule of 5.3

Your final "=" here is beta equality. Were expecting the "bound"
property to be preserved by beta? As you observed, it is not true. Did
the book claim otherwise?

As for the correctness of the actual definitions
<http://books.google.com/books?id=OPFoJZeI8MEC&pg=PA84>, 5.2. seems
correct although sloppily named (it should say "X occurs free in E" or
"X has a free occurrence in E" instead of "X is free in"). 5.3. seems
to define a property that would properly be named "there is a binder
for X in E". Note that this is different from e.g. "X has a bound
occurrence in E".


Lauri