Scheme - Local declarations in lambda calculus

Author

Local declarations in lambda calculus

Gangadhar

2006-12-11, 7:18 pm

All,
I am trying to learn lambda calculus, and am referring to this site:
http://www.csse.monash.edu.au/~lloy...eFP/Lambda/Ch/. Specifically,
in this page
http://www.csse.monash.edu.au/~lloy...h/01.Calc.html,
the author tries to explain how local variables and definitions can be
written in Lambda Calculus. Quoting the page,
let x=e in f in the particular language can be translated to (lambda
x.f)e. The value of e is assigned to x by applying the normal order of
evaluation and beta reduction, in that order. The next statement
regarding multiple local variable declarations has stumped me a little.
I was able to evaluate it to a certain level, and then I am unable to
figure out how to proceed next. Can someone please help me out.
The author uses hd - to get the head of the list, and tl to get the
tail of a list.
Here is the evaluation of the multiple local variables:
let x=e, y=f in g
The author converts the above into this lambda calculus expression:
(lambda xy. (lambda x. lambda y. g) (hd xy) (tl xy)) (e::f)
Evaluating using the normal order of evaluation, this becomes:
(lambda x. lambda y.g)(hd e::f)(tl e::f)
After this, I think normal order of evaluation should be applied to the
expression before the actual beta reduction happens. The next steps in
the evaluation are something I am unable to evaluate.
I couldn't find a group for lambda calculus and hence am posting it
here (and also because I have started learning scheme).

Thank You
Gangadhar

Marlene Miller

2006-12-11, 7:18 pm

Gangadhar wrote
> Here is the evaluation of the multiple local variables:
> let x=e, y=f in g
> The author converts the above into this lambda calculus expression:
> (lambda xy. (lambda x. lambda y. g) (hd xy) (tl xy)) (e::f)
>Evaluating using the normal order of evaluation, this becomes:
>(lambda x. lambda y.g)(hd e::f)(tl e::f)
>After this, I think normal order of evaluation should be applied to the
>expression before the actual beta reduction happens. The next steps in
>the evaluation are something I am unable to evaluate.

(define e 1) (define f 2) (define g 3)
(let ((x e) (y f)) g) => 3
((lambda (x y) g) e f) => 3
(((lambda (x) (lambda (y) g)) e) f) => 3

I would evaluate the last expression this way:

1 Evaluate ((lambda (x) (lambda (y) g)) e) and f
1.1 Evaluate (lambda (x) (lambda (y) g)) and e
1.2 Apply function to val-e
1.2.1 Bind x to val-e
1.2.2 Evaluate (lambda (y) g)
2 Apply function to val-f
2.1 Bind y val-f
2.2 Evaluate g

Marlene Miller

2006-12-11, 7:18 pm

>(lambda x. lambda y.g)(hd e::f)(tl e::f)

I think the way this is evaluated is

1. beta reduction. replace all free occurrences of x in lambda y. g with e
(lambda y.g) (tl e::f)

2. beta reduction. replace all free occurrences of y in g with f
g

Gangadhar

2006-12-11, 7:18 pm

Marlene Miller wrote:
>
> I think the way this is evaluated is
>
> 1. beta reduction. replace all free occurrences of x in lambda y. g with e
> (lambda y.g) (tl e::f)
>
> 2. beta reduction. replace all free occurrences of y in g with f
> g
Thank you Marlene. That helped me to understand how the evaluation
happens. The statement
(lambda x. lambda y.g) (hd e::f) (tl e::f) sort of put me off track in
terms of evaulation. If the same was given as (lambda x (lambda y.g))
(hd e::f)(tl e::f), may be the beta reduction would have become a
little easier to understand [that indeed is the way the beta reduction
happens isn't it ?]. I didn't take a look at the scheme code yet, will
do once I get my head around lambda calculi. Thank you.

Regards
Gangadhar

Marlene Miller

2006-12-11, 7:18 pm

"Gangadhar" wrote in message:
> Marlene Miller wrote:
with e[color=darkred]
> Thank you Marlene. That helped me to understand how the evaluation
> happens.

I guess you noticed in 1. there were not any free occurrences of x in lambda
y.g . Therefore e did not replace any x's. Similarly in 2. there were not
any free occurrences of y in g. Therefore f did not replace any y's.

> The statement
> (lambda x. lambda y.g) (hd e::f) (tl e::f) sort of put me off track in
> terms of evaulation. If the same was given as (lambda x (lambda y.g))
> (hd e::f)(tl e::f), may be the beta reduction would have become a
> little easier to understand

They say
lambda x1 ... xn . M
is an abbreviation for
lambda x1 (lambda x2 (... (lambda xn (M)) .. ))

Therefore, I assume (lambda x . lambda y . g) means (lambda x (lambda y
(g)))

> [that indeed is the way the beta reduction
> happens isn't it ?].

One (general PL) book I have explains beta reduction this way...

For any lambda abstraction lambda x . e and any expression M, we say
(lambda x . E) M --->beta E[M\x]
where E[M\x] denotes the expression E with all free occurrences of x
replaced by M.

That book also says...
Beta reduction is not permitted if any free variables in M would become
bound in E[M\x].

To understand that last sentence, we need to look elsewhere...
http://www.cs.ru.nl/E.Barendsen/ond...iaal/lambda.pdf
See Definition 2.4(iii) on page 10.

(Note one of the authors is Henk Barendregt. Introduction to Lambda Calculis
is not his Lambda Calculus (1981 or 1991).)

> I didn't take a look at the scheme code yet, will
> do once I get my head around lambda calculi. Thank you.

That's okay. What I know about lambda calculus is about 3 more paragraphs
than you know. Therefore, I used Scheme instead, hoping you could translate
and figure out that binding is related to substitution. I can also verify
what I say by executing the expression in an interactive interpreter.

The above mentioned book has a nice example of a sequence of beta-reductions
for this
(lambda f . lambda g . lambda h . f g (h h)) (lambda x . lambda y . x) h
(lambda x . x x)
I'll reproduce it, if it will help you.

Marlene

Sponsored Links