Absal

An optimal evaluator for the λ-calculus. Absal works by compiling terms to (symmetric) interaction combinators.

It asymptotically beats all usual evaluators of functional programs, including Scheme Chez, Haskell GHC, JavaScript V8 and so on, which means it can be millions of times faster in some cases, as explained on this article.

It is similar to other optimal evaluators, except that it doesn't include any book-keeping machinery ("oracle"), only the "elegant core". Because of that, the implementation is very small, around 250 lines of code, including parsers.

Sadly, this algorithm isn't complete: it is incapable of evaluating λ-terms that copy a copy of themselves (like (λx.(x x) λf.λx.(f (f x)))). While this is very rare in practice, making Absal compatible with the entire λ-calculus is an important open problem.

Usage

• Install

  npm install -g abstract-algorithm

• Use as a command

  absal "(λf.λx.(f (f x)) λf.λx.(f (f x)))"
  
  # or...
  
  absal <file_name>

• Use as a lib

  const Absal = require("absal");
  
  // Parses a λ-term
  var term = Absal.core.read("(λf.λx.(f (f x)) λf.λx.(f (f x)))");
  
  // Compiles to interaction combinators net
  var inet = Absal.inet.read(Absal.comp.compile(term));
  
  // Reduces the net
  var rewrites = Absal.inet.reduce(inet);
  
  // Decompiles back to a λ-term
  var term = Absal.comp.decompile(inet);
  
  // Prints the result
  console.log(Absal.core.show(term));
  console.log("("+rewrites+" rewrites)");

• Work with interaction combinators directly

  const Absal = require("absal");
  
  // Creates an interaction combinator net with 4 nodes
  var inet = Absal.inet.read(`
  - a b a
  - c d b
  - c e e
  - d f f
  `);
  
  // Reduces the net
  var rewrites = Absal.inet.reduce(inet);
  
  // Prints the result
  console.log(Absal.inet.show(inet));
  console.log("("+rewrites+" rewrites)");

Some drawings

• Numbers

• Pairs

• Either

Stuff

• This

• This

• Formality