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)");