Home » forums » LtU Forum

Eta-expansion of abstractions outside the lambda-calculus

I've been reading up on multi-stage programming recently and came accross Eta-expansion does The Trick which interests me because partial evaluation is something I think deserves higher visibility in programming in general.

I've seen η-expansion in the context of the various λ-calculi before but I can't seem to translate this to algol style languages. I must be missing something trivial or obvious. Could anyone please enlighten me?

By Daniel Slaney at 2007-01-08 12:10 | LtU Forum | previous forum topic | next forum topic | other blogs | 5405 reads

Comment viewing options

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

Suppose we've got an

Suppose we've got an imperative language in named style (where every side-effecting expression gets its own name):

e ::= n | x | e = e | e + e | etc. (only pure expressions go here)

c ::= e | !e | ref(e) | e := e' | let x = c1 in c2

Here, !e dereferences a pointer, ref(e) allocates a new pointer pointing to e, and e := e' evaluates e to a pointer value, and then updates it with e'. let x = c1 in c2 evaluates c1, binds its result to the variable x, and then evaluates c2.

This language is extremely close to being in monadic style, and in fact that's the idea that gives the eta-expansion rule for it:

c == let x = c in x

We also have a beta-rule for this language:

let x = e in c ==  c[e/x]

and also a commuting conversion:

let x = (let y = c1 in c2) in 
c3

== 

let y = c1 in 
let x = c2 in 
c3

By neelk at Mon, 2007-01-08 15:35 | login or register to post comments

Let me see if I have this right...

So you simply wrap a function around the statement/command?

If you were using a language without inferred types would the enclosing function have to bind the free variables of c?

I can see what you mean by the monadic comment from the code examples. Reminds me of Monad Laws in do notation.

Thanks for the information.

By Daniel Slaney at Mon, 2007-01-08 22:28 | login or register to post comments

There are no functions in

There are no functions in the little language I sketched out. The eta rule is exactly the observation that let x = c in x and c compute the same thing. So in C, this would be the equivalence of:

int x = expression;
return x;

compared to 

return expression;

By neelk at Tue, 2007-01-09 01:53 | login or register to post comments

Thanks again.

Thanks again.

By Daniel Slaney at Tue, 2007-01-09 08:58 | login or register to post comments