Scheme - Problem with EOPL exercise

Author

Problem with EOPL exercise

Alex McGuire

2004-09-09, 8:57 pm

Having finally begun to work my way through EOPL (My theory that I could
learn by osmosis by simply leaving the book unopened next to my desk
doesn't seem to work), I'm stuck on exercise 1.20, which is

1.20. Give an example of a lambda calculus expression in which a
variable occurs free but which has a value that is independent of the
value of the free variable.

EOPL defines the lambda calculus by the grammar

<expression> ::= <identifier>
::= (lambda (<identifier> ) <expression> )
::= (<expression> <expression> )

I'm not familiar with lambda calculus but the definition on wikipedia
seems the same.

I thought at first of expressions like

(lambda (x)
(lambda (y) y))

but according to EOPL x is not free in this expression.

I'm now completely stumped, given this grammar I can't even think of an
expression with a free variable that could be valued.

This isn't homework, in fact I'd appreciate an illuminating hint even
more than the answer.

thanks,

Alex

Alex McGuire

2004-09-09, 8:57 pm

As has happened before, after two hours spent thinking about the problem
a solution occurs to me five minutes after posting to usenet.

((lambda (x) y) z)

z is free, but no matter what it is bound to the result will always be y.

Is this right?

thanks,

Alex

Alex McGuire wrote:
> Having finally begun to work my way through EOPL (My theory that I could
> learn by osmosis by simply leaving the book unopened next to my desk
> doesn't seem to work), I'm stuck on exercise 1.20, which is
>
>
> 1.20. Give an example of a lambda calculus expression in which a
> variable occurs free but which has a value that is independent of the
> value of the free variable.
>
> EOPL defines the lambda calculus by the grammar
>
> <expression> ::= <identifier>
> ::= (lambda (<identifier> ) <expression> )
> ::= (<expression> <expression> )
>
> I'm not familiar with lambda calculus but the definition on wikipedia
> seems the same.
>
> I thought at first of expressions like
>
> (lambda (x)
> (lambda (y) y))
>
> but according to EOPL x is not free in this expression.
>
> I'm now completely stumped, given this grammar I can't even think of an
> expression with a free variable that could be valued.
>
> This isn't homework, in fact I'd appreciate an illuminating hint even
> more than the answer.
>
>
>
> thanks,
>
>
> Alex

Marlene Miller

2004-09-10, 3:59 am

Hi Alex.

I was working 1.20 a few w

s ago, and that's the exact same answer I came
up with. Of course, that doesn't mean it is correct.

It's the next one that

me.
1.21. Give an example of a lambda calculus expression in which the same
variable occurs both free and bound.

My answer is ((lambda (x) x) x). But as I see it, the bound variable x and
the free variable x are not the same variable.

Marlene

"Alex McGuire" <alex@ignorethisbit-alexmcguire.com> wrote in message
news:chqqa5$c86$1@news-reader4.wanadoo.fr...[color=darkred]
> As has happened before, after two hours spent thinking about the problem
> a solution occurs to me five minutes after posting to usenet.
>
> ((lambda (x) y) z)
>
> z is free, but no matter what it is bound to the result will always be y.
>
> Is this right?
>
> thanks,
>
> Alex
>
>
> Alex McGuire wrote:

Nic Ferrier

2004-09-10, 3:59 am

Alex McGuire <alex@ignorethisbit-alexmcguire.com> writes:

> As has happened before, after two hours spent thinking about the
> problem a solution occurs to me five minutes after posting to usenet.
>
> ((lambda (x) y) z)
>
> z is free, but no matter what it is bound to the result will always be y.
>
> Is this right?

Here's a straight forward example:

(lambda (name)
(lambda (method)
(cond
((eq? method 'address)
(list "Some Street" "Townsville" "ZZZ177"))

((eq? method 'person)
(list name)))))

So this is a procedure that when called with a 'name' returns another
procedure.

The returned procedure is a method dispatcher procedure, an example
use of the above (presuming the top lambda is called make-person) would be:

(let ((me (make-person "nic")))
(me 'address))
=> ("Some Street" "Townsville" "ZZZ177"))

Now the bit you want to know: in the returned lambda (the one that
implements the method dispatcher) the variable 'name' occurs free.

This means that it is not bound by the arguments of the procedure but
is refereneced through environment capture; the second lambda
'remembers' what bindings were in force when it was created.

So to return to the sparsity of your example:

((lambda (x) (lambda (y) (+ x y))) 6)

returns a proc which can add things to 6, eg:

(((lambda (x) (lambda (y) (+ x y))) 6) 4)
=> 10

The variable x is said to occur free here in the inner lambda.

Again, this is because x is not bound in the arguments of the inner
lambda. x is only in scope in the inner lambda by the practice of
environment capture.

Nic Ferrier
http://www.tapsellferrier.co.uk

Marlene Miller

2004-09-10, 3:59 am

"Alex McGuire" <alex@ignorethisbit-alexmcguire.com> wrote in message
news:chqqa5$c86$1@news-reader4.wanadoo.fr...
> As has happened before, after two hours spent thinking about the problem
> a solution occurs to me five minutes after posting to usenet.
>
> ((lambda (x) y) z)
>
> z is free, but no matter what it is bound to the result will always be y.
>
> Is this right?
>
> thanks,
>
> Alex
>
>
> Alex McGuire wrote:
[color=darkred]

Alex, maybe this is obvious, but DrScheme will tell you it's right.
[color=darkred]
> ((lambda (x) y) z)
; => reference to undefined identifier: z

So z is free.

> (define z 1)
> ((lambda (x) y) z)
; => reference to undefined identifier: y

So y is free.

(define z 1)
(define y 2)
((lambda (x) y) z)
; => 2

So its right.

Ron Garret

2004-09-10, 3:59 am

In article <87k6v2nbpd.fsf@tapsellferrier.co.uk>,
Nic Ferrier <nferrier@tapsellferrier.co.uk> wrote:

> Alex McGuire <alex@ignorethisbit-alexmcguire.com> writes:
>
>
> Here's a straight forward example:

Here's an even more straightforward one:

(lambda (x) y)

A less controversial answer would be something like this:

((lambda (x) (lambda (y) y)) z)

Z occurs free, but the value of this expression is always the identity
function regardless of the value of Z.

rg

Alex McGuire

2004-09-10, 3:59 am

Nic Ferrier wrote:
>
> Here's a straight forward example:
>
> (lambda (name)
> (lambda (method)
> (cond
> ((eq? method 'address)
> (list "Some Street" "Townsville" "ZZZ177"))
>
> ((eq? method 'person)
> (list name)))))
>

But that's not a lambda calculus expression, at least according the
grammar I wrote in the original post.
<snip>

>
> So to return to the sparsity of your example:
>
> ((lambda (x) (lambda (y) (+ x y))) 6)
>
> returns a proc which can add things to 6, eg:
>
> (((lambda (x) (lambda (y) (+ x y))) 6) 4)
> => 10
>
> The variable x is said to occur free here in the inner lambda.
>
> Again, this is because x is not bound in the arguments of the inner
> lambda. x is only in scope in the inner lambda by the practice of
> environment capture.

x is free in the inner lambda, but the value of the inner lambda isn't
independent of the value of x, which is what the exercise required, I
think - I took the exercise to mean this

"Find a lambda expression E with a free variable x such that no matter
what x is bound to in an enclosing expression, the value of E doesn't
change."

Alex McGuire

2004-09-10, 3:59 am

Ron Garret wrote:
> In article <87k6v2nbpd.fsf@tapsellferrier.co.uk>,
> Nic Ferrier <nferrier@tapsellferrier.co.uk> wrote:
>
>
>
>
> Here's an even more straightforward one:
>
> (lambda (x) y)
>
I don't think this works,

1 ]=> ((lambda (y) ((lambda (x) y) 1)) 10)

;Value: 10

1 ]=> ((lambda (y) ((lambda (x) y) 1)) 5)

;Value: 5

> A less controversial answer would be something like this:
>
> ((lambda (x) (lambda (y) y)) z)
>
> Z occurs free, but the value of this expression is always the identity
> function regardless of the value of Z.
>
> rg

Alex McGuire

2004-09-10, 3:59 am

Marlene Miller wrote:
> Hi Alex.
>
> I was working 1.20 a few w

s ago, and that's the exact same answer I came
> up with. Of course, that doesn't mean it is correct.
>
> It's the next one that

me.
> 1.21. Give an example of a lambda calculus expression in which the same
> variable occurs both free and bound.
>
> My answer is ((lambda (x) x) x). But as I see it, the bound variable x and
> the free variable x are not the same variable.
>
> Marlene
>

Hi Marlene

That was puzzling me too. I think the confusion is that by 'variable',
EOPL simply means the symbol, in this case 'x'. In some expression two
'x's may denote different things, but they are still the same variable.

Obviously this is not how a programmer would describe the word
'variable', but after looking at the lambda calculus section on
wikipedia last night I think it's what they mean.

Alex

Alex McGuire

2004-09-10, 8:59 am

Ron Garret wrote:
> In article <87k6v2nbpd.fsf@tapsellferrier.co.uk>,
> Nic Ferrier <nferrier@tapsellferrier.co.uk> wrote:
>
>
......[color=darkred]
> A less controversial answer would be something like this:
>
> ((lambda (x) (lambda (y) y)) z)
>
......

You're right, the solution Marlene and I came up with fails when y and z
are bound to the same value, which of course can't happen with yours

1 ]=> ((lambda (z)
((lambda (y)
((lambda (x) y) z))
z))
11)

;Value: 11

1 ]=> ((lambda (z)
((lambda (y)
((lambda (x) y) z))
z))
13)

;Value: 13

cheers,

Alex

Alex McGuire

2004-09-10, 8:59 am

Ron Garret wrote:

> In article <87k6v2nbpd.fsf@tapsellferrier.co.uk>,
> Nic Ferrier <nferrier@tapsellferrier.co.uk> wrote:
>
>
be y.[color=darkred]
......
[color=darkred]
> A less controversial answer would be something like this:
>
> ((lambda (x) (lambda (y) y)) z)
>
......

You're right, the solution Marlene and I came up with fails when y and z
are bound to the same value, which of course can't happen with yours

1 ]=> ((lambda (z)
((lambda (y)
((lambda (x) y) z))
z))
11)

;Value: 11

1 ]=> ((lambda (z)
((lambda (y)
((lambda (x) y) z))
z))
13)

;Value: 13

cheers,

Alex

Ron Garret

2004-09-10, 4:01 pm

In article <chrjt3$o55$1@news-reader3.wanadoo.fr>,
Alex McGuire <alex@ignorethisbit-alexmcguire.com> wrote:

> Ron Garret wrote:
> I don't think this works,

Why not?

> 1 ]=> ((lambda (y) ((lambda (x) y) 1)) 10)
>
> ;Value: 10
>
> 1 ]=> ((lambda (y) ((lambda (x) y) 1)) 5)
>
> ;Value: 5

