Lambda Calculus: Bound and Free formal definitions

older
SampleVar semantics, documentation...

Mark Spezzano

29 Dec 2010 29 Dec '10

9:05 p.m.

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

Show replies by date

Antoine Latter

29 Dec 29 Dec

9:51 p.m.

New subject: Lambda Calculus: Bound and Free formal definitions

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Mark Spezzano

10:22 p.m.

New subject: Lambda Calculus: Bound and Free formal definitions

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Gregg Reynolds

10:40 p.m.

New subject: Lambda Calculus: Bound and Free formal definitions

On Wed, Dec 29, 2010 at 9:22 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.

Seems odd. I recommend you always work from at least three different texts. Here's Hindley and Seldinhttp://www.amazon.com/Lambda-Calculus-Combinators-Introduction-Roger-Hindley... : "An occurrence of a variable x in a term P is called - *bound* if it is in the scope of a \x in P (NB: using \ as lambda) - *bound and binding* iff it is the x in \x - *free* otherwise" The tricky question is: bound to what, exactly? -Gregg

Mark Spezzano

10:50 p.m.

New subject: Lambda Calculus: Bound and Free formal definitions

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Stefan Holdermans

30 Dec 30 Dec

2:42 a.m.

New subject: Lambda Calculus: Bound and Free formal definitions

Mark, Whether a variable is bound or free depends on the scope under consideration. In (\x. x) (\y. x) the variable x is bound in \x. x, but free in \y. x; hence, it's free in (\x. x) (\y. x) as a whole. However, in \x. (\x. x) (\y. x) it's bound... HTH, Stefan

David Sabel

4:56 a.m.

New subject: Lambda Calculus: Bound and Free formal definitions

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Lauri Alanko

5:08 a.m.

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

Hans Aberg

4:27 a.m.

New subject: Lambda Calculus: Bound and Free formal definitions

On 30 Dec 2010, at 03:05, Mark Spezzano wrote:

...

... regarding formal definitions of FREE and BOUND variables he gives Defn 5.2 as

It is the occurrence of a variable that is free or bound. An occurrence of a variable is bound if it is in the scope of something that binds it; otherwise it is free.

5256

Age (days ago)

5256

Last active (days ago)

List overview

Download

8 comments

8 participants

participants (8)

Antoine Latter
David Sabel
Gregg Reynolds
Hans Aberg
Lauri Alanko
Mark Spezzano
Mark Spezzano
Stefan Holdermans