Home

Lambda Animator

Lambda Animator from Mike Thyer is a tool for displaying and experimenting with alternate reduction strategies in the LC. The tool can use a number of reduction strategies, including completely lazy evaluation.

The tool can be invoked in several different modes (via JWS or as an applet), and contains many examples, and the documentation provides clear definitions of the sometime confusing terminology in the field.

Notice that the "step" and "run" buttons only work when rendering new graphs, which only works if you are running in trusted mode and have Graphviz installed. Otherwise you'll have to use the the up/down cursor keys or the scroll bar to review already rendered graphs (which exist for all the examples).

The site list relevant papers and dissertations.

By Ehud Lamm at 2007-07-11 09:31 | Lambda Calculus | other blogs | 11434 reads

Comment viewing options

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

relation to optimal evaluation?

completely lazy evaluation sounds very cool, and it indeed solves some practical leak problem in call-by-need that's caused by loss of sharing of functional applications under lambda. I wonder how it compares to optimal evaluation, as Francois-Regis Sinot's paper doesn't go deep on this except saying it's not optimal by an example.

By ninegua at Thu, 2007-07-12 02:09 | login or register to post comments

Thyer's DPhil & the efficiency of optimality

In the abstract to his DPhil, Thyer claims:

Although optimal evaluators are well known, it is argued that less well understood degrees of sharing, in between the sharing of conventional functional languages and optimal evaluators, are of more practical use.

This is a claim that Ian Mackie has also been interested in, although I think there is very little evidence for it:

  1. The negative result of Asperti & Mairson only observes that optimal reductions can't do magic, or, more explicitly, either P=NP or any optimal reduction strategy for the lambda calculus must potentially do a lot of work to contract each redex, so leading to our interest in the "bookkeeping overhead" of optimal evaluators;
  2. Lamping's optimal lambda evaluator has a very high bookkeeping overhead & Ian Mackie has produced suboptimal evaluators for the lambda calculus which have more sharing than CBNeed evaluators and which have much lower bookkeeping overheads (see his PhD thesis & his paper Yet Another Lambda Evaluator, both of which used to circulate as preprints, but I can't find now...).
  3. But in fact, we know very little about optimal reductions & so can conclude little about our failure to contrive optimal evaluators with comparatively low bookkeeping overhead.

Thyer's thesis looks very interesting: there has been too little work been done on investigating intermediate degrees of sharing. Published in 1999: well, better hear about it late than never...

Edit: fixed discussion of Mackie's work, fixed links (thanks Andrei)

By Charles Stewart at Thu, 2007-07-12 08:49 | login or register to post comments

Lambdascope

Lambdascope has a very small set of interaction rules, and unlike YALE it's optimal.

Thyer's algorithm for completely lazy evaluation actually looks very similar to Lambdascope at first sight. but I've yet to read all the details of his phD work.

By ninegua at Thu, 2007-07-12 13:28 | login or register to post comments

Links missing

Thyer's thesis is here. I don't know what should be referenced by the other link, though.

By Andrei Formiga at Thu, 2007-07-12 14:31 | login or register to post comments

complete laziness and optimal evaluation

It's nice to be LtU'ed, thanks for posting the story Ehud.

One way to view the connection between complete laziness and optimal evaluation, is to think of complete laziness as possessing two of three sharing mechanisms that can be used to implement optimal evaluation.

Consider the following reduction systems:

  1. term reduction
  2. graph reduction
  3. complete laziness
  4. optimal evaluation

These sharing mechanisms can be used to get from one to the next:

  1. graph sharing
  2. delayed substitution with memo-tables
  3. substitution swapping

Complete laziness is a very interesting stage in its own right. It gives you the specializing benefit of a multi-stage language, without requiring the staging annotations. And more than that the specializing effect is inherited beyond the original program, so when specializing an interpreter, the interpreted program will also be specialized, and if its program is also an interpreter it too is specialized, and so on.

Unfortunately, although the memo-table technique makes eliminating towers of interpreters easy, for everyday programs the memo-tables don't stop growing, so unless you program in an unusual style, programs you would expect to run in linear time take n log n time.

The lambda animator demonstrates some of the programming styles which can be used to mitigate this.

An exciting open question is whether a completely lazy evaluator can be capable of both specializing away interpreters and also running conventional programs in conventional time. If this can be done, that would be a great practical result, you could do multi-stage programming with no annotations.

Perhaps using interaction nets to implement complete laziness would solve this.

If it's not possible, it would be good to have a proof it's not, much like Asperti and Mairson's. Without either an implementation or a negative proof, I'll always be wondering.

By Mike Thyer at Thu, 2007-07-12 16:03 | login or register to post comments

lazy v.s. completely lazy v.s. optimal

I guess the argument against complete laziness and optimal are their costs. Here is a sample experiment I did with (n 2 I x), where n and 2 are church numeral, I is the identity function, and x is just a variable.

I'll use the number of beta, number of steps (obtained from Thyer's animator), number of interactions (using lambdascope's algorithm) as the metric for lazy, completely lazy, and optimal respectively.

n   Lazy C.Lazy Optimal
--------------------------
1   6    8      53
2   11   15     93
3   20   25     140
4   37   40     194
5   70   66     255
6   135  114    323
7   264  204    398
8   392  377    453
9   644  719    539

It's easy to tell that they are of O(n * 2^n), O(n^7) and O(n^2) respectively. It's also worth mentioning that if we count the number of betas, optimal is O(n), and completely lazy is O(n^3).

Indeed, I fail to see why optimal has bad overhead in terms of time complexity. At least my experiement shows that optimal is with-in a constant factor of lazy, if not a speed up, even if we count total number of interactions instead of betas.

By ninegua at Fri, 2007-07-13 14:53 | login or register to post comments

mixed strategy

If a mixed lazy / completely-lazy strategy is used then the following steps are required:

n Lazy/C.Lazy
-------------
1    7
2   11 
3   15
4   19
5   23
6   27
7   31
8   35
9   41

This is done with the following use of apply-strategy:

(apply-strategy 'name 'need (nine two) I 'x)

(using substitute-by-need and call-by-need as the default strategies)

It would be interesting to see optimal evaluators applied to examples which really demonstrate their potential. Specifically the ability to use fewer beta reductions than the shortest term-reduction sequence.

The sharing in lazy and completely lazy reduction isn't used so much to increase sharing, as to postpone decisions about whether to reduce a redex. So any efficiency benefits are no better than the efficiency benefits of a term reduction system which magically knows which redex are needed ahead of time.

In contrast, the sharing performed by an optimal evaluator cannot be related to a single term reduction sequence. The number of beta-reductions performed can be lower than the number of beta-reductions in the shortest term reduction sequence.

I've not seen any examples try to exploit this property yet. Perhaps this is where optimal evaluation can really shine.

By Mike Thyer at Sat, 2007-07-14 13:29 | login or register to post comments