But that's a red herring. The question was:

> 1.20. Give an example of a lambda calculus expression in which a
> variable occurs free but which has a value that is independent of the
> value of the free variable.

The expression (lambda (x) y) meets these conditions. It has a variable
that occurs free (Y) and it has a value that is independent of Y. That
value is a procedure that returns Y. The value returned by this
procedure is obviously not independent of Y, but the procedure itself is.

I knew this would be controversial, which is why I included the second
example:

((lambda (x) (lambda (y) y)) z)

but this is equivalent to:

(lambda (y) y)

which is "the identity function". But it's not really "the" identity
function, it's just "an" identity function. Likewise, (lambda (x) y) is
either "the" function that returns Y or "a" function that returns Y, but
in either case, if you accept ((lambda (x) (lambda (y) y)) z) as a
solution to the problem (which most people would) then there is no
principled reason to reject (lambda (x) y). And if you think there is,
consider the following:

(lambda (x) (if (and (odd? x) (even? x)) y x))

or:

(lambda (x) (if (find-counterexample-to-fermats-last-theorem) y x))

Rendering "if", "and", "odd?", "even?" and "find-counterexample-to-
fermats-last-theorem" as lambda calculus expressions are left as
exercises. (I strongly recommend tackling them in that order.)

Of course, if you are a student it could be unwise to raise this issue
with your professor.

E.

William D Clinger

2004-09-10, 4:01 pm

"Marlene Miller" <marlenemiller@worldnet.att.net> wrote:
> Alex, maybe this is obvious, but DrScheme will tell you it's right.
>
> ; => reference to undefined identifier: z
>
> So z is free.

What does DrScheme say about

((lambda (x) (lambda (x) x)) (lambda (x) z)) ?

Will

Marlene Miller

2004-09-10, 8:57 pm

"William D Clinger" <cesuraSPAM@verizon.net> wrote in message
> What does DrScheme say about
>
> ((lambda (x) (lambda (x) x)) (lambda (x) z)) ?
>
> Will

Oh, this is good. When I use the SICP environment model (and draw all those
boxes and circles), I see that a procedure P1 with body (lambda (x) x) is
created, and a procedure P2 with body z is created. When P1 is applied to
P2, an environment E1 is created with x bound to P2. Then (lambda (x) x) is
evaluated and a procedure P3 pointing to E1 is created. But the body of P2,
namely z, is never evaluated. P3 is returned.

Thank you.

(It's not good to study a book on your own. You never know when you have
wrong answers.)

Marlene

Alex McGuire

2004-09-10, 8:57 pm

Ron Garret wrote:
......

>
>
> Why not?
>
>
>
>
> But that's a red herring. The question was:
>
>
>
>
> The expression (lambda (x) y) meets these conditions. It has a variable
> that occurs free (Y) and it has a value that is independent of Y. That
> value is a procedure that returns Y. The value returned by this
> procedure is obviously not independent of Y, but the procedure itself is.
>
Aha. I had assumed that

'has a value that is independent of the value of the free variable'

meant

'is independent of any binding of the free variable outside the lambda
expression'

I see the difference now, I think.

Do you think the question was loosely worded? If so could you express it
more rigorously?

> I knew this would be controversial, which is why I included the second
> example:
>
> ((lambda (x) (lambda (y) y)) z)
>
> but this is equivalent to:
>
> (lambda (y) y)
>
> which is "the identity function". But it's not really "the" identity
> function, it's just "an" identity function. Likewise, (lambda (x) y) is
> either "the" function that returns Y or "a" function that returns Y, but
> in either case, if you accept ((lambda (x) (lambda (y) y)) z) as a
> solution to the problem (which most people would) then there is no
> principled reason to reject (lambda (x) y). And if you think there is,
> consider the following:
>
> (lambda (x) (if (and (odd? x) (even? x)) y x))
>
> or:
>
> (lambda (x) (if (find-counterexample-to-fermats-last-theorem) y x))
>
I'm not sure what objection to (lambda (x) y) I could have that is
countered by these examples.

> Rendering "if", "and", "odd?", "even?" and "find-counterexample-to-
> fermats-last-theorem" as lambda calculus expressions are left as
> exercises. (I strongly recommend tackling them in that order.)

I'll try that, well maybe not the last, as my hard drive is too small to
contain the expression. I'd be interested to know if

(lambda (x) (if (and (odd? x) (even? x)) y x))

reduces to

(lambda (x) x)

Alex

Matthias Blume

2004-09-10, 8:57 pm

Alex McGuire <alex@ignorethisbit-alexmcguire.com> writes:

> Ron Garret wrote:
> .....
>
> Aha. I had assumed that
>
> 'has a value that is independent of the value of the free variable'
>
> meant
>
> 'is independent of any binding of the free variable outside the lambda
> expression'
>
> I see the difference now, I think.
>
> Do you think the question was loosely worded? If so could you express
> it more rigorously?

The question is rather loosely worded -- in the context of Scheme,
where "binding" and "value" of a variable are not the same thing. If
the language didn't have mutable variables, then the answer would have
been quite firmly: (lambda (x) y) does depend on y!

In Scheme the situation is a bit tricky:

1. There are mutable variables, so the value of (lambda (x) y)
would not change even if you assigned a new value to y.
2. The value of (lambda (x) y) does depend on the
binding of y (that is: the location that y is bound to). For
example, car and cdr of the value returned by

(cons (let ((y 1)) (lambda (x) y))
(let ((y 1)) (lambda (x) y)))

would be different.
3. However, in many implementations of Scheme the car and cdr even of

(let ((y 1)) (cons (lambda (x) y) (lambda (x) y)))

will be different, but that is neither required nor prohibited by
the standard.

So don't be misled. Under certain interpretations of the question,
(lambda (x) y) is a perfectly good answer. The value of this
expression certainly depends on the binding of y (but not on its
value).

Matthias

Marlene Miller

2004-09-10, 8:57 pm

"Alex McGuire" <alex@ignorethisbit-alexmcguire.com> wrote

> You're right, the solution Marlene and I came up with fails when y and z
> are bound to the same value, which of course can't happen with yours

Alex,

re: ((lambda (x) y) z)

Is this what you mean by y and z being bound to the same value?

((lambda (y) ((lambda (x) y) z)) z)

Marlene

Marlene Miller

2004-09-10, 8:57 pm

"Marlene Miller" <marlenemiller@worldnet.att.net> wrote > Alex,
>
> re: ((lambda (x) y) z)
>
> Is this what you mean by y and z being bound to the same value?
>
> ((lambda (y) ((lambda (x) y) z)) z)
>
> Marlene

Please ignore this. It's the same as your examples at 12:04 AM.

Marlene Miller

2004-09-11, 3:56 am

"Matthias Blume" <find@my.address.elsewhere> wrote in message
>
> The question is rather loosely worded -- in the context of Scheme,
> where "binding" and "value" of a variable are not the same thing. If
> the language didn't have mutable variables, then the answer would have
> been quite firmly: (lambda (x) y) does depend on y!
>
> In Scheme the situation is a bit tricky:
>
> 1. There are mutable variables, so the value of (lambda (x) y)
> would not change even if you assigned a new value to y.
> 2. The value of (lambda (x) y) does depend on the
> binding of y (that is: the location that y is bound to). For
> example, car and cdr of the value returned by
>
> (cons (let ((y 1)) (lambda (x) y))
> (let ((y 1)) (lambda (x) y)))
>
> would be different.
> 3. However, in many implementations of Scheme the car and cdr even of
>
> (let ((y 1)) (cons (lambda (x) y) (lambda (x) y)))
>
> will be different, but that is neither required nor prohibited by
> the standard.
>
> So don't be misled. Under certain interpretations of the question,
> (lambda (x) y) is a perfectly good answer. The value of this
> expression certainly depends on the binding of y (but not on its
> value).
>
> Matthias

(define p
(lambda (x)
(lambda (x) y)))

(equal? (p 1) (p 1)) ; => #f

The value of the expression (lambda (x) y) varies even when the value of y
is the same.

I was thinking, to know whether the value of an expression depends on the
value of a variable, we should evaluate the expression for each value of the
variable and compare the results. This strategy will not work here.

Marlene

Kristof Bastiaensen

2004-09-11, 8:56 am

On Fri, 10 Sep 2004 18:26:15 -0500, Matthias Blume wrote:

> Alex McGuire <alex@ignorethisbit-alexmcguire.com> writes:

I don't understand how (lambda (x) y) can be considered independent of
y. The value of this expression is y. Is y independent of y?
[color=darkred]

If the value of the function depends on y, then I would say that the
function depends on y.
[color=darkred]
>
> The question is rather loosely worded -- in the context of Scheme, where
> "binding" and "value" of a variable are not the same thing. If the
> language didn't have mutable variables, then the answer would have been
> quite firmly: (lambda (x) y) does depend on y!
>

I disagree. The question stated clearly "a lambda calculus expression",
not a "scheme expression".

