Éole is a Lévy-optimal lambda calculus evaluator, and isasymptoticallyfaster than conventional evaluators. It can compute “quickly enough” things that non-Lévy-optimal evaluators can’t. For example, it can compute200 ^ 200% 31wih Church’s numeral without doing anything special (ie without using mathematical properties).
Éole …
handles the full untyped lambda calculus
based on an interaction network (a graph rewriting system).
Lévy-optimally (avoids duplication of redexes by sharing).
comes with 2 reduction strategies
reduce to normal form (default)
reduce to weak head normal form
has an optional garbage collector(on by default)
it is also modular: you can create your own!
specialized at compile time
has an optional memory compactor(off by default)
accepts some limits
reduction steps
readback depth (while converting the internal graph back to a lambda expression)
can show you some statistics
can create a representation of the internal structure with graphviz:
The gif above shows a reduction of
delta=a->a a . delta (b->b).
In the above graph, nodes have the following format:UIDwith
(*********************:
(x: lambda abstraction, declaring the variable (x)
We have the 3 special nodes Root, Sink and Erase which aremeta nodes
@: Application node
▼ stem: “Sharer” node
▼ ID: “Share boundary” node calledfan in
▲ ID: “Share boundary” node calledfan out
The flashy red arrows show the possible interactions (several possible), while the flashy green node indicates the next interaction (only one). The other filled nodes between the root and the green show the stack currently stacked and that will eventually be considered for reduction.
To follow the description of the steps, get thestatic pdf:
Initial graph:
See howdelta=a->a a.is translated into a function call(λdelta ->...) (λa->aa),
See how the reference toais shared through a special “stem fan” node.
See how the identity(λb ->b)only involves the abstraction node: the variable is represented by targeting the asbtraction node itself.
After reduction of(λdelta ->...) (λa->.
Ready to reduce(λa->aa) (λb ->b).
After reduction of(λa->aa) (λb ->b).
We have( λb ->b) (λb ->b), but see how(λb ->b)appears only once in the graph.
The application node8is stacked.
We start the actual duplication of(λb ->b).
Thestemfan “differentiates” itself into labeled fans.
See how the “body” (empty here) is still shared (between the fans).
Because the application was stacked, it is the next interacting node.
After the reduction of(λb ->b) (λb ->b )(application node 8).
The application is reduced even if the body of the function is still being shared
After the “resolution” of the share, we reach the final state( λb ->b).
Even if it is asymptotically faster, it is not really efficient in common scenario. Seethis recent summary by Asperti (2017)for a quick overview also covering this point.
Éole is implemented following ideas from Levy, Lamping, Asperti, Lafont and many others. Lambda expressions are converted into an interaction net (a computational model) which is then reduced. A good introduction can be found in the book:
Asperti, Andrea and Guerrini, Stefano. The optimal implementation of functional programming languages. Cambridge University Press, 1998.
Summary
Interaction nets contain nodes that can interact (e.g. an application node can interact with a lambda abstraction node). They work by applying local rewriting rules tointeractingpairs of nodes. They are a model of computation and can be use to implement a lambda calculus interpreter. A lambda calculus interpreter is “Lévy-optimal” if it avoids duplicating work, i.e. redexes, but also “virtual redexes” (things that might create redexes down the road). This is done through “sharing” and “unsharing” which are represented respectively by “fan in” and “fan out” nodes.
When something is shared, a fan in and fan out delimiting the new share are created. The tricky part is that several distinct shares may overlap. When a fan in meets a fan out, is it the end of share (a “sharing” node meeting its “unsharing” counterpart), or not (the nodes represent different shares)? Answering that question is the main problem that Lamping was the first to solve with his algorithm.
Lamping, John. An algorithm for optimal lambda calculus reduction. Proceeding POPL 1990, Pages 16 – 30.
The only problem is that the algorithm has a non negligible amount of overhead due to a lot of bookkeeping operations. In some extreme cases, the bookkeeping is in O (2 ^ n) when the number of beta reductions is O (n).
Julia Lawall and Harry G. Mairson. Optimality and Inefficiency: What Isn’t a Cost Model of the Lambda Calculus? (1996) ACM SIGPLAN Proceedings 1996, Pages 92 – 101.
Beyond that, performing interactions in the nets amount to a pretty straightforward graph rewriting system (special note: the garbage collection can also be challenging). Hence, the “fans pairing” algorithm was given a special name:the Oracle. In other words: do your interactions, and when two fans meet, ask the oracle what to do. I like to think (probably inaccurately) about optimal reductions as:
Optimal reduction=interaction net oracle
The Éole approach
Éole’s changes are:
Its interaction nets are directed
It has two kinds of fans in:
Stem fans, which are “sharer” and do not have a fan out counterpart
Differentiated fans in, which with their fans out counterpart create “share boundaries”
A lazy labeling of differentiated fans in.
Stem fans differentiated themselves when crossing a lambda abstraction node. A new unique label is created and assigned to the now differentiated fan in (going down the body of the abstraction) and its matching fan out (following the binder). In the current implementation, the lazy labeling is done through a global 64 bits counter. This break the spirit of thelocal rewriting rules, but isn’t a problem at all implementation wise.
More details, are to come in a paper (hopefully with a proof of Éole), along with a discussion on the garbage collector and reduction strategies (the current implementation offers 2 of them, see below).
Using the system (Linux instructions, probably works on mac too)
Building
You need an up-to-date installation of Rust (but not a nightly release). Just go in the main folder and:
cargo build --release
This will create an executable in thetarget / releasefolder.
Éole can generatedot filesthat can then be passed tographvizto draw the several reduction steps. Installgraphvizif you want to visualize what is going on! The./ dotgraph.shscript creates the graphs and then assemble them usingpdfuniteOn Archlinux, pdfunite is provided by poppler. Check your distribution for things aroundpoppler(likepoppler-utils) if you want it.
First test
Launching
./ target / release / eole
Should print the help and exit. Have a quick read!
Thetestsfolder contains a several files you can try or use as example. Let’s start with something simple (linux style):
./ target / release / eole tests / 00 _ def.eole
which defines the identity function and the evaluates it (without an argument) should print:
(i5->i5)
In lambda calculus, we would writeλi5.i5. Theicomes from the source and the5is an internal identifier.
Generating graph
If you havegraphvizinstalled, you can try
./ launch.sh -G tests / 04 _ delta.eole
Éole will create ageneratedfolder and put adot filesper reduction step in it (plus the initial state of the network).
Note: Thelaunch.shscript purpose is to clean any previousgeneratedfolder before callingeole, forwarding all the arguments. Then, it calls the./ dotgraph.shscript, which generate the graphs.
The- Gflag ask a graph per reduction step. The- gflags only generate the initial and final graph.
Never put anything in generated!. /launch.shdoes a brutal cleaning …
Black nodes are special nodes:
The root is used internally to anchor the graph.
Other black node are used by the garbage collector.
If it is a node “inside the graph”, it is a temporary root for the reduction.
The flashy green node represents the next interacting destructor.
The flashy violet nodes represent the stack of nodes from the root to the next interacting node.
Possible interaction are highlighted in red.
Limiting the number of interaction
Some term can diverge, e.g. the term(λi.ii) (λi.ii)forever reduced into itself. In that case, we can limit the number of interactions with the- rflag.
./ launch.sh tests / 05 _ delta_delta.eole -r 50
Note:this is a limit on the number of interactions, not β- reductions!
will indeed shows you that 50 is a limit on interaction: only 10 β-reductions were performed.
Reduction strategies
By default, Éole uses afullstrategy: it will reduce everything, ie if a term has a normal form, it will reach it. For example, the following computes3!with Church numbers.
This should print(x 38 ->(y 52 ->(x 38 (x 38 (x 38 (x 38 (x 38 (x (y) ))))))))), ie 6 in Church number. Note that thefullstrategy does not do useless work, ie it isnota “strict” or “call by value” strategy!
We can also use a lazy strategy with the ‘-s’ flags:
And this will print something “bigger” because the lazy strategy stops at the weak head normal form.
Limiting the read back
Some “small” graphs can represent quite “large” syntactic lambda terms. The read back can be limited (in “depth” when traveling the graph) by the- lflag. Try this:
By default, Éole never releases the memory. This is can be seen by theEnd allocationstats, showing the amount of memory used by the nodes just before terminating. The compaction can be activated with the- Mflags
A lambda abstraction is written with an arrow, e.g.a->aisλa.aand application is done by juxtaposition. A file can contains several definitions, terminated by a dot:symbol=term.Finally, a file can contain one term to evaluate, also dot-terminated.
GIPHY App Key not set. Please check settings