parsing lambda calculus
Author Message
parsing lambda calculus

Andre> Lf.(Ly.yx)((Lyz.y(yz)) f)

Andre> wherein I use L for lambda and of course Lyz is shorthand for Ly.Lz

Andre> What does the expression beta reduce to?

Andre> (What's behind the question is to get at how the rule regarding
Andre> application binding tighter than abstraction is applied when parsing
Andre> complicated expressions).

2 notes: (1) the convention is that the body of a lambda extends as far as
possible, so, in your example, any reduction will take place within the
outermost Lf.  (2) the x in (Ly.yx) is a free variable.
So the reduction is (unless I make a dumb mistake):

Lf.(Ly.yx)((Lyz.y(yz)) f)
-> Lf.((Lyz.y(yz)) f)x
-> Lf.(Lz.f(fz))x
-> Lf.f(fx)

Hope this helps.
--Greg
--
----------------------------------------------------------------------------
| Greg Sullivan,  17 Cullinane Hall               Phone:(617)373-8685(w),    |
| College of Computer Science,                          (617)964-7699(h),    |
| Northeastern University                               (617)373-5121(fax)   |

|____________________________________________________________________________

Wed, 26 Feb 1997 21:37:02 GMT
parsing lambda calculus
I have a question regarding the parsing of lambda calculus
expressions.  As far as I know there's no lambda calculus mailing
list, so hopefully this list is close enough.

Here's the expression:

Lf.(Ly.yx)((Lyz.y(yz)) f)

wherein I use L for lambda and of course Lyz is shorthand for Ly.Lz

What does the expression beta reduce to?

(What's behind the question is to get at how the rule regarding
application binding tighter than abstraction is applied when parsing
complicated expressions).

Thanks.
--

Wed, 26 Feb 1997 20:39:51 GMT
parsing lambda calculus
Andre> Hmm.  Well, I got the same result you got, but I had never heard of
Andre> the "convention" you mention. The word convention makes me nervous.
Andre> I'd like to think things are more rigorous than to be based on a
Andre> convention.  I'd like to think the parsing of lambda calculus is a
Andre> well defined art with parsing rules just like Boolean algebra has
Andre> (i.e. AND binds tighter than OR).

Andre> Maybe it's just a matter of how you wish to think about things, but I
Andre> think using the rule: "application binds tighter than abstraction"
Andre> [Gunter 92: Semantics of Programming Languages] subsumes the
Andre> convention you cited.

Actually, the paragraph in Gunter you cite starts with the sentence "To keep
the number of parentheses at a minimum we employ several standard parsing
conventions."  I.e. there is no ambiguity in the parsing of the lambda
calculus, if the syntax for application is "(M M)", but it is useful for human

My phrasing, "the body of a lambda extends as far as possible", is, I believe,
the same as Gunter's (more precise) phrasing, "application binds more tightly
than abstraction".  Correct me if I'm wrong.

--Greg
--
----------------------------------------------------------------------------
| Greg Sullivan,  17 Cullinane Hall               Phone:(617)373-8685(w),    |
| College of Computer Science,                          (617)964-7699(h),    |
| Northeastern University                               (617)373-5121(fax)   |

|____________________________________________________________________________

Fri, 28 Feb 1997 09:39:33 GMT
parsing lambda calculus

[. . .]

Thanks for the response--much appreciated.

Quote:
>2 notes: (1) the convention is that the body of a lambda extends as far as
>possible, so, in your example, any reduction will take place within the
>outermost Lf.

Hmm.  Well, I got the same result you got, but I had never heard of
the "convention" you mention. The word convention makes me nervous.
I'd like to think things are more rigorous than to be based on a
convention.  I'd like to think the parsing of lambda calculus is a
well defined art with parsing rules just like Boolean algebra has
(i.e. AND binds tighter than OR).

Maybe it's just a matter of how you wish to think about things, but I
think using the rule: "application binds tighter than abstraction"
[Gunter 92: Semantics of Programming Languages] subsumes the
convention you cited.

--

Fri, 28 Feb 1997 04:42:28 GMT
parsing lambda calculus

[. . .]

Thanks for the response--much appreciated.

>2 notes: (1) the convention is that the body of a lambda extends as far as
>possible, so, in your example, any reduction will take place within the
>outermost Lf.

Hmm.  Well, I got the same result you got, but I had never heard of
the "convention" you mention. The word convention makes me nervous.
I'd like to think things are more rigorous than to be based on a
convention.  I'd like to think the parsing of lambda calculus is a
well defined art with parsing rules just like Boolean algebra has
(i.e. AND binds tighter than OR).

Maybe it's just a matter of how you wish to think about things, but I
think using the rule: "application binds tighter than abstraction"
[Gunter 92: Semantics of Programming Languages] subsumes the
convention you cited.

I agree with you in that it is not a matter of conventions of how to do
the reductions but a matter of conventions of how to write the
expressions.  There is no fixed standard for the latter, and different
authors use different notations.  The one I like best goes as follows:

Let \ stand for ``lambda''. Furthermore, let V* be an infinite
enumerable set of ``variables''.  The following production rules
produce the grammar of lambda expressions:

start symbol: E

(i)     E => x               where x in V*                   (variable)
(ii)    E => \x.E    where x in V*                   (abstraction)
(iii)   E => (E E)                                   (combination)

This is sufficient, but for convenience you can add the relaxation
rules:

E => (L)
L => E E
L => L E

and the identity:

(E1 E2 ... En) == (( ... (E1 E2) ...) En)

With this syntax there is only one parse-tree for every
lambda-expression, which excludes any ambiguities.  (Note that there
are no parenthesis involved in the rule for abstractions.)

The problem of which beta-redex to choose while doing reductions is a
totally unrelated problem.  It is known that leftmost-outermost
reduction (i.e. ``normal order'' evaluation) always arrives at a
normal form (provided there is one).  Normal forms are uniquely
determined up to alpha-conversion (renaming of bound variables).

This property might lead some of us to the conclusion, that normal
order evaluation is some kind of convention.  Interestingly, it is
quite the opposite: most real programming languages use call-by-value,
which is strongly related to ``applicative order evaluation''
(rightmost innermost reduction).  Only few very-high-level modern
functional languages use lazy (normal order) evaluation.

BTW, Scheme uses applicative order evaluation (call-by-value).

--
-Matthias

Fri, 28 Feb 1997 05:47:15 GMT

 Page 1 of 1 [ 5 post ]

Relevant Pages