> In Scheme the situation is a bit tricky:
>
> 1. There are mutable variables, so the value of (lambda (x) y)
> would not change even if you assigned a new value to y.

???

(define (a) (lambda (x) y))
(define y 1)
(a) ;=> 1
(set! y 2)
(a) ;=> 2

> 2. The value of (lambda (x) y) does depend on the
> binding of y (that is: the location that y is bound to). For
> example, car and cdr of the value returned by
>
> (cons (let ((y 1)) (lambda (x) y))
> (let ((y 1)) (lambda (x) y)))
>
> would be different.
> 3. However, in many implementations of Scheme the car and cdr even of
>
> (let ((y 1)) (cons (lambda (x) y) (lambda (x) y)))
>
> will be different, but that is neither required nor prohibited by the
> standard.
>
> So don't be misled. Under certain interpretations of the question,
> (lambda (x) y) is a perfectly good answer. The value of this expression
> certainly depends on the binding of y (but not on its value).
>

I see what you are getting at. But the value and the binding of a
variable are only different because scheme is an impure functional
language. Ideally they are the same (as in haskell or ML). In the
scope of this question they are the same, because the question asked
for a lambda-calculus expression. So (lambda (x) y) would be a wrong
answer to this question.

> Matthias

Regards,
KB

Matthias Blume

2004-09-11, 3:57 pm

Kristof Bastiaensen <kristof@vleeuwen.org> writes:

> On Fri, 10 Sep 2004 18:26:15 -0500, Matthias Blume wrote:
>
>
> I don't understand how (lambda (x) y) can be considered independent of
> y. The value of this expression is y. Is y independent of y?

Yes. (The question is "what does y name -- is it a value, or a location?".)

>
>
> If the value of the function depends on y, then I would say that the
> function depends on y.
>
>
> I disagree. The question stated clearly "a lambda calculus expression",
> not a "scheme expression".

Ok. In that case the answer is very clearly: (lambda (x) y) depends
on y and would not be a good answer to the question.

>
> ???
>
> (define (a) (lambda (x) y))
> (define y 1)
> (a) ;=> 1
> (set! y 2)
> (a) ;=> 2

That's not the point. The value of the function itself (its identity)
has not changed by assigning to the variable.

>
>
> I see what you are getting at. But the value and the binding of a
> variable are only different because scheme is an impure functional
> language.

Exactly.

> Ideally they are the same (as in haskell or ML). In the
> scope of this question they are the same, because the question asked
> for a lambda-calculus expression. So (lambda (x) y) would be a wrong
> answer to this question.

That is right. That is exactly what I was getting at.

Matthias

Ron Garret

2004-09-11, 3:57 pm

In article <pan.2004.09.11.11.42.44.953968@vleeuwen.org>,
Kristof Bastiaensen <kristof@vleeuwen.org> wrote:

> I don't understand how (lambda (x) y) can be considered independent of
> y. The value of this expression is y.

No, it isn't. You are confusing (lambda (x) y) with ((lambda (x) y)).
These are not the same thing. The value of the latter is indeed Y, but
the value of the former is a function.

> If the value of the function depends on y, then I would say that the
> function depends on y.

Certainly. The value of the expression is a function that depends on Y.
But this is the case regardless of the value of Y. No matter what the
value of Y is, the value of the expression is THE SAME FUNCTION. Since
the value of the expression is the same thing regardless of the value of
Y, it is a valid answer to the original question.

rg

Ron Garret

2004-09-11, 3:57 pm

In article
<Rjx0d.577525$Gx4.305989@bgtnsc04-news.ops.worldnet.att.net>,
"Marlene Miller" <marlenemiller@worldnet.att.net> wrote:

> (define p
> (lambda (x)
> (lambda (x) y)))
>
> (equal? (p 1) (p 1)) ; => #f
>
> The value of the expression (lambda (x) y) varies even when the value of y
> is the same.

Try:

(define p
(lambda (y)
(lambda (x) x)))

and you'll get the same result.

Scheme is not the lambda calculus.

rg

Ron Garret

2004-09-11, 3:57 pm

In article <m1fz5ppuy0.fsf@tti5.uchicago.edu>,
Matthias Blume <find@my.address.elsewhere> wrote:

>
> The question is rather loosely worded -- in the context of Scheme,
> where "binding" and "value" of a variable are not the same thing.

This is true, but I think it's irrelevant to the matter at hand. The
looseness in the question is, IMO, the use of the word "independent"
without defining what that means with regards to functional values.

For example, is the following independent of Y?

(if y (lambda (x) x) (lambda (z) z))

Once again, mentally map IF onto an appropriate lambda calculus
translation.

rg

Ron Garret

2004-09-11, 3:57 pm

In article <chtaqv$hb2$1@news-reader4.wanadoo.fr>,
Alex McGuire <alex@ignorethisbit-alexmcguire.com> wrote:

>
> I'll try that, well maybe not the last, as my hard drive is too small to
> contain the expression. I'd be interested to know if
>
> (lambda (x) (if (and (odd? x) (even? x)) y x))
>
> reduces to
>
> (lambda (x) x)

If you're serious about pursuing this you might want to take a look at
the ACL2 automatic theorem prover.

rg

Matthias Blume

2004-09-11, 3:57 pm

Ron Garret <rNOSPAMon@flownet.com> writes:

> In article <pan.2004.09.11.11.42.44.953968@vleeuwen.org>,
> Kristof Bastiaensen <kristof@vleeuwen.org> wrote:
>
>
> No, it isn't. You are confusing (lambda (x) y) with ((lambda (x) y)).
> These are not the same thing. The value of the latter is indeed Y, but
> the value of the former is a function.
>
>
> Certainly. The value of the expression is a function that depends on Y.
> But this is the case regardless of the value of Y. No matter what the
> value of Y is, the value of the expression is THE SAME FUNCTION.

False. If y means 2, then (lambda (x) y) is the function that always
returns 2. If y means 3, then (lambda (x) y) is the function that
always returns 3. These two functions are obviously not the same.

> Since the value of the expression is the same thing regardless of
> the value of Y, it is a valid answer to the original question.

False.

Matthias

Matthias Blume

2004-09-11, 3:57 pm

Ron Garret <rNOSPAMon@flownet.com> writes:

> In article <m1fz5ppuy0.fsf@tti5.uchicago.edu>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
>
> This is true, but I think it's irrelevant to the matter at hand. The
> looseness in the question is, IMO, the use of the word "independent"
> without defining what that means with regards to functional values.

False. As someone else has pointed out, in the context of the lambda
calculus (which is how the question was phrased -- but I initially
missed that), (lambda (x) y) is not independent of y. By
"independent" we usually mean that the value of the former does not
vary with the value of the latter.

> For example, is the following independent of Y?
>
> (if y (lambda (x) x) (lambda (z) z))
>
> Once again, mentally map IF onto an appropriate lambda calculus
> translation.

No -- if by "appropriate lambda calculus translation" you mean
something like the following:

"if" = (lambda (c t e) (c t e))
"true" = (lambda (x y) x)
"false" = (lambda (x y) y)

Proof:

let y = (lambda (x y) 1), so
(if y ... ...) --> 1
let y = (lambda (x y) 2), so
(if y ... ...) --> 2
both regardless of ...

In a typed lambda calculus, however, the above is independent of y because
my proof won't type-check there.

Matthias

Lauri Alanko

2004-09-11, 3:57 pm

In article <m2sm9on5n3.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:
[color=darkred]
> In a typed lambda calculus, however, the above is independent of y because
> my proof won't type-check there.

Unless y diverges.

Lauri

Anton van Straaten

2004-09-11, 3:57 pm

Alex McGuire wrote:

> I'll try that, well maybe not the last, as my hard drive is too small
> to contain the expression. I'd be interested to know if
>
> (lambda (x) (if (and (odd? x) (even? x)) y x))
>
> reduces to
>
> (lambda (x) x)

If you consider that in untyped lambda calculus, 'x' could be any function
whatsoever, this reduction isn't valid, in general (assuming the usual
meaning of odd? and even?, which depend on their input, x).

For example, using typical encodings for booleans, Church numerals etc.,
applying your original function to the boolean value 'true', represented as
(lambda (x) (lambda (y) x)), can produce a result of y, which nicely shows
that in general, your function is not the identity function, and further,
that the free occurrence of y isn't redundant.

Of course, you can constrain the input to your function to be numeric, but
untyped LC reduction doesn't "know" that (kind of the way herbivorous
dinosaurs in Jurassic Park may not know that they're not supposed to eat
humans), so it doesn't really help you. You'd have to apply outside
knowledge during the reduction process to get the result you want. I'll
give an example below.

Using typical encodings, your expression can be reduced to something like
the following, given in Scheme syntax, but with "lambda (x)" replaced by \x.

(\x. ((((((x (\x. ((x (\x. (\y. y))) (\x. (\y. x))))) (\x. (\y. x))) ((x
(\x. ((x (\x. (\y. y))) (\x. (\y. x))))) (\x. (\y. y)))) (\x. (\y. y))) y)
x))

That's fully expanded; with abbreviations for booleans, it looks like this:

(\x. (((((x (\x. (x false true)) true) ((x (\x. (x false true))) false))
false) y) x))

The problem here is that the expression depends on the value of x, and can't
be further reduced without that.

