Home

Lambdascope

Lambdascope:
Another optimal implementation of the lambda-calculus

We have presented an implementation of the lambda-calculus
in the spirit of the calculational approach [...], and which
is fully in the traditions of calculi with explicit substitution
and of graph implementations of term rewriting. As far as
we know it is the first such calculus which is optimal in the sense of Levy. Moreover, as far as we know this is the
first optimal calculus featuring only a single scope delimiter
node instead of the usual two, croissants and brackets,
which by force eliminates the problems which are caused by
having more than one scope node [...]. The calculus
is simple, half a page suffices [...] to describe
it, and completely reduction-based (no semantic read-back
in the implementation). As a consequence it can be trivially
implemented in any (modern) programming language.

Remembering our discussion on atoms of PLs (such as scope and name), I decided this paper might be of interest.

By Andris Birkmanis at 2005-04-30 07:25 | Lambda Calculus | other blogs | 12566 reads

Comment viewing options

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

Very much of interest

Based on a first glance, I'm dubious about whether the authors can really claim to be ...fully in the traditions of calculi with explicit substitution... given the fact that they seem to be depending upon modelling rackets and croissants in their term calculus, but I'm very pleased to see a paper tackling the readback problem in an apparently clean manner.

More to follow, but I'm in the middle of the refereeing crunch for SD05, so it will have to wait a fair while...

By Charles A Stewart at Sat, 2005-04-30 18:39 | login or register to post comments

Any Uses?

Has anyone seen any uses of optimal reduction?

This scheme is the simplest so far (and avoids the croissant pileup of some earlier schemes). You would figure it would open up some new applications.

By q37 at Sun, 2005-05-01 00:06 | login or register to post comments

I'm Trying...

...to understand whether or not it has applications to this post from Tim Sweeney.

By Paul Snively at Tue, 2005-06-28 20:37 | login or register to post comments

Explicit substitution for graphs

Explicit substitution for graphs is a 5 page introduction to the material in Lambdascope by one of the authors.

By chance, has anyone come accross an interesting example of a hard interaction, mentioned in Yves Lafont's Introduction to interaction nets ?

By Christian Cl at Mon, 2005-05-02 22:08 | login or register to post comments