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

[David Sabel]

Hi,
  the definition in the book is a syntactic one, you are not allowed to 
beta-reduce when applying the definition.
In  particular

E = E1 E2 = (\x.xy)(\z.z)
The definition speaks about the term
(\x.xy)(\z.z) and not about (\z.z)y

and the definition does not speak about occurences of variables, it implicitely defines
the _set_ of bound variables and the _set_ of free variables of term.

Both sets needn't be disjoint, for example
In (\x.x) x
x is a free as well as a bound variable.

Regards,
  David


Am 30.12.2010 04:50, schrieb Mark Spezzano:
> Hi all,
>
> Thanks for your comments
>
> Maybe I should clarify...
>
> For example,
>
> 5.2 FREE:
> ========
> If E1 = \y.xy then x is free
> If E2 = \z.z then x is not even mentioned
>
> So E = E1 E2 = x (\z.z) and x is free as expected
> So E = E2 E1 = \y.xy and x is free as expected
>
> 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
> So E = E2 E1 = (\z.z)(\x.xy) = (\x.xy) then x is bound.
>
> Where's my mistake in the second-to-last example? Shouldn't x be bound (somewhere/somehow)?
>
> Thanks,
>
> Mark
>
>
> On 30/12/2010, at 1:52 PM, Mark Spezzano wrote:
>
>> Duh, Sorry. Yes, there was a typo
>>
>> the second one should read
>>
>> If E is a combination E1 E2 then X is bound in E if and only if X is bound in E1 or is bound in E2.
>>
>> Apologies for that oversight!
>>
>> Mark
>>
>>
>> On 30/12/2010, at 1:21 PM, Antoine Latter wrote:
>>
>>> Was there a typo in your email? Because those two definitions appear
>>> identical. I could be missing something - I haven't read that book.
>>>
>>> Antoine
>>>
>>> On Wed, Dec 29, 2010 at 9:05 PM, Mark Spezzano
>>> <mark.spezzano at chariot.net.au>  wrote:
>>>> Hi,
>>>>
>>>> Presently I am going through AJT Davie's text "An Introduction to Functional Programming Systems Using Haskell".
>>>>
>>>> On page 84, regarding formal definitions of FREE and BOUND variables he gives Defn 5.2 as
>>>>
>>>> The variable X is free in the expression E in the following cases
>>>>
>>>> a)<omitted>
>>>>
>>>> b) If E is a combination E1 E2 then X is free in E if and only if X is free in E1 or X is free in E2
>>>>
>>>> c)<omitted>
>>>>
>>>> Then in Defn 5.3 he states
>>>>
>>>> The variable X is bound in the expression E in the following cases
>>>>
>>>> a)<omitted>
>>>>
>>>> b) If E is a combination E1 E2 then X is free in E if and only if X is free in E1 or X is free in E2.
>>>>
>>>> c)<omitted>
>>>>
>>>> Now, are these definitions correct? They seem to contradict each other....and they don't make much sense on their own either (try every combination of E1 and E2 for bound and free and you'll see what I mean). If it is correct then please give some examples of E1 and E2 showing exactly why. Personally I think that there's an error in the book.
>>>>
>>>> You can see the full text on Google Books (page 84)
>>>>
>>>> Thanks for reading!
>>>>
>>>> Mark Spezzano
>>>>
>>>>
>>>> _______________________________________________
>>>> Haskell-Cafe mailing list
>>>> Haskell-Cafe at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe