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