Simple Kombinator Interpreter - a combinatory logic & lambda calculus parser and interpreter. Supports SKI, BCKW, Church numerals, and setting up assertions ('quests') involving all of the above.
npm install @dallaylaen/ski-interpreterThis package contains a
combinatory logic
and lambda calculus
parser and interpreter focused on traceability and inspectability.
It is written in plain JavaScript (with bolted on TypeScript support)
and can be used in Node.js or in the browser.
* SKI and BCKW combinators
* Lambda expressions
* Church numerals
* Defining new terms
* λ ⇆ SKI conversion
* Comparison of expressions
* Includes a class for building and executing test cases for combinators
* Uppercase terms are always single characters and may be lumped together;
* Lowercase alphanumeric terms may have multiple letters and must therefore be separated by spaces;
* Whole non-negative numbers are interpreted as Church numerals, e.g. 5 x y evaluates to x(x(x(x(x y)))). They must also be space-separated from other terms;
* x y z is the same as (x y) z or x(y)(z) but not x (y z);
* Unknown terms are assumed to be free variables;
* Lambda terms are written as x->y->z->expr, which is equivalent tox->(y->(z->expr)) (aka right associative). Free variables in a lambda expression ~~stay in Vegas~~ are isolated from terms with the same name outside it;
* X = y z defines a new term.
* I x ↦ x _// identity_;
* K x y ↦ x _//constant_;
* S x y z ↦ x z (y z) _// fusion_;
* B x y z ↦ x (y z) _// composition_;
* C x y z ↦ x z y _// swapping_;
* W x y ↦ x y y _//duplication_;
The special combinator + will increment Church numerals, if they happen to come after it:
* + 0 // 1
* 2 + 3 // -> +(+(3)) -> +(4) -> 5
The term + 0 idiom may be used to convert
numbers obtained via computation (e.g. factorials)
back to human readable form.
Applications and native terms use normal strategy, i.e. the first term in the tree
that has enough arguments is executed and the step ends there.
Lambda terms are lazy, i.e. the body is not touched until
all free variables are bound.
* all of the above features (except comparison and JS-native terms) in your browser
* expressions have permalinks
* can configure verbosity and execution speed
* Quests
This page contains small tasks of increasing complexity.
Each task requires the user to build a combinator with specific properties.
REPL comes with the package as bin/ski.js.
``bash`
npm install @dallaylaen/ski-interpreter
`javascript
#!node
const { SKI } = require('@dallaylaen/ski-interpreter');
// Create a parser instance
const ski = new SKI();
// Parse an expression
const expr = ski.parse(process.argv[2]);
// Evaluate it step by step
for (const step of expr.walk({max: 100})) {
console.log([${step.steps}] ${step.expr});`
}
`javascript
const { SKI } = require('@dallaylaen/ski-interpreter');
const ski = new SKI();
const expr = ski.parse(src);
// evaluating expressions
const next = expr.step(); // { steps: 1, expr: '...' }
const final = expr.run({max: 1000}); // { steps: 42, expr: '...' }
const iterator = expr.walk();
// applying expressions
const result = expr.run({max: 1000}, arg1, arg2 ...);
// same sa
expr.apply(arg1).apply(arg2).run();
// or simply
expr.apply(arg1, arg2).run();
// equality check
ski.parse('x->y->x').equals(ski.parse('a->b->a')); // true
ski.parse('S').equals(SKI.S); // true
ski.parse('x').apply(ski.parse('y')).equals(ski.parse('x y')); // also true
// defining new terms
ski.add('T', 'CI'); // T x y = C I x y = I y x = y
ski.add('M', 'x->x x'); // M x = x x
// also with native JavaScript implementations:
ski.add('V', x=>y=>f=>f.apply(x, y), 'pair constructor');
ski.getTerms(); // all of the above as an object
// converting lambda expressions to SKI
const lambdaExpr = ski.parse('x->y->x y');
const steps = [...lambdaExpr.toSKI()];
// steps[steps.length - 1].expr only contains S, K, I, and free variables, if any
// converting SKI expressions to lambda
const skiExpr = ski.parse('S K K');
const lambdaSteps = [...skiExpr.toLambda()];
// lambdaSteps[lambdaSteps.length - 1].expr only contains lambda abstractions and applications
`
The format methods of the Expr class supports
a number of options, see the source code for details.
By default, parsed free variables are global and equal to any other variable with the same name.
Variables inside lambdas are local to said lambda and will not be equal to anything except themselves.
A special scope argument may be given to parse to limit the scope. It can be any object.
`javascript`
const scope1 = {};
const scope2 = {};
const expr1 = ski.parse('x y', {scope: scope1});
const expr2 = ski.parse('x y', {scope: scope2}); // not equal
const expr3 = ski.parse('x y'); // equal to neither
const expr4 = ski.parse('x', {scope: scope1}).apply(ski.parse('y', {scope: scope1})); // equal to expr1
Variables can also be created using magic SKI.vars(scope) method:
`javascript`
const scope = {};
const {x, y, z} = SKI.vars(scope); // no need to specify names
Expressions are trees, so they can be traversed.
`javascript
expr.any(e => e.equals(SKI.S)); // true if any subexpression is S
expr.traverse(e => e.equals(SKI.I) ? SKI.S.apply(SKI.K, SKI.K) : null);
// replaces all I's with S K K
// here a returned Expr object replaces the subexpression,null
// whereas means "leave it alone and descend if possible"`
The Quest class may be used to build and execute test cases for combinators.
`javascript
const { Quest } = require('@dallaylaen/ski-interpreter');
const q = new Quest({
name: 'Test combinator T',
description: 'T x y should equal y x',
input: 'T',
cases: [
['T x y', 'y x'],
],
});
q.check('CI'); // pass
q.check('a->b->b a'); // ditto
q.check('K'); // fail
q.check('K(K(y x))') // nope! the variable scopes won't match
``
See quest page data for more examples.
* @ivanaxe for luring me into icfpc 2011 where I was introduced to combinators.
* @akuklev for explaining functional programming to me so many times that I actually got some idea.
* "To Mock The Mockingbird" by Raymond Smulian.
* combinator birds by Chris Rathman
* Fun with combinators by @oisdk
* Conbinatris by Dirk van Deun
This software is free and available under the MIT license.
© Konstantin Uvarin 2024–2026