Assuming x is a number encoded as a Church numeral, it's easy to show that
(x false true) evaluates to the identity function, for any numeric x>0
(that's left as an exercise for the reader). With that outside knowledge,
we can reduce the above to:

(\x. (((((x (\x. (\y. y)) true) ((x (\x. (\y. y))) false)) false) y) x))

We can see some subterms here which happen to be our representation of
booleans, so the above can be rewritten for easier comprehension as:

(\x. (((((x false true) (x false false)) false) y) x))

Again, (x false true) is the identity function for x>0. It so happens that
the same is true of (x false false). Given that, the above reduces to:

(\x. (false y x))

Now we're getting somewhere: via ordinary reduction, this reduces to:

(lambda (x) x)

....which is the answer you wanted, keeping in mind that, at least by the
above sketch, this is only guaranteed to work for x>0. However, this wasn't
achieved only by lambda calculus reduction: it involved outside knowledge of
equivalences that don't arise out of the reduction process itself.

Anton

David Van Horn

2004-09-11, 3:57 pm

EOPL states:
> 1.20. Give an example of a lambda calculus expression in which a
> variable occurs free but which has a value that is independent of
> the value of the free variable.

Alex McGuire wrote:
> Do you think the question was loosely worded? If so could you express it
> more rigorously?

Here is another way to look at the question:

Give an example of an expression E in which the variable z occurs free, such
that for all values V, V':

((lambda (z) E) V) has the same value as ((lambda (z) E) V')

Note that values are the subset of expressions of the form
(lambda (<var> ) <exp> ).

There are two implied notions here that are left a bit fuzzy at this point
in EoPL if I recall correctly (it's been a long time, and my copy is not in
front of me).

1) For an expression E, what does it mean to say "E has a value V"?
2) For values V, V', what does it mean to say "V is the same as V'"?

It suffices to say for the purposes of this example that:

"E has a value V" iff
- E is a value V
- E is of the form (E1 E2) and
E1 has the value (lambda (x) E') and
E2 has the value V' and
E'[V'/x] has the value V

Where E[V/x] means to replace all free occurrences of x with V in E.
(You may have to look ahead for substitution). Note that not all
expressions "have a value."

"V is the same as V'" iff we can alpha-convert one to obtain exactly the
other.

Where alpha-convert means "to consistently rename the bound variables of
a value." For example, (lambda (x) x) is the same as (lambda (y) y).
(You may have to look ahead for alpha-conversion).

If we return to Will Clinger's suggestion:

Let E = ((lambda (x) (lambda (x) x)) (lambda (x) z))

Does ((lambda (z) E) V) have the same value as ((lambda (z) E) V') for all
V, V'?

David

Marlene Miller

2004-09-11, 8:56 pm

"Ron Garret" <rNOSPAMon@flownet.com> wrote in message
news:rNOSPAMon-4B67F3.08345311092004@nntp1.jpl.nasa.gov...
> In article
> <Rjx0d.577525$Gx4.305989@bgtnsc04-news.ops.worldnet.att.net>,
> "Marlene Miller" <marlenemiller@worldnet.att.net> wrote:
>
y[color=darkred]
>
> Try:
>
> (define p
> (lambda (y)
> (lambda (x) x)))
>
> and you'll get the same result.

Yes. But we are studying (lambda (x) y) because y is free.

>
> Scheme is not the lambda calculus.
>
> rg

Yes. On page 6 of EoPL, "This grammar defines the elements of <expression>
as Scheme values, so it is convenient to manipulate them." Since the BNF
productions for the lambda calculus do not say anything about values, I
thought I should use Scheme values.

I was trying to understand what "depends on" means. It has something to do
with one thing changing causing another thing to change. How can we know if
the other thing has changed? By testing for equality. But how can we test
for equality if the other thing changes whether or not we change y?

Matthias Blume

2004-09-11, 8:56 pm

Lauri Alanko <la@iki.fi> writes:

> In article <m2sm9on5n3.fsf@hanabi.local>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
>
> Unless y diverges.

Well, assuming y is a value.

Ron Garret

2004-09-11, 8:56 pm

In article <m2sm9on5n3.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:

>
> No -- if by "appropriate lambda calculus translation" you mean
> something like the following:
>
> "if" = (lambda (c t e) (c t e))
> "true" = (lambda (x y) x)
> "false" = (lambda (x y) y)
>
> Proof:
>
> let y = (lambda (x y) 1), so
> (if y ... ...) --> 1
> let y = (lambda (x y) 2), so
> (if y ... ...) --> 2
> both regardless of ...

That is indeed the usual rendering of IF, TRUE and FALSE in the lambda
calculus, but you thwarted the intent of my example by binding Y to a
value that is nether true nor false according to this mapping. My
intent was closer to:

(if some-expression-that-evaluates-to-true-or-false-depending-on-Y
(lambda (x) x)
(lambda (y) y))

rg

Ron Garret

2004-09-11, 8:56 pm

In article <m2wtz0n5x5.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:

> Ron Garret <rNOSPAMon@flownet.com> writes:
>
>
> False. If y means 2, then (lambda (x) y) is the function that always
> returns 2. If y means 3, then (lambda (x) y) is the function that
> always returns 3. These two functions are obviously not the same.

Well, it depends on what you mean by "the same". They are both "the
function that returns Y."

However, upon re-reading EOPL I think I am actually on very shaky ground
with this position, since EOPL defines free-ness as being relative to a
context. So a reasonable interpretation of the question is to find an
expression with a free variable whose value is the same IN ANY CONTEXT,
not just (as I tacitly assumed) a "top-level" context where the
expression containing the free variable is not enclosed in a context
that binds that variable. Under that interpretation my answer does
indeed fail, since (as I believe Anton was first to point out in this
thread) Y could have different bindings. But I'll stand by my answer
under my original interpretation.

rg

Matthias Blume

2004-09-12, 3:56 am

Ron Garret <rNOSPAMon@flownet.com> writes:

> In article <m2sm9on5n3.fsf@hanabi.local>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
>
> That is indeed the usual rendering of IF, TRUE and FALSE in the lambda
> calculus, but you thwarted the intent of my example by binding Y to a
> value that is nether true nor false according to this mapping. My
> intent was closer to:
>
> (if some-expression-that-evaluates-to-true-or-false-depending-on-Y
> (lambda (x) x)
> (lambda (y) y))

Right. I already said that with static typing your claim would be
true. What you want is, effectively, static typing.

Matthias

Matthias Blume

2004-09-12, 3:56 am

Ron Garret <rNOSPAMon@flownet.com> writes:

> In article <m2wtz0n5x5.fsf@hanabi.local>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
>
> Well, it depends on what you mean by "the same". They are both "the
> function that returns Y."
>
> However, upon re-reading EOPL I think I am actually on very shaky ground
> with this position, since EOPL defines free-ness as being relative to a
> context. So a reasonable interpretation of the question is to find an
> expression with a free variable whose value is the same IN ANY CONTEXT,
> not just (as I tacitly assumed) a "top-level" context where the
> expression containing the free variable is not enclosed in a context
> that binds that variable. Under that interpretation my answer does
> indeed fail, since (as I believe Anton was first to point out in this
> thread) Y could have different bindings. But I'll stand by my answer
> under my original interpretation.

I don't understand your original interpretation. Could you explain?

If the variable is assumed to not be bound at all, how could anything
"depend" on it? After all, it has no meaning then. Thus, the only
possible interpretation of the question is, indeed, the one you gave:
the value of the expression in question must be independent of how its
context binds that free variable.

Matthias

Kristof Bastiaensen

2004-09-12, 3:57 pm

On Sat, 11 Sep 2004 08:32:57 -0700, Ron Garret wrote:

> In article <pan.2004.09.11.11.42.44.953968@vleeuwen.org>,
> Kristof Bastiaensen <kristof@vleeuwen.org> wrote:
>
>
> No, it isn't. You are confusing (lambda (x) y) with ((lambda (x) y)).
> These are not the same thing. The value of the latter is indeed Y, but
> the value of the former is a function.
>

That's correct. I meant the value of the lambda-expression is y
when applied to an argument.

Regards,
KB

Ron Garret

2004-09-12, 8:56 pm

In article <m2fz5omeox.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:

> Ron Garret <rNOSPAMon@flownet.com> writes:
>
>
> I don't understand your original interpretation. Could you explain?

I had assumed that freeness was an absolute property, i.e. that the
answer to "Does Y occur free in (lambda (y) (lambda (x) (f x y))) was
unambiguously "no". On this view, all free variables are "top-level" or
"global" references. (I put these terms in scare quotes because there
really isn't any such thing in the lambda calculus as "top-level" or
"global", but there also isn't really any such thing as "the value of an
expression" either, there is only equivalence of expressions according
to the reduction rules, so the question itself opens the door to playing
a little fast and loose with the terminology.)

On this view, (lambda () y) is the function that returns Y, or to be
more precise, it is the function that returns the value of the global
and therefore unique (and, I might add, in the lambda calculus,
immutable) binding of Y. Or it would be if the lambda calculus actually
had such a concept as "global".

FWIW, I wasn't raising this example just to be a wise guy. I had an
actual pedagogical purpose, namely, to highlight the difference between
"the function that returns Y" and "the value returned by the function
that returns Y when that function is actually invoked." These are not
the same thing, even in the lambda calculus (and certainly not in
Scheme). The latter clearly depends on Y, but the former arguably does
not, though I concede that this is far from a slam dunk.

In any case, it's all a moot point because EOPL defines freeness in a
relative rather than the absolute sense that I was assuming. Y *does*
occur free in :

(lambda (y) (lambda (x) (f x y)))

within the context of the sub-expression (lambda (x) (f x y)). So
(lambda () y) is the function that returns Y, but one cannot assume that
the binding of Y that it returns is global and therefore unique. Which
is the point that I guess you were making from the outset.

rg

Matthias Blume

2004-09-12, 8:56 pm

Ron Garret <rNOSPAMon@flownet.com> writes:

> [ ... ] but there also isn't really any such thing as "the value of an
> expression" either,

That is false. Any operational semantics of the lambda calculus comes
with a notion of "value". The set of values is usually a subset of
all expressions. In the case of call-by-value, the set of values
consists of "flat" values (int, bool, ...) and head-normal-forms.

> On this view, (lambda () y) is the function that returns Y, or to be
> more precise, it is the function that returns the value of the global
> and therefore unique (and, I might add, in the lambda calculus,
> immutable) binding of Y.

As you said yourself, in the lambda calculus there is no global or
unique binding of Y. In fact, for the purpose of evaluation, one
usually considers closed terms only.

> FWIW, I wasn't raising this example just to be a wise guy. I had an
> actual pedagogical purpose, namely, to highlight the difference between
> "the function that returns Y" and "the value returned by the function
> that returns Y when that function is actually invoked." These are not
> the same thing, even in the lambda calculus (and certainly not in
> Scheme).

So far, so good.

> The latter clearly depends on Y, but the former arguably does
> not,

It does! Absolutely!

> though I concede that this is far from a slam dunk.

Ok, good.

Matthias

Ron Garret

2004-09-13, 3:57 am

In article <m28ybfatj3.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:

>
> It does! Absolutely!

Well, there's a constructive answer. You know, Matthias, it is
customary in civilized discourse when disagreeing with someone to
actually provide an argument in support of your position rather than
simply saying, in effect, "You're wrong. Nyah." That makes it much
easier to frame a respectful response, and helps to prevent discussions
from degenerating into flamefests.

Consider the following Scheme code:

(define y 1)
(define yf1 (lambda () y)))
(set! y 2)
(define yf2 (lambda () y)))

