Home » forums » LtU Forum

implementing by-value reduction in lambda calculus

Greetings,

I am having trouble wrapping my head around by-value substitution in lambda calculus. To try to warm up to lambda calculus I wrote a reducer, which works for leftmost outermost evaluation. However, when I tried to implement by-value it seemed to work fine, accept in a situation where by-value should have failed. Instead I get the same reduction as if I were using the left-outermost substitution (which in this case should succeed). I am using the definition given in Sestoft, Peter's "Demonstrating Lambda Calculus Reduction." Given this occurrence of an error, I am led to the conclusion that either (1) I got lucky on left-outermost reduction or (2) I am missing something on by-value reduction.

I would greatly appreciate any feedback or advice that this community can give.

Sincerely,

Jon

By jdgallag at 2009-02-28 21:23 | LtU Forum | previous forum topic | next forum topic | other blogs | 7767 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Don't reduce under lambda

If you're getting the same result as left-outermost reduction, a likely reason is that you're "reducing under lambda" in both cases. However, in the by-value case, you shouldn't reduce inside lambda expressions until you're actually applying them to arguments, whereas for normal order reduction, you reduce inside lambdas regardless of whether they're applied to arguments.

If that's not the answer, try examining the steps of a reduction that doesn't give the right results and comparing it to the reduction steps obtained from a tool like Sestoft's online LC reducer.

By Anton van Straaten at Sun, 2009-03-01 00:01 | login or register to post comments

sorry if this sounds dumb

What do you mean by "you're not reducing under lambda"?

By jdgallag at Sun, 2009-03-01 20:40 | login or register to post comments

Reducing lambda bodies

"Reducing under lambda" refers to applying reductions to a lambda body, i.e. to the expression within a lambda expression. So in the lambda expression (\x.M), reducing under lambda means reducing the expression M. I used the phrase because Sestoft uses it throughout the paper you mentioned, although on checking the paper I notice he doesn't ever define it.

In by-value reduction, lambda bodies are not reduced unless and until a lambda expression is applied to arguments; so if a lambda expression is never applied to arguments, its body should never get reduced.

By Anton van Straaten at Mon, 2009-03-02 00:02 | login or register to post comments

call-by-name and call-by-value

If you're implementing call-by-name and call-by-value, both of which just reduce to weak normal form, then you don't need to ever reduce under lambdas. If you get to something like \x.(\y. A) B and you continue reducing "under the lambda" to \x.A[y->B], etc., then you're going to head normal form. If you use call-by-name and continue reducing under lambdas, that's called normal order reduction. Whether you use call-by-name or call-by-value (whether you reduce arguments before substituting) is really an orthogonal issue to whether you continue to normal form. [Oops, this is all in the paper you're reading, so nm]

The problem you're having should be pretty trivial to debug - just print a trace of reductions when you try to reduce a term that should diverge under call-by-value, like (\xy.y)((\x.x x)(\x.x x)).

By Matt M at Mon, 2009-03-02 17:17 | login or register to post comments

Applicative

I don't know that I've ever heard a name given to call-by-value that continues to normal form

It's applicative order reduction, which is usually defined as reducing the leftmost-innermost redex first. Of course that's confusing because call-by-value functional languages are often called "applicative", so to be explicit you'd say "applicative order reduction to normal form", which is what the Sestoft paper mentioned in the topic does (in sec. 7.4).

By Anton van Straaten at Mon, 2009-03-02 18:55 | login or register to post comments

okay so

This is another point I might be struggling with. Is it the case that call-by-name is the same as leftmost-outermost reduction? It appears that there are different variants of call-by-name.

By jdgallag at Mon, 2009-03-02 18:28 | login or register to post comments

Reductions

1. Leftmost-outermost reduction with no restrictions is "normal order reduction to normal form" (see sec. 7.2 of Sestoft's paper).

2. Leftmost-outermost reduction which does not "reduce under lambda", i.e. doesn't reduce lambdas that haven't been applied to arguments, is call-by-name reduction (sec. 7.1). More precisely, it's call by name reduction to weak head normal form - the normal form it can reach is restricted by the limitation of not reducing under lambda.

3. Leftmost-innermost reduction which doesn't reduce under lambda is call-by-value reduction (sec. 7.3) Reduction in this case reaches weak normal form.

What I assumed from your original posting was that you were originally doing (1), and that in trying to do (3) you were in fact still reducing under lambda, which would explain how you manage to get the same results as (1).

By Anton van Straaten at Mon, 2009-03-02 18:54 | login or register to post comments

leftmost-outermost

In the paper you're reading (assuming it's this one), it looks like call-by-name and leftmost-outermost reduction are being used synonymously and without implying that evaluation should stop at a particular normal form (ie neither term implies whether evaluation under lambdas should occur).

(FYI, you should use 'reply' when responding to a particular post)

By Matt M at Mon, 2009-03-02 18:56 | login or register to post comments