HerrmannM / eole, Hacker News

HerrmannM / eole, Hacker News



É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:

gif for delta id

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)
    • λ ● x: lambda abstraction, declaring theunusedvariablex
      • 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:

    1. Initial graph:
      • See howdelta=a->a 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.
    2. After reduction of(λdelta ->...) (λa->.
      • Ready to reduce(λa->aa) (λb ->b).
    3. 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.
    4. 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.
    5. 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
    6. After the “resolution” of the share, we reach the final state( λb ->b).


    • Éole is experimental and not proven (WIP)
      • Only use for research and curiosity purpose!
    • “Lévy-optimal” does not means “efficient”

    É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.


    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

    1. 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”
    2. 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)


    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


    ./ 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:


    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

    ./ -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.

    ./ tests / 05 _ delta_delta.eole -r 50

    Note:this is a limit on the number of interactions, not β- reductions!

    Show me some stats

    Add the- vflags:

    ./ tests / 05 _ delta_delta.eole -r 50 -v

    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.

    ./ tests / benchmarks / fact 03 _ noid.eole

    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:

    / tests / benchmarks / fact 03 _ noid.eole -s lazy

    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:

    ./ tests / benchmarks / fact 07 _ noid.eole -l 0 -v -g

    Have a look at the graph, and then try this:

    ./ tests / benchmarks / fact 07 _ noid.eole -v

    Memory options

    The garbage collector can be deactivated with the- mflag. Try this command and take a look at the memory used by the nodes:

    ./ tests / benchmarks / fact 80

    Then compare with:

    ./ tests / benchmarks / fact 80 eole -v -m none

    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

    ./ tests / benchmarks / fact 80 eole -v -M 1

    Syntax of Éole’s file

    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.

    See the examples in thetestsfolder.


Brave Browser
Read More

What do you think?

Leave a Reply

Your email address will not be published.

GIPHY App Key not set. Please check settings

Dow Futures Creep Up as Stock Market Eyes Record Highs Within Days, Crypto Coins News

Dow Futures Creep Up as Stock Market Eyes Record Highs Within Days, Crypto Coins News

Build you own dial up ISP in 2019, Hacker News