There is in Scheme no difference between yf1 and yf2 (other than the
implementation-dependent possibility that they are not eqv?). That is
an incontrovertible fact. Now, Scheme is not the lambda calculus, but I
nonetheless submit that this fact about Scheme makes my position about
the lambda calculus sufficiently tenable that any disagreement deserves
more support than you have provided.

rg

Matthias Blume

2004-09-13, 3:57 am

Ron Garret <rNOSPAMon@flownet.com> writes:

> In article <m28ybfatj3.fsf@hanabi.local>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
>
> Well, there's a constructive answer. You know, Matthias, it is
> customary in civilized discourse when disagreeing with someone to
> actually provide an argument in support of your position rather than
> simply saying, in effect, "You're wrong. Nyah." That makes it much
> easier to frame a respectful response, and helps to prevent discussions
> from degenerating into flamefests.

I have already explained this position before. If you snip all the
context (including the thread leading up to it), then, yes, this might
be construed as an uncivilised argument. But it wasn't.

> Consider the following Scheme code:
>
> (define y 1)
> (define yf1 (lambda () y)))
> (set! y 2)
> (define yf2 (lambda () y)))
>
> There is in Scheme no difference between yf1 and yf2 (other than the
> implementation-dependent possibility that they are not eqv?).

Right. They are also both in the scope of the same Y. The same would
be true even if you had used "define" instead of "set!" the second
time around. That's Scheme for you. If you try the same in, say,
SML, you get:

-----
$ sml
Standard ML of New Jersey v110.48 [FLINT v1.5], August 10, 2004
- val y = 1
= val yf1 = fn () => y
= val y = 2
= val yf2 = fn () => y;
val y = <hidden-value> : int
val yf1 = fn : unit -> int
val y = 2 : int
val yf2 = fn : unit -> int
- yf1 ();
val it = 1 : int
- yf2 ();
val it = 2 : int
-----

> That is an incontrovertible fact.

.... which is perfectly consistent with what I said. In fact, I
explained all this in some detail in my very first contribution to
this thread.

> Now, Scheme is not the lambda calculus, but I
> nonetheless submit that this fact about Scheme makes my position about
> the lambda calculus sufficiently tenable that any disagreement deserves
> more support than you have provided.

The problem is that your example does not support your claim. That's
all. Yes, the two lambdas are equal (modulo procedure identity). But
that is because they both share the same binding for Y. (And that is
because in Scheme variables denote locations, not values. I did
explain that. Moreover, at the Scheme toplevel all variables are
effectively pre-bound, i.e., DEFINE acts like SET!)

I'm sorry if you felt being stepped on your toes.

Matthias

PS: Erann, er, Ron, I just figured out who you are. Rather strange...

Anton van Straaten

2004-09-13, 3:57 am

Ron Garret wrote:
> Consider the following Scheme code:
>
> (define y 1)
> (define yf1 (lambda () y)))
> (set! y 2)
> (define yf2 (lambda () y)))
>
> There is in Scheme no difference between yf1 and yf2 (other than the
> implementation-dependent possibility that they are not eqv?). That is
> an incontrovertible fact. Now, Scheme is not the lambda calculus, but I
> nonetheless submit that this fact about Scheme makes my position about
> the lambda calculus sufficiently tenable that any disagreement deserves
> more support than you have provided.

The reason the lambda calculus case is different, though, is the same reason
that you can't use Scheme in support of your case.

As I think Matthias previously pointed out, in the Scheme case, the 'y' in
(lambda () y) refers to a location. In the lambda calculus case, it refers
directly to a value (perhaps more generally, a function).

So, in any context in which (lambda (x) y) has a meaning in the lambda
calculus, its meaning depends on the value of y. It's about as simple as
that (which in Matthias' defense, is probably why he wasn't providing any
more explanation than he already has).

Anton

Anton van Straaten

2004-09-13, 3:57 am

Marlene Miller wrote:
> I was trying to understand what "depends on" means. It has something to do
> with one thing changing causing another thing to change. How can we know
if
> the other thing has changed? By testing for equality. But how can we test
> for equality if the other thing changes whether or not we change y?

You're right that testing for equality in the case of procedures is
problematic.

If you're not already familiar with extensional vs. intensional equality,
you might take a look at the treatment of the subject in HTDP (not related
to procedures):
http://www.htdp.org/2001-01-18/Book/node213.htm

Also, it's instructive to read what R5RS says about equality of procedures
for "eqv?". Notice the difference between which situations must return #t,
vs. which must return #f.

The point with procedures is that extensional equality, in general, can't be
determined by testing, since it involves applying each procedure being
compared to every possible argument, and comparing all the results. Of
course, to do that all you need is infinite time. Intensional equality is
even trickier in general, requiring intelligent comparing of the semantic
content of procedures.

So, in a case like this, it's usually up to our own reasoning to determine
procedure equivalence. To determine whether a procedure has changed in this
case, you really have to either reason about it intensionally, and/or test
it extensionally. E.g. if you can demonstrate that the procedure gives
different results when you change something that it depends on, then you've
proved the dependence.

Of course, in this discussion, one question is whether the thing being
depended on is allowed to change, i.e. in lambda calculus, once y has a
value, it's not allowed to change. Which is precisely why the answer to
whether (lambda (x) y) depends on y is yes, in the case of the lambda
calculus, even though the answer for Scheme is no (at least arguably).

Anton

Matthias Blume

2004-09-13, 3:57 am

Matthias Blume <find@my.address.elsewhere> writes:

> Ron Garret <rNOSPAMon@flownet.com> writes:
>
>
> That is false. Any operational semantics of the lambda calculus comes
> with a notion of "value". The set of values is usually a subset of
> all expressions. In the case of call-by-value, the set of values
> consists of "flat" values (int, bool, ...) and head-normal-forms.

Ok, let me give a definition of "depends on" without referring to
values (or semantics, for that matter). All I assume is an equational
theory that lets us prove certain claims of the form e1 = e2 or e1 !=
e2. I will use "==" and "!==" to specify syntactic equality and
non-equality, resp.

We say that an expression e depends on a variable x iff:

There exists substitutions s1 and s2 such that all of the following is
true:

freevars(e) = domain(s1) = domain(s2)
forall y in freevars(e) . if y !== x then s1(y) == s2(y)
s1(e) != s2(e)

In English: Both s1 and s2 provide expressions to be substituted for
all the free variables of e. Moreover, s1 and s2 must agree on all
free variables of e other than x. The two substitutions, when applied
to e, yield expressions that are not equal in the equational theory.

---

Now let us prove that (lambda (x) y) depends on y:

Assuming familiar alpha-beta-based equality (or, alternatively,
alpha-beta-eta-based), it is easy to see that (lambda (x) y) depends
on y. Just pick:

s1 = { y -> 1 }
s2 = { y -> 2 }

The results of the substitutions are (lambda (x) 1) and (lambda (x)
2), respectively. These two are normal forms which are not
syntactically equal up to alpha. Therefore, they are not equal.

Matthias

Marlene Miller

2004-09-13, 3:57 am

"Anton van Straaten" <anton@appsolutions.com> wrote in message
news:ih91d.18373$az6.1556@newsread2.news.atl.earthlink.net...
> Marlene Miller wrote:
do[color=darkred]
> if
test[color=darkred]
>
> You're right that testing for equality in the case of procedures is
> problematic.
>
> If you're not already familiar with extensional vs. intensional equality,
> you might take a look at the treatment of the subject in HTDP (not related
> to procedures):
> http://www.htdp.org/2001-01-18/Book/node213.htm
>
> Also, it's instructive to read what R5RS says about equality of procedures
> for "eqv?". Notice the difference between which situations must return
#t,
> vs. which must return #f.
>
> The point with procedures is that extensional equality, in general, can't
be
> determined by testing, since it involves applying each procedure being
> compared to every possible argument, and comparing all the results. Of
> course, to do that all you need is infinite time. Intensional equality is
> even trickier in general, requiring intelligent comparing of the semantic
> content of procedures.
>
> So, in a case like this, it's usually up to our own reasoning to determine
> procedure equivalence. To determine whether a procedure has changed in
this
> case, you really have to either reason about it intensionally, and/or test
> it extensionally. E.g. if you can demonstrate that the procedure gives
> different results when you change something that it depends on, then
you've
> proved the dependence.
>
> Of course, in this discussion, one question is whether the thing being
> depended on is allowed to change, i.e. in lambda calculus, once y has a
> value, it's not allowed to change. Which is precisely why the answer to
> whether (lambda (x) y) depends on y is yes, in the case of the lambda
> calculus, even though the answer for Scheme is no (at least arguably).
>
> Anton
>

Thank you for the crystal clear explanation. And thank you for the two good
references. I stopped thinking too early. I didn't ask what it means for
procedures to be equal (although I did use equal? to try to help out).

Marlene

Ron Garret

2004-09-13, 3:57 am

In article <m2zn3uafim.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:

> Matthias Blume <find@my.address.elsewhere> writes:
>
>
> Ok, let me give a definition of "depends on"

I do not dispute that one can give a definition of "depends on" where
(lambda () y) depends on Y. But one can also give a definition of
"depends on" where it does not (e.g. Scheme semantics). Given that the
topic at hand is an exercise in a textbook whose major subject is Scheme
and not the lambda calculus it still seems to me that the issue is
legitimately debatable.

rg

Matthias Blume

2004-09-13, 9:03 am

Ron Garret <rNOSPAMon@flownet.com> writes:

> In article <m2zn3uafim.fsf@hanabi.local>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
>
> I do not dispute that one can give a definition of "depends on" where
> (lambda () y) depends on Y. But one can also give a definition of
> "depends on" where it does not (e.g. Scheme semantics). Given that the
> topic at hand is an exercise in a textbook whose major subject is Scheme
> and not the lambda calculus it still seems to me that the issue is
> legitimately debatable.

Didn't I pretty much say exactly that in my very first answer in this thread?

Matthias

David Rush

2004-09-13, 4:00 pm

Ron Garret <rNOSPAMon@flownet.com> writes:
> In article <m28ybfatj3.fsf@hanabi.local>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
> Well, there's a constructive answer. You know, Matthias, it is
> customary in civilized discourse

Have you been following the last several months of the
He-who-must-not-be-named saga? Many people are likely to have rather
less patience than usual with errors at the moment.

david rush
--
Remember: There is no Scheme underground

Ron Garret

2004-09-13, 4:00 pm

In article <m2vfei9wfd.fsf@hanabi.local>,
Matthias Blume <find@my.address.elsewhere> wrote:

> Ron Garret <rNOSPAMon@flownet.com> writes:
>
>
> Didn't I pretty much say exactly that in my very first answer in this thread?

Yes. You and Anton von Straaten both made this point before I did. And
I have acknowledged it and agreed with it several times now. What are
we arguing about?

rg

Matthias Blume

2004-09-13, 4:00 pm

Ron Garret <rNOSPAMon@flownet.com> writes:

> What are we arguing about?

Beats me.

David Rush

2004-09-17, 9:00 am

Matthias Blume <find@my.address.elsewhere> writes:
> Ron Garret <rNOSPAMon@flownet.com> writes:
> Beats me.

Where is Bill Richter when we need him?

david rush
--
Learning Scheme is like studying theoretical physics. Its the path
that may lead you to discover the true nature of things.
-- Shinji Ikari (on comp.lang.scheme)

Nic Ferrier

2004-09-17, 9:00 am

David Rush <kumo@gofree.indigo.ie> writes:

> Matthias Blume <find@my.address.elsewhere> writes:
>
> Where is Bill Richter when we need him?

Nooooooooooooooooooooooooooooooooooooooo
oooooooooooooooooooooo.

--
Nic Ferrier
http://www.tapsellferrier.co.uk

Matthias Blume

2004-09-17, 9:01 pm

David Rush <kumo@gofree.indigo.ie> writes:

> Matthias Blume <find@my.address.elsewhere> writes:
>
> Where is Bill Richter when we need him?

Who?

Bill Richter

2004-09-17, 9:01 pm

David Rush <kumo@gofree.indigo.ie> wrote

Where is Bill Richter when we need him?

:) I'm lurking for another w

or so, David. I struck out with the
big 3 (Will, MB & Shriram), but maybe someone will make a good
impression on me, show me they can distinguish a function (in the
sense of Schmidt) from a procedure. E.g. functions don't have
preferred definitions, but procedures do. So e.g. a semantic function
can have both a denotational definition and a non-denotational
definition (I posted <57189ce0.0408282200.6d7d0088@posting.google.com>
one, a mod of Stoy's Ex 13.22), but a "semantic procedure" could not.

Uh, the 1st post in this thread

me, because I don't know what
EoPL's notion of "value" in the Lambda Calculus, but Marlene's
followup question seemed easy enough:

1.21. Give an example of a lambda calculus expression in which
the same variable occurs both free and bound.

That is, it's easy in Scheme, which has constructions like `if', so:

(if x (lambda (x) x) 2 3)

the first occurrence of x is free, but the 2nd one is not. Now you
just have to remember that you can simulate things like `if' in LC,
but actually, this is even simpler:

(x (lambda (x) x))

The first occurrence of x is free, but the 2nd one is bound. Or maybe
the 2nd and 3rd occurrence of x are bound.

I apologize if the EoPL questions were settled in the thread: I
flipped through the thread real quickly & couldn't tell.

Shriram Krishnamurthi

2004-09-17, 9:01 pm

richter@math.northwestern.edu (Bill Richter) writes:

> That is, it's easy in Scheme, which has constructions like `if', so:
>
> (if x (lambda (x) x) 2 3)
>
> the first occurrence of x is free, but the 2nd one is not. Now you
> just have to remember that you can simulate things like `if' in LC,
> but actually, this is even simpler:

Still not learned to use an editor, eh.

> (x (lambda (x) x))
>
> The first occurrence of x is free, but the 2nd one is bound. Or maybe
> the 2nd and 3rd occurrence of x are bound.

Wrong.

Shriram

Nic Ferrier

2004-09-17, 9:01 pm

richter@math.northwestern.edu (Bill Richter) writes:

> but maybe someone will make a good impression on me, show me they
> can distinguish a function (in the sense of Schmidt) from a
> procedure.

That won't happen. We're all quite mad. Some of us criminally.

Save yourself and run away from here.

Bill Richter

2004-09-18, 3:57 am

Shriram Krishnamurthi <sk@cs.brown.edu> responded to me in message
news:<w7dd60k4ya0.fsf@cs.brown.edu>...

> (x (lambda (x) x))
>
> The first occurrence of x is free, but the 2nd one is bound. Or
> maybe the 2nd and 3rd occurrence of x are bound.

Wrong.

Shriram, I correctly answered Marlene's question, which you snipped:

1.21. Give an example of a lambda calculus expression in
which the same variable occurs both free and bound.

and my example (x (lambda (x) x)) is in on p 29 of F-F's mono on LC_v
<http://www.ccs.neu.edu/course/com3357/mono.ps>. If you're nailing me
on the 2nd occurrence of x not being bound, but only being a "binding
instance", as you say in PLAI, then

1) I guess I was wrong, but this distinction is not discussed in F-F,
and it's irrelevant to beta_v reduction, or beta reduction in LC, and

2) I found a problem with your substitution code in PLAI.

It'll take me a while to get there, as I'll first prove that I was
correct about Marlene's EoPL problem. From p 26 of F-F:

The relation FV maps an [LC_v] expression to a set of *free
variables* in the expression. Intuitively, x is a free
variable in the expression if it appears outside of any
(lambda (x) ...). More formally, we define the relation FV
as follows:

FV( x ) = {x}

FV( (lambda (x) M) ) = FV( M ) - {x}

FV( (M N) ) = FV( M ) union FV( N )

Examples of FV:

FV( x ) = {x}

FV( (x (y x)) ) = {x, y}

FV( (lambda (x) (x y)) ) = {y}

FV( (z (lambda (z) z)) ) = {z}

So I correctly answered Marlene's EoPL question: z is a free variable
in (z (lambda (z) z)), but z is clearly a bound variable as well.

Now let's get to the question not needed for the EoPL ex 1.21: whether
the binding instance is a bound/free variable. I'll restate:

> Or maybe the 2nd and 3rd occurrence of x in (x (lambda (x) x))
> are bound.

This is maybe an error of mine, but it's not well explained by F-F,
because it's not necessary to understand this distinction to handle LC
or LC_v. What you need to understand is how to beta_v reduce

((lambda (x) M) V) |--->_v M[x <- V]

beta_v reduction means replace every free occurrence of x in M with V.
We don't need to even define bound variables for this! So if

M = (x (lambda (x) x))

it makes no difference if the 2nd occurrence of x is bound, or the
binding instance, as you say in PLAI. We know the 2nd & 3rd
occurrence aren't free, by F-F's rules above, and that's all we need
in order to successfully beta_v reduce ((lambda (x) M) V):

M[x <- V] = (x (lambda (x) x))[x <- V] = (V (lambda (x) x))

I don't see where F-F formally define bound variables, so we can put
F-F in agreement with PLAI by saying that the first (parenthesized) x
in (lambda (x) x) is neither free nor bound, but is the "binding
instance". So for full clarity, maybe I shoulda posted:

In the LC expression
(x (lambda (x) x))
the left-most match of the variable x is free,
and the right-most match of the variable x is bound, and
the middle match of the variable x is the binding occurrence which
binds the right-most x.

Let's look at Ch 3 of PLAI, where you have a simple LC-like grammar

M in WAE
n in Z
x in Ide

M ::= n | {+ M M} | {- M M} | {{with <x> M} M}

So the big difference between your WAE (with & alg exp) and LC is that
{with <x> M} is not itself an expression in WAE. In Definition 2, you
explain that the x in <x> is the binding instance in the expression
{{with <x> M} M}
That's fine. But I'm not thrilled with your next 3 defs. It's the
sorta thing that I was always

about until I read F-F's mono:

Definition 3: The scope of the binding instance is the region of
program text in which instances of the identifier refer to the binding
instance.

Definition 4: An identifier is *bound* if it contained within the
scope of a binding instance of its name.

Definition 5: An identifier not contained within the scope of a
binding instance is free.

What these defs don't explain is what the scope is! It looks to me
like you only define scope in your code for (subst exp sub-id val),
and that's of course a good way, but I prefer F-F's approach, which is
standard in the LC literature.

But it looks to me like your definition of scope is different from the
LC_v scope, and of course that would be OK, since your language is
different, {with <x> M} not being an expression itself. But it looks
to me like you're saying substituting x with 5 in
{{with <x> M} N}
does nothing. That's what I get out of your code

(define (substitute expr sub-id val)
(cases WAE expr
...
[with bound-id named-expr bound-body
(if (symbol=? bound-id sub-id)
expr
(with bound-id named-expr
(substitute bound-body sub-id val)))]))

That's what I learn from the line "expr".

But in LC or LC_v, we'd substitute x with 5 in N. That is, in F-F's
ISWIM I posted on, we have the beta_v reductions

((lambda (x)
((lambda (x) (+ x x))
x))
5)

|--->_v

((lambda (x) (+ x x))
5)

|--->_v (+ 5 5) |--->_v 10

which is of course the answer DrScheme gives. Now it looks to me
like PLAI is saying that the WAE expression

{with x 5
{with x x
{+ x x}}}

should reduce to

{with x x
{+ x x}}

and that's fine if you want it, but it's not what Scheme or LC_v
does. In Scheme or LC_v, we should've gotten

{with x 5
{+ x x}}

I think. I looked at this for the 1st time tonight, so I apologize if
I'm getting this wrong. But it's not an editor mistake. I'm bold
because I'm waaay outta time, waaay over my deadline, so I make lots
of mistakes. I'll keep going. I don't even like the last line
of your substitute code, in case bound-id != sub-id. Here's what I
the think the fragment above should read:

(define (substitute expr sub-id val)
(cases WAE expr
...
[with bound-id named-expr bound-body
(if (symbol=? bound-id sub-id)
(with bound-id
(substitute named-expr sub-id val)
bound-body)
(with bound-id
(substitute named-expr sub-id val)
(substitute bound-body sub-id val)))]))

> That is, it's easy in Scheme, which has constructions like `if',
> so:
>
> (if x (lambda (x) x) 2 3)
>
> the first occurrence of x is free, but the 2nd one is not. Now
> you just have to remember that you can simulate things like `if'
> in LC, but actually, this is even simpler:

Still not learned to use an editor, eh.

Here you may have a point, but there is nothing wrong with my
text-editor skills. I'm an expert user of Emacs, and I'm about the
only person here who bothers to re-fill citations. So if I ever get
something wrong, it's a real error on my part.

I guess your (good) point here is that Scheme has a different notion
of free & bound variables than in LC or LC_v. As MB posted earlier in
the thread, Scheme talks about variables being bound to locations.
From R5RS:

"An identifier that names a location is called a variable and is said
to be bound to that location."

The phrase free variable doesn't occur in the text of R5RS, as one
sees with the Emacs command
(isearch-resume "free[
]" t nil t "free[ ^I^J]" t)
and the word free is not in the R5RS index.

But I know all this. What I meant is that the Scheme notion of
lexical scope (or static scope) is much the same as the LC notion of
free & bound variables. From R5RS again:

" Like Algol and Pascal, and unlike most other dialects of Lisp except
for Common Lisp, Scheme is a statically scoped language with block
structure. To each place where an identifier is bound in a program
there corresponds a region of the program text within which the
binding is visible. The region is determined by the particular
binding construct that establishes the binding; if the binding is
established by a lambda expression, for example, then its region is
the entire lambda expression. Every mention of an identifier refers
to the binding of the identifier that established the innermost of
the regions containing the use. If there is no binding of the
identifier whose region contains the use, then the use refers to the
binding for the variable in the top level environment, if any
(chapters 4 and 6); if there is no binding for the identifier, it is
said to be unbound."

The "if the binding is established by a lambda expression, for
example, then its region is the entire lambda expression" is pretty
much what I quoted from F-F. Of course it's a Scheme error to
evaluate an unbound variable, but free variables are fine in LC/LC_v.

Marlene Miller

2004-09-18, 3:57 am

"Bill Richter" <richter@math.northwestern.edu> wrote in message
> but Marlene's
> followup question seemed easy enough:
>
> 1.21. Give an example of a lambda calculus expression in which
> the same variable occurs both free and bound.
> [...]
> but actually, this is even simpler:
>
> (x (lambda (x) x))
>
> The first occurrence of x is free, but the 2nd one is bound. Or maybe
> the 2nd and 3rd occurrence of x are bound.

Thank you Bill. That's a good example.

To me, the first x and the third x are not the _same_ variable. In the
section of EoPL where this exercise occurs, they are teaching how variable
references are bound to variable declarations. Those x's are bound to
different declarations.

Maybe they meant the same _symbol_, not the same _variable_.

Shriram Krishnamurthi

2004-09-18, 3:57 am

richter@math.northwestern.edu (Bill Richter) writes:

> Shriram, I correctly answered Marlene's question, which you snipped:
>
> 1.21. Give an example of a lambda calculus expression in
> which the same variable occurs both free and bound.

Irrelevant (and I'm not going to say whether you were correct or not,
because I don't like answering textbook problems on newsgroups).

> If you're nailing me
> on the 2nd occurrence of x not being bound, but only being a "binding
> instance", as you say in PLAI, then

Yes, that's what I was doing.

> 1) I guess I was wrong, but this distinction is not discussed in F-F,
> and it's irrelevant to beta_v reduction, or beta reduction in LC, and

In order: yes, their-problem-not-mine, irrelevant (ie, its irrelevancy
is irrelevant), irrelevant.

> 2) I found a problem with your substitution code in PLAI.

This will be fun.

> I don't see where F-F formally define bound variables, so we can put
> F-F in agreement with PLAI by saying that the first (parenthesized) x
> in (lambda (x) x) is neither free nor bound, but is the "binding
> instance".

We can, indeed, assuming your claims about F-F's lack of definition
are valid.

> Let's look at Ch 3 of PLAI, where you have a simple LC-like grammar
>
> M in WAE
> n in Z
> x in Ide
>
> M ::= n | {+ M M} | {- M M} | {{with <x> M} M}

I have no such grammar. Your version of the WITH expression does not
appear anywhere in the book. If you want to make up your own
language, fine, but please don't ascribe it to my book -- it'll only
confuse other readers.

> So the big difference between your WAE (with & alg exp) and LC is that
> {with <x> M} is not itself an expression in WAE.

{with <x> M} isn't a term in the LC either.

> I'm not thrilled with your next 3 defs.
> [...]
> What these defs don't explain is what the scope is!

That's exactly right.

> It looks to me
> like you only define scope in your code for (subst exp sub-id val),

Precisely. If I do it purely mathematically,

(a) it would be too complicated for the average student to follow, and

(b) it would still not be executable code, and something might go
wrong in the translation of the mathematical definition to code.

By defining it procedurally, I claim to minimize the first problem and
I obviously eliminate the second.

> and that's of course a good way, but I prefer F-F's approach, which is
> standard in the LC literature.

Fine, but why are you telling me this?

1. I'm not writing a book on the LC, so I don't see why I should care
about what is "standard in the LC literature".

2. It is fairly "standard" to offer procedural representations of
definitions in the LC literature.

3. If a student asked me for a more notational presentation I would
refer them to other works.

4. Standardization has its di

vantages, too.

5. I'm not out to copy other books.

> But it looks to me like your definition of scope is different from the
> LC_v scope, and of course that would be OK, since your language is
> different, {with <x> M} not being an expression itself. But it looks
> to me like you're saying substituting x with 5 in
> {{with <x> M} N}
> does nothing. That's what I get out of your code
>
> (define (substitute expr sub-id val)
> (cases WAE expr
> ...
> [with bound-id named-expr bound-body
> (if (symbol=? bound-id sub-id)
> expr
> (with bound-id named-expr
> (substitute bound-body sub-id val)))]))
>
> That's what I learn from the line "expr".

First of all, this is not exactly code from my book. The code you've
presented (and I'm not talking about the elision) isn't even
syntactically correct.

More to the point, you're making a gigantic ass of yourself.

For the reader following along at home, here's the deal. Richter
begins to read chapter 3 of my book. He gets through the preface,
through 3.1 (Defining Substitution), sees 3.2 (Interpreting With, pg
20), and stops right there. What he fails to do is turn over to the
next page (pg 21), where section 3.3 (The Scope of with Expressions)
begins. In a matter of two pages (21 and 22), the book addresses,
with examples, all the problems that Richter identifies.

As someone who felt the book did not adequately describe the scope of
WITH expressions, one would think Richter would have at least glanced
at section 3.3. He would not have to go very far to realize something
was fishy. The very first sentence [which makes more sense in
context] is,

Actually, maybe not. In fact, many of these test cases result in
free identifier errors! What gives?

To your credit, Bill, you did figure out that the code is wrong. To
your discredit, you didn't think to turn a page before posting a 250+
line message. To your embarassment, the next page addressed
everything in your message.

> Here you may have a point, but there is nothing wrong with my
> text-editor skills. I'm an expert user of Emacs

Since you've never understood the point I've been making every time
I've accused you of lacking text-editor skills, let me explicate.

You seem to think of a newsgroup as a publication medium for
stream-of-consciousness messages. It never occurs to you that your
reader's time might be valuable, so you ought to be considerate and
prune your messages. In particular, if you make a mistake, or find a
better answer, that you should use your TEXT EDITOR to go back up,
delete the previous prose, and replace it with the corrected or
improved prose. Oh no: you just keep appending along in a stream, as
if you were operating in Unix mail or rn sans editor.

Your expertise in Emacs ain't worth a hill o' beans if you can't use
it to edit your prose.

[Fyi, I re-read this post three times, and made many edits, before
sending it out.]

> I guess your (good) point here is that Scheme has a different notion
> of free & bound variables than in LC or LC_v.

I haven't made that claim anywhere.

Shriram

Bill Richter

2004-09-18, 8:56 pm

"Marlene Miller" responded to me in message
news:<gLO2d.603627$Gx4.107854@bgtnsc04-news.ops.worldnet.att.net>...

> 1.21. Give an example of a lambda calculus expression in
> which the same variable occurs both free and bound.
>
> (x (lambda (x) x))
>
> The first occurrence of x is free, but the 2nd one is bound. Or
> maybe the 2nd and 3rd occurrence of x are bound.

Thank you Bill. That's a good example.

Thanks, Marlene, and I see it's almost identical to what you
originally posted yourself:

My answer is ((lambda (x) x) x). But as I see it, the bound
variable x and the free variable x are not the same variable.

I apologize for missing that. I saw your post before posting mine,
but I mis-parsed your answer, and didn't see that the 3rd x was free.

To me, the first x and the third x are not the _same_ variable. In
the section of EoPL where this exercise occurs, they are teaching
how variable references are bound to variable declarations. Those
x's are bound to different declarations.

Maybe they meant the same _symbol_, not the same _variable_.

These are interesting questions, but I can't say much, as I don't have
a copy of EoPL, and maybe I'm not an expert in this stuff. But these
are not Lambda Calculus (LC) questions. Ex 1.21 is an LC question,
and in LC, variable and symbol mean the same thing. Presumably EoPL
is trying to explain that LC sheds some light on real languages like
Scheme. And I think that's true, because Scheme's lexical (or static)
scope is pretty well explained by the LC notions of free & bound
variables. Actually I didn't explain bound variables last post,
following F-F, who just give one example, but it's this:

If the variable x occurs freely in the LC expression M, then this
occurrence of x is bound in the LC expression
(lambda (x) M),
and is bound to (or maybe by) the parenthesized x, and this x (right
after lambda) is called the binding occurrence.

But you barely need to know this in LC. What you need to know in LC
in beta & alpha reduction, and they both have to do with substituting
free variables. I did beta_v reduction before, and alpha is similar:

If the variable y does not occur freely in the LC expression M, then
(lambda (x) M)
is said to be alpha equivalent to the LC expression
(lambda (y) M[x <- y])
where M[x <- y] is the result of replacing all free occurrences of x in
M with y.

So F-F are OK: it's only necessary to define free variables.

Now Marlene, the whole rest of the thread went right by me. The
original question (not yours) was an LC question which I didn't
understand, but the thread seemed to be mostly about Scheme.

Bill Richter

2004-09-18, 8:56 pm

Shriram Krishnamurthi <sk@cs.brown.edu> responded to me in message
news:<w7disacnpuo.fsf@cs.brown.edu>...

> Shriram, I correctly answered Marlene's question, which you snipped:
>
> 1.21. Give an example of a lambda calculus expression in
> which the same variable occurs both free and bound.

Irrelevant (and I'm not going to say whether you were correct or
not, because I don't like answering textbook problems on
newsgroups).

I'll say it, Shriram, I was right, and Marlene gave the correct answer
as well in the 3rd post in the thread, where it got buried. But yes:
it's probably better to ask questions, as Will did once in the thread.

> If you're nailing me on the 2nd occurrence of x not being bound,
> but only being a "binding instance", as you say in PLAI, then

Yes, that's what I was doing.

Great, I understood you. And I understood something else too: I
realized your original code was using non-Scheme-like scope, and the
fix I posted is pretty much identical to your fix on p 23, and partly
that shows I'm learning something, but mainly it shows that your scope
rules for WAE are in line with Scheme and LC. That's great!

So that's it for my response, but let me answer some points anyway.
That's a great joke "(ie, its irrelevancy is irrelevant)".

> Let's look at Ch 3 of PLAI, where you have a simple LC-like
> grammar
>
> M in WAE
> n in Z
> x in Ide
>
> M ::= n | {+ M M} | {- M M} | {{with <x> M} M}

I have no such grammar. Your version of the WITH expression does
not appear anywhere in the book. If you want to make up your own
language, fine, but please don't ascribe it to my book -- it'll
only confuse other readers.

Thanks, I see I goofed, I typo-ed the with expression, and left off
the last <ide> production, so I should've written

M ::= n | {+ M M} | {- M M} | {with {<x> M} M} | x

I hope you're not carping that I didn't write exactly what you wrote,
but if so, let me type the PLAI BNF for WAE verbatim:

WAE ::= <num> | {+ <WAE> <WAE>} | {- <WAE> <WAE>}
| {with {<x> <WAE>} <WAE>} | <x>

I rewrote your BNF in the way Schmidt explains in his Thm 3.13.

> So the big difference between your WAE (with & alg exp) and LC is that
> {with <x> M} is not itself an expression in WAE.

{with <x> M} isn't a term in the LC either.

Right, I blew that, even not counting my typo. I

your
language with a Stoy dynamic scope language in Ch 3.13, where he has
expressions ((lambda (x) M) P), but (lambda (x) M) is not an
expression itself. But I blew the translation, which really goes:

((lambda (x) M) P) <-----> {with {<x> P} M}

So we can't read off in your WAE expression the secret lambda exp.

> I'm not thrilled with your next 3 defs.
> [...]
> What these defs don't explain is what the scope is!

That's exactly right.

Great!

> It looks to me like you only define scope in your code for (subst
> exp sub-id val),

Precisely. If I do it purely mathematically [...]

Yeah, as I said, the way you did it's fine, but I like the LC/LC_v
approach also.

> But it looks to me like your definition of scope is different
> from the LC_v scope, and of course that would be OK, since your
> language is different, {with <x> M} not being an expression
> itself. But it looks to me like you're saying substituting x
> with 5 in
> {{with <x> M} N}
> does nothing. That's what I get out of your code
>
> (define (substitute expr sub-id val)
> (cases WAE expr
> ...
> [with bound-id named-expr bound-body
> (if (symbol=? bound-id sub-id)
> expr
> (with bound-id named-expr
> (substitute bound-body sub-id val)))]))
>
> That's what I learn from the line "expr".

First of all, this is not exactly code from my book. The code
you've presented (and I'm not talking about the elision) isn't even
syntactically correct.

OK, thanks, & I the problem is that I don't understand your syntax. I
should learn. I see some typos, here's my correction:

(define (subst expr sub-id val)
(cases WAE expr
...
[with (bound-id named-expr bound-body)
(if (symbol=? bound-id sub-id)
expr
(with bound-id named-expr
(subst bound-body sub-id val)))]))

For the reader following along at home, here's the deal. Richter
begins to read chapter 3 of my book.

That's not even right! I printed out your whole book a few months
ago, and I noted that you talked about substitution, so I just tried
to find it. So I didn't even start in chapter 3 :^0

He gets through the preface, through 3.1 (Defining Substitution),
sees 3.2 (Interpreting With, pg 20), and stops right there. What
he fails to do is turn over to the next page (pg 21), where section
3.3 (The Scope of with Expressions) begins. In a matter of two
pages (21 and 22), the book addresses, with examples, all the
problems that Richter identifies.

As someone who felt the book did not adequately describe the scope
of WITH expressions, one would think Richter would have at least
glanced at section 3.3. He would not have to go very far to
realize something was fishy. The very first sentence [which makes
more sense in context] is,

Actually, maybe not. In fact, many of these test cases result in
free identifier errors! What gives?

To your credit, Bill, you did figure out that the code is wrong.

And I fixed it correctly too!

To your discredit, you didn't think to turn a page before posting a
250+ line message. To your embarrassment, the next page addressed
everything in your message.

Ooops!

> Here you may have a point, but there is nothing wrong with my
> text-editor skills. I'm an expert user of Emacs

Since you've never understood the point I've been making every time
I've accused you of lacking text-editor skills, let me explicate.

You seem to think of a newsgroup as a publication medium for
stream-of-consciousness messages. It never occurs to you that your
reader's time might be valuable, so you ought to be considerate and
prune your messages. In particular, if you make a mistake, or find
a better answer, that you should use your TEXT EDITOR to go back
up, delete the previous prose, and replace it with the corrected or
improved prose. Oh no: you just keep appending along in a stream,
as if you were operating in Unix mail or rn sans editor.

That's not quite true. I usually do a bunch of editing, and I usually
flush out a number of errors in the process. And I always try to cut
'n paste the most interesting part to the top, so the reader doesn't
have to wade through tons of fluff before getting to the good part.

[Fyi, I re-read this post three times, and made many edits, before
sending it out.]

Perhaps you exceed me there. I do always run the spell-checker, and I
usually flag mispelled words by the person I'm responding to, like
your `embarassment', which as you see I corrected above. I do always
"preview message" in Google, which uses a fixed width font, and Emacs
has a variable width font, so that flushes out some errors too.

> I guess your (good) point here is that Scheme has a different notion
> of free & bound variables than in LC or LC_v.

I haven't made that claim anywhere.

Then I don't know what you flagged me on then, but it's not important.
I only brought in Scheme because Scheme has both lexical scoping and
multi-argument constructions like `if'. I wasn't trying to assert
anything about Scheme in my original post.

Marlene Miller

2004-09-19, 3:56 am

"Bill Richter" <richter@math.northwestern.edu> wrote in message

> Ex 1.21 is an LC question, and in LC, variable and symbol mean the same
thing.

> If the variable x occurs freely in the LC expression M, then this
> occurrence of x is bound in the LC expression
> (lambda (x) M),
> and is bound to (or maybe by) the parenthesized x, and this x (right
> after lambda) is called the binding occurrence.

Some people say a variable is bound to a value. Some people say a variable
is bound to a location. Some people say a variable is a location. In section
1.3.1, a variable reference is bound by a declaration.

Thank you Bill. Now I have a better understanding of why this other usage of
variable and binding exist.

Bill Richter

2004-09-19, 8:59 pm

"Marlene Miller" responded to me in message
news:<o883d.607399$Gx4.231067@bgtnsc04-news.ops.worldnet.att.net>...

> Ex 1.21 is an LC question, and in LC, variable and symbol mean
> the same thing.

> If the variable x occurs freely in the LC expression M, then this
> occurrence of x is bound in the LC expression
> (lambda (x) M),
> and is bound to (or maybe by) the parenthesized x, and this x
> (right after lambda) is called the binding occurrence.

Some people say a variable is bound to a value. Some people say a
variable is bound to a location. Some people say a variable is a
location.

But this is all Scheme talk, Marlene. (R5RS says the 2nd, and I think
that's the right way to handle mutation.) For the EoPL LC exercises,
you