lambster

A lambda calculus interpreter written in TypeScript, packaged for npm.

Features

Clean, minimal command-line interface with REPL and ability to run files
No external dependencies

Selectable verbosity for lambda calculus term reduction output:

Result (none): only the result of the reduction

λ> (Lx y. x y)(Lw. (Lx.x w) a w) b
>>> ((a b) b)

Reductions (low): intermediate reductions

λ> (Lx y. x y)(Lw. (Lx.x w) a w) b
λ > (((λx. (λy. (x y))) (λw. (((λx. (x w)) a) w))) b)
β > (((λx. (λy. (x y))) (λw. ((a w) w))) b)
β > ((λy. ((λw. ((a w) w)) y)) b)
β > ((λy. ((a y) y)) b)
β > ((a b) b)
>>> ((a b) b)

Step-by-step (high): intermediate reductions with plain English explanation for each reduction

λ> (Lx y. x y)(Lw. (Lx.x w) a w) b
λ > (((λx. (λy. (x y))) (λw. (((λx. (x w)) a) w))) b)

Beta reducing 'a' into '(λx. (x w))'
β > (((λx. (λy. (x y))) (λw. ((a w) w))) b)

Beta reducing '(λw. ((a w) w))' into '(λx. (λy. (x y)))'
β > ((λy. ((λw. ((a w) w)) y)) b)

Beta reducing 'y' into '(λw. ((a w) w))'
β > ((λy. ((a y) y)) b)

Beta reducing 'b' into '(λy. ((a y) y))'
β > ((a b) b)

>>> ((a b) b)

Simple variable system with useful predefined lambda calculus terms

λ> duplicate = Lx.x x
>>> duplicate = (λx. (x x))
λ> duplicate z
>>> (z z)

λ> env
true:	(λt. (λf. t))
false:	(λt. (λf. f))
and:	(λa. (λb. ((a b) a)))
or:	(λa. (λb. ((a a) b)))
not:	(λb. ((b false) true))
if:	(λp. (λa. (λb. ((p a) b))))
... (all bindings in the environment are printed)
λ> or true false
>>> (λX0. (λf. X0))
    ↳ equivalent to: true

Optional free variable renaming

λ> (Ly.y) y
λ > ((λy. y) y)
ε > 'y' → 'X`0'
β > X`0
>>> X`0

Shorthand for introducing nested lambda functions
```
λ> (Lx y. y x)
>>> (λx. (λy. (y x))
```

Shorthand for introducing lambda functions

λ> (lambda x. x) y
>>> y
λ> (λx. x) y
>>> y
λ> (Lx. x) y
>>> y

Clear and robust error printing

λ> (xx
Error at line 1 [4, 5]: Expected ')' to close expression.
    (xx
       ^
λ> Lx x
Error at line 1 [5, 6]: Expected dot after abstraction declaration, got '<newline>'.
    Lx x
        ^

Results are checked for structural equivalence to terms bound in the environment

λ> env
plus:	(λm. (λn. ((m incr) n)))
one:	(λf. (λx. (f x)))
two:	(λf. (λx. (f (f x))))
three:	(λf. (λx. (f (f (f x)))))
...
λ> plus one two
>>> (λf. (λy. (f (f (f y)))))
    ↳ equivalent to: three

Simple comment support
```
λ> (Lx.x) y # This is a comment
>>> y
```

Installation

lambster is available on npm! Simply install the package:

npm i lambster

Usage

CLI

After lambster is installed, launch the interactive prompt:

$ lambster

Client

After lambster is installed, import and use the interpreter:

import { Interpreter, Verbosity, InterpreterOptions } from "lambster";

const interpreter: Interpreter = new Interpreter();

interpreter.evaluate("(Ly. y) z");
// <console output>
// >>> z

The interpreter can also be passed an InterpreterOptions to control output parameters.

Interpreter output is surfaced via console.log by default, and can be customized via the transports option.

import { Interpreter, Verbosity, InterpreterOptions } from "lambster";

let output: string = "";

const interpreter: Interpreter = new Interpreter({
    verbosity: Verbosity.LOW,
    transports: [
        log => (output += log), // called once for each step of the reduction
    ],
});

interpreter.evaluate("(Lx.x x) y");

console.log(output);
// <console output>
// λ > ((λx. (x x)) y)
// β > (y y)
// >>> (y y)

API Reference

class Interpreter:

constructor(options?: InterpreterOptions)
- Create an instance of an Interpreter, optionally with the given options.
- If options are not provided, interpreter parameters are given these default values:
  - verbosity: Verbosity.NONE (prints result only)
  - transports: [console.log]
  - rename_free_vars: false
  - show_equivalent: true
interpret(source: string)
- Interpret the given string and write the output to the provided transports

interface InterpreterOptions

verbosity?: Verbosity
- Optional Verbosity level for the interpreter
transports?: LoggerTransport[]
- Optional list of transport functions that the interpreter will pass its output to
rename_free_vars?: boolean
- Optional boolean that controls whether the interpreter will rename free variables to unambiguous names
show_equivalent?: boolean
- Options boolean that controls whether the interpreter will also print named terms that the result of a reduction is structurally equivalent to

enum Verbosity

NONE
- Indicates the least amount of verbosity to the interpreter. Only the result of the reduction will be logged.
LOW
- Indicates that the interpreter will log the result and type of each intermediate reduction while reducing a given term.
HIGH
- Indicates that the interpreter will log a plain English explanation along with each intermediate reduction while reducing a given term.

Grammar

For all you PL nerds out there, the interpreter recognizes this grammar:

Grammar for lambster

program     → ( stmt )* EOF ;

stmt        → bindingStmt
            | commandStmt
            | termStmt
            | "\n" ;
bindingStmt → IDENTIFIER "=" expression "\n" ;
commandStmt → "help" "\n"
            | "env" "\n"
            | "unbind" IDENTIFIER "\n" ;
termStmt    → term "\n" ;
term        → IDENTIFIER
            | abstraction
            | application
            | grouping ;
abstraction      → LAMBDA IDENTIFIER+ "." expression ;
application → expression expression ;
grouping    → "(" expression ")" ;
LAMBDA      → "L" | "\" | "λ" | "lambda" ;
IDENTIFIER  → [a-z0-9]+ ;

Modified for recursive descent parsing

term            → abstraction
                | application ;
abstraction     → LAMBDA IDENTIFIER+ "." term ;
application     → atom atom* ;
atom            → "(" term ")"
                | IDENTIFIER
                | abstraction ;

Operator precedence (descending)

Name	Associates
Application	Left
Abstraction	Extends as far to the right as possible

Planned features

Automatically parse numeric constants into their Church numeral equivalent
Support for De Bruijn indices
Even prettier printing in step-by-step verbosity
Library functions that do useful/interesting things (TBD)

minchingtonak/lambster