Lambda-Calculus Evaluator

Kovacsics Robert

January 4, 2019

Type an expression into the following text area (using the fn x => body syntax), click parse, then click on applications to evaluate them. Also have a look at the examples section below, where you can click on an application to reduce it (e.g. click on pow 2 3 to get 3 2, then fn x => 2 (2 (2 x))).

(fn n m f x => n f (m f x)) 2 3

Display type λ x . x fn x => x

Maximum single steps

Evaluation strategy

Strict/Eager

Non-strict/Call-by-name

This is ported from my original one at my alma mater webpage, somewhat updated with better diagrams and more modern code.

it can be embedded into websites by linking to lambda-calc.min.js and is available under the permissive MIT license.

MIT license header

⟨lambda-calc.css⟩+≡

/* Copyright 2019 by Robert Kovacsics

   Permission is hereby granted, free of charge, to any person
   obtaining a copy of this software and associated documentation
   files (the "Software"), to deal in the Software without
   restriction, including without limitation the rights to use, copy,
   modify, merge, publish, distribute, sublicense, and/or sell copies
   of the Software, and to permit persons to whom the Software is
   furnished to do so, subject to the following conditions:

   The above copyright notice and this permission notice shall be
   included in all copies or substantial portions of the Software.

   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
   EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
   MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
   NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
   BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
   ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
   CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
   SOFTWARE.
*/

⟨lambda-calc.js⟩+≡

// Copyright 2019 by Robert Kovacsics
//
// Permission is hereby granted, free of charge, to any person
// obtaining a copy of this software and associated documentation
// files (the "Software"), to deal in the Software without
// restriction, including without limitation the rights to use, copy,
// modify, merge, publish, distribute, sublicense, and/or sell copies
// of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be
// included in all copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
// BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
// ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
// CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

The implementation is documented in a literate-programming style below

it uses space-based lexing (though you don’t need to put spaces around parentheses), and only implements the following prefix functions:

the following doesn’t parse
a fn x => y
and you have to use
a (fn x => y)
even though both of them are equally unambiguous. This is not fixed yet, as it would require a change to the grammar, and hence a re-computation of the parse tables which is laborious, and it is not a high priority problem, as Poly/ML and GHC have the same parsing behaviour.

Built-in definitions

Y: fn f => (fn x => f (x x)) (fn x => f (x x))
id: fn x => x
compose: fn f g => fn x => f (g x)
true: fn x y => x
false: fn x y => y
if: fn p x y => p x y
pair: fn x y => fn f => f x y
fst: fn p => p (fn x y => x)
snd: fn p => p (fn x y => y)
cons: fn x y => fn f init => f x (y f init)
nil: fn f init => init
fold: fn f l init => l f init
map: fn f l => fn g init => l (compose g f) init
succ: fn n => fn f x => f (n f x)
add: fn n m => fn f x => n f (m f x)
mul: fn n m => fn f x => n (m f) x
pow: fn n m => m n
pred: fn n f x => n (fn g h => h (g f)) (fn u => x) (fn u => u)
eq0: fn n => n (fn x => false) true

and the special built-in let variable value.

Examples

Evaluating operator: Try clicking on the “x” to evaluate the sequence of identity functions. Also, have a look at what happens if you change the maximum number of single steps.
id id id id x
Capture avoiding substitution: (fn f x => f x) x
Extending the environment: let Y (fn f => (fn x => f (x x)) (fn x => f (x x)))
Looping forever: let loop (Y (fn x => x))
Note, that I have decided to use the Y combinator with an identity function, as using the Omega combinator just expands to itself in a single step, so is perhaps less useful as an example.
the following doesn’t parse
a fn x => y
and you have to use
a (fn x => y)
even though both of them are equally unambiguous. This is not fixed yet, as it would require a change to the grammar, and hence a re-computation of the parse tables which is laborious, and it is not a high priority problem, as Poly/ML and GHC have the same parsing behaviour.
Adding numbers: let add (fn n m => fn f x => n f (m f x))
add 2 3
Multiplying numbers: let mul (fn n m => fn f x => n (m f) x)
mul 2 3
Equality to zero: let eq0 (fn n => n (fn x => false) true)
Successor: let succ (fn n => fn f x => f (n f x))
Predecessor: Here is the simpler predecessor:
let pred (fn n => snd (n (fn p => pair (succ (fst p)) (fst p)) (pair 0 0)))
And here is a faster predecessor, try it out to see how it works:
let pred2 (fn n f x => n (fn g h => h (g f)) (fn u => x) (fn u => u))
Raising to a power: let pow (fn n m => m n)
pow 2 3
Recursive function: Here you have to be careful about the order of the evaluation, otherwise you may loop forever. Choosing the non-strict strategy always reduces to beta-normal form, but you might want to eagerly evaluate the predecessor function when you see it, otherwise you will end up evaluating (pred 2) and (pred (pred 2)) rather than just (pred 2) and (pred 1). But anyway, perhaps iterating this to completion isn’t as useful as just iterating a couple of steps, to see how the Y combinator works.
let *loop* (fn loop => fn n => if (eq0 n) 1 (loop (pred n)))
Y *loop* 2

Implementation

To embed, add the following to the <head> tag:

<script type="text/javascript" src="https://kovirobi.uk/teaching-material/lambda-calc.min.js"></script>

and something like so to the <body> tag:

<pre class="lambda">
  pow 2 3
</pre>
<script type="text/javascript">
{ let pre = document.currentScript.previousElementSibling
  tie_value(pre.innerText, pre);
}
</script>

the style used here is

⟨lambda-calc.css⟩≡

.lambda {
  border: 1px solid black;
  border-radius: 0.25rem;
  padding: 0.5rem;
  margin: 0.5rem;
  font-family: CaskaydiaCove NFM, monospace;
}

Parsing

Parsing tables

First we need to parse the expression, using the grammar given below. This grammar is more complex than the one given in supervisions, as it is the concrete syntax tree, not the abstract syntax tree, and thus encodes parsing precedences and parenthesisation. It also has the added start symbol, and the shorthand for nested lambdas.

\begin{aligned} S \ &::=&& E_r\ \$ \\ E_r \ &::=&& \text{``fn''}\ \text{Vars}\ \text{``=>''}\ E_r \\ E_r \ &::=&& E_l \\ E_l \ &::=&& E_l\ E \\ E_l \ &::=&& E \\ E \ &::=&& var \\ E \ &::=&& \text{``(''}\ E_r\ \text{``)''} \\ \text{Vars} \ &::=&& var\ \text{Vars} \\ \text{Vars} \ &::=&& var \end{aligned}

MathML doesn’t seem to be rendered super well in Chromium engine based browsers.

Because this grammar is left-recursive (for the application, we don’t care about variables/letters being left-associative or right-associative), and because it is fairly small, we can hand-generate an SLR parsing table, as opposed to using a simple recursive-descent parser.

The tables are created by computing the set closure of the next state function, that is to say, executing the next state function on each of the current states in the set, until no more new states are added.

The next state function works by computing, for each grammar rule in the current set, a new set composed of the current symbol accepted. Then each of the new sets is closed under the non-terminal expansion function, that is to say, if the new grammar rule has the cursor before a non-terminal, then all the rules for that non-terminal are added.

As an example, consider state 0 (we always start with the start rule) on which we have already performed the non-terminal expansion. Hence why we have added $E_r$ , $E_l$ and $E$ rules. Then, as an example, state 2 is created when state 0 receives an “fn” token, on which we perform the closure again, which adds the “Vars” rules.

As well as the parser state machine, we also need the follow table, for which we first need the first table. It is a table of all the terminals which may appear first from a given non-terminal. It is computed by looking at all the grammar rules, more detail of which can be found on the internet or in the Dragon Book.

Symbol	Eᵣ	Eₗ	E	Vars
	“fn”	var	var	var
First	var	“(”	“(”
	“(”

First table, for each non-terminal what may appear

The follow table is similarly calculated by looking at the grammar rules, and also using the first table. More details may be found in the same place.

Symbol	var	fn	=>	(	)	Eᵣ	Eₗ	E	Vars
	$	var	var	“fn”	$	$	$	$	“=>”
	“)”		“fn”	var	“)”	“)”	“)”	“)”
Follow	var		“(”	“(”	var		var	var
	“(”				“(”		“(”	“(”

Follow table, for each column, each row symbol may appear

The action and go to tables are a different way of representing the same information which the parser state machine represents. Shift actions are created when a parser state has a transition on a terminal, and go to are when the state has a transition on a non-terminal. Reduce actions mean that a state has an item which has received all its terminals and non-terminals.

State	Action						Go to
	var	fn	=>	(	)	$	Eᵣ	Eₗ	E	Vars
0	S 9	S 2		S 10			1	6	8
1						Accept
2	S 13									3
3			S 4
4	S 9	S 2		S 10			5	6	8
5					R 2	R 2
6	S 9			S 10	R 3	R 3			7
7	R 4			R 4	R 4	R 4
8	R 5			R 5	R 5	R 5
9	R 6			R 6	R 6	R 6
10	S 9	S 2		S 10			11	6	8
11					S 12
12	R 7			R 7	R 7	R 7
13	S 13		R 9							14
14			R 8

Action and go to tables, what to do when encountering symbol in state

Note that we have shift/reduce conflicts at states 6 and 11, but the SLR algorithm resolves these, as we only need to reduce if the next symbol is a “(” or a “=>”, respectively.

Parsing implementation

First, we will set JavaScript to be in strict mode (if it supports it), so that we can catch errors earlier.

⟨lambda-calc.js⟩≡

"use strict";

Before implementing parsing, we will need to do lexing. For this we will just use space as a separator, and create lexemes from each substring. We do a bit of a hack, where we put spaces around parentheses, so that simple string-splitting will work.

⟨lambda-calc.js⟩+≡

function Lexer(lexemes, end_lexeme) {
  this.lexemes = lexemes;
  this.lex = function (str) {
    str = str.replace(/=>|\(|\)/g, " $& "); // Arrow/parentheses
    str = str.replace(/\/\/[^\n]*/g, ""); // Comments
    this.array = str.trim().split(/\s+/);
    this.array = this.array.map(
      el => new (this.lexemes.find(lex => lex.is(el))) (el));
    this.array.push(new end_lexeme());
    this.index = 0;
  }
  this.advance = function () { lexer.index++; };
  this.peek = function () {
    if (lexer.index === lexer.array.length) return null;
    else                                    return lexer.array[lexer.index];
  };
}

The lexemes are objects which can be constructed from a string, and also have a ‘static’ property which determines if the string represents that lexeme. Note, that I have been lazy, and the variable lexeme doesn’t know about reserved words, so the order matters for constructing the lexer.

⟨lambda-calc.js⟩+≡

function FnLexeme (fn) { this.name = "fn"; }
FnLexeme.is = str => str === "fn";

function ArrowLexeme (arrow) { this.name = "=>"; }
ArrowLexeme.is = str => str === "=>";

function LParenLexeme (lpar) { this.name = "("; }
LParenLexeme.is = str => str === "(";

function RParenLexeme (rpar) { this.name = ")"; }
RParenLexeme.is = str => str === ")";

function EndLexeme (end) { this.name = "$"; }
EndLexeme.is = str => false;

function VarLexeme (variable) { this.name = variable; }
VarLexeme.is = str => true;

var lexer = new Lexer([FnLexeme, ArrowLexeme, LParenLexeme,
                        RParenLexeme, VarLexeme], EndLexeme);

The parser is constructed on top of a lexer. It works by executing shift or reduce actions until the action returns true, to signal that the parser is in the accepting state. Note that instead of looking up the current lexeme and state in a two-dimensional action table and then using conditionals to see which action to perform (which is the imperative way), we use a prototype-based approach, by dispatching on the lexeme and the action. Dispatching on the lexeme does turn the action table on its side, but it allows us to use numbers to represent states.

⟨lambda-calc.js⟩+≡

function Parser(lexer) {
  this.lexer = lexer;

  this.parse = function (str) {
    this.states = [0];
    this.values = [];
    this.lexer.lex(str);
    let accepted = false;
    while (!accepted &&
            this.lexer.peek() !== null) {
      let lexeme = this.lexer.peek();
      let action = lexeme.action[this.states.top()];
      accepted = action(this.states, this.values, this.lexer);
    };

    return accepted && this.values.top();
  };
}

var parser = new Parser(lexer);

For convenience, I also define two methods on arrays, top and empty. Note that in larger projects such extensions could be problematic. To see why, suppose that another library has a different implementation of top, say one which checks if the length is greater than zero. This could be solved by a module system, which would allow us to have our own extension to Array, which unless we export it, is not available to the hypothetical other library, and vice versa.

⟨lambda-calc.js⟩+≡

Array.prototype.top = function () { return this[this.length - 1]; };
Array.prototype.empty = function () { return this.length === 0; };

The action table is added to the lexeme prototype property, which isn’t the prototype of the lexeme class (that is the __proto__ property), but the prototype of the instance of a lexeme class (i.e. (new FnLexeme("fn")).__proto__ === FnLexeme.prototype). In other words, we extend each lexeme ‘class’ with new member variables. In a static object-oriented language such as Java or C++, we would have had to use the visitor pattern on lexemes, or hard-code the parse table in the lexeme. This method does have disadvantages, as mentioned for the previous code block.

⟨lambda-calc.js⟩+≡

FnLexeme.prototype.action =
  [Shift(2),   ParseError, ParseError, ParseError, Shift(2),
    ParseError, ParseError, ParseError, ParseError, ParseError,
    Shift(2),   ParseError, ParseError, ParseError, ParseError];

ArrowLexeme.prototype.action =
  [ParseError, ParseError, ParseError, Shift(4),  ParseError,
    ParseError, ParseError, ParseError, ParseError, ParseError,
    ParseError, ParseError, ParseError, Reduce9,    Reduce8];

LParenLexeme.prototype.action =
  [Shift(10),  ParseError, ParseError, ParseError, Shift(10),
    ParseError, Shift(10),  Reduce4  ,  Reduce5,    Reduce6,
    Shift(10),  ParseError, Reduce7,    ParseError, ParseError];

RParenLexeme.prototype.action =
  [ParseError, ParseError, ParseError, ParseError, ParseError,
    Reduce2,    Reduce3,    Reduce4,    Reduce5,    Reduce6,
    ParseError, Shift(12),  Reduce7,    ParseError, ParseError];

EndLexeme.prototype.action =
  [ParseError, Accept,     ParseError, ParseError, ParseError,
    Reduce2,    Reduce3,    Reduce4,    Reduce5,    Reduce6,
    ParseError, ParseError, Reduce7,    ParseError, ParseError];

VarLexeme.prototype.action =
  [Shift(9),   ParseError, Shift(13),  ParseError, Shift(9),
    ParseError, Shift(9),   Reduce4,    Reduce5,    Reduce6,
    Shift(9),   ParseError, Reduce7,    Shift(13),  ParseError];

Our parse error is rather primitive at the moment, but if there is a problem, the browser debugger should be able to help.

⟨lambda-calc.js⟩+≡

function ParseError(s, v, lexer) {
  throw [s, v, lexer.peek(), lexer];
}

The accept action just returns true, so that the parsing loop will now we have finished parsing.

⟨lambda-calc.js⟩+≡

function Accept(s, v, terminals) {
  return true;
}

The shift action shifts a state onto the state stack, and shifts the lexeme onto the value stack.

⟨lambda-calc.js⟩+≡

function Shift(state) {
  return function (s, v, lexer) {
    v.push(lexer.peek());
    s.push(state);
    lexer.advance();
    return false;
  };
}

The reduce actions pop off one item for each part of the corresponding grammar rule body, then use the go to table to push a new state. This is in effect, making a transition on the grammar rule head, from the current state. For the value stack, we do our custom actions to create a syntax tree.

⟨lambda-calc.js⟩+≡

let E_r_goto = [1, ,,, 5, ,,,,, 11, ,,,,];
let E_l_goto = [6, ,,, 6, ,,,,,  6, ,,,,];
let E_goto = [8, ,,, 8, , 7, ,,, 8, ,,,,];
let Vars_goto = [,, 3, ,,,,, ,,,,, 14, ,];

function Reduce1(s, v, lexer) { throw "Should accept instead of reducing S"; }
function Reduce2(s, v, lexer) {
  let E_r = v.pop(), arrow = v.pop(), vars = v.pop(), fn = v.pop();
  vars.reverse()
  s.pop(); s.pop(); s.pop(); s.pop();
  v.push(new Fn(vars, E_r));
  s.push(E_r_goto[s.top()]);
  return false;
}
function Reduce3(s, v, lexer) {
  s.pop();
  s.push(E_r_goto[s.top()]);
  return false;
}
function Reduce4(s, v, lexer) {
  let operand = v.pop(), operator = v.pop();
  s.pop(); s.pop();
  v.push(new App(operator, operand));
  s.push(E_l_goto[s.top()]);
  return false;
}
function Reduce5(s, v, lexer) {
  s.pop();
  s.push(E_l_goto[s.top()]);
  return false;
}
function Reduce6(s, v, lexer) {
  let variable = v.pop();
  s.pop();
  v.push(new Var(variable.name));
  s.push(E_goto[s.top()]);
  return false;
}
function Reduce7(s, v, lexer) {
  let rpar = v.pop(), E_r = v.pop(), lpar = v.pop();
  s.pop(); s.pop(); s.pop();
  v.push(E_r);
  s.push(E_goto[s.top()]);
  return false;
}
function Reduce8(s, v, lexer) {
  let vars = v.pop(), variable = v.pop();
  s.pop(); s.pop();
  vars.push(new Var(variable.name));
  v.push(vars);
  s.push(Vars_goto[s.top()]);
  return false;
}
function Reduce9(s, v, lexer) {
  let variable = v.pop();
  s.pop();
  v.push([new Var(variable.name)]);
  s.push(Vars_goto[s.top()]);
  return false;
}

Our syntax tree is composed of variables, applications and abstractions, which better correspond with the abstract syntax of the lambda calculus.

E ::= x | \lambda x. E | E E

⟨lambda-calc.js⟩+≡

function Var(name) {
  this.name = name;
}

function Fn(vars, body) {
  this.vars = vars;
  this.body = body;
}

function App(operator, operand) {
  this.operator = operator;
  this.operand = operand;
}

Evaluating

Application

Because the single-step is non-deterministic, we let the user chose what to evaluate first, by selecting an application to apply. This is still not fully unambiguous, as the user may chose to apply an application whose left-hand side is not fully reduced, in this case we will let the user chose between strict and non-strict evaluation, and also have a maximum-steps field.

As the user may chose an application in the middle of the whole expression, we need a way of propagating the result of that application upwards in the syntax tree. We will do this by using continuations.

\dfrac{M \to M'} {\lambda x . M \to \lambda x . M'} \textrm{(body)}

⟨lambda-calc.js⟩+≡

Var.prototype.setup = function () { /*No equivalent rule*/ }

Fn.prototype.setup = function () {
  this.body.continuation = (value) => this.continuation(new Fn(this.vars, value));
  this.body.setup();
}

Note that for the body of the continuation, we are using the arrow notation, and not function () { ... }. This is because using the function syntax will bind the value of the this variable during the execution of the function, to the object of that function.

The benefit of using a continuation shines through in the ambiguity of reducing either side of the application.

\dfrac{M \to M'} {M\ N \to M'\ N} \textrm{(left)}

\dfrac{N \to N'} {M\ N \to M\ N'} \textrm{(right)}

⟨lambda-calc.js⟩+≡

App.prototype.setup = function () {
  this.operator.continuation =
    (value) => this.continuation(new App(value, this.operand));
  this.operator.setup();
  this.operand.continuation =
    (value) => this.continuation(new App(this.operator, value));
  this.operand.setup();
}

The last case we consider is performing an application, when the left-hand side is a value. You may note that we have ignored the rule for using alpha-conversion when reducing. We have put the alpha-renaming logic into this step.

As this is the interactive step, we take two arguments (globals for easy embedding, supplied from above), which correspond to how many small-steps should we do if the left-hand side of the application isn’t a value; and what evaluation strategy should we use for the small-steps.

\dfrac{} {\left(\lambda x . M\right) N \to M[N/x]} \textrm{(app)}

⟨lambda-calc.js⟩+≡

var max_steps = 10;
var eager_strategy = false;
App.prototype.perform = function () {
  let next_operator = this.operator;
  let next_operand = this.operand;
  for (let steps = 0; steps < max_steps; ++steps) {
    if (next_operator.is_steppable()) {
      next_operator = next_operator.step();
    } else if (next_operator.requires_eager() &&
                next_operand.is_steppable()) {
      next_operand = next_operand.step();
    } else {
      return this.continuation(next_operator.apply(next_operand));
    }
  }
  return this.continuation(new App(next_operator, next_operand));
}

Var.prototype.is_steppable = function () { return false; }
Fn.prototype.is_steppable  = function () { return false; }
App.prototype.is_steppable = function () { return true; }

We first implement the application of a lambda-term to a value, the finished small-step is given at the end of this section, and is much shorter. In the case of a variable, we can’t really do much, so just return an application term, though note that we perform cloning so that each node is unique. This might be useful if we perform mutation on a node.

For the function case, we first do alpha-renaming to avoid capturing variables. Then strip one variable, and substitute for it. The avoidCapture ensures we don’t need to worry about capturing variables.

⟨lambda-calc.js⟩+≡

Var.prototype.apply = function (actual) {
  return new App(this.clone(), actual.clone());
}

Fn.prototype.apply = function (actual) {
  let renamed = this.avoidCapture(actual.free_var_names(), this.used_names());
  let formal = renamed.vars[0];
  if (this.vars.length > 1) {
    let slice = renamed.vars.slice(1);
    return new Fn(slice, renamed.body).subst(formal, actual);
  } else {
    return renamed.body.subst(formal, actual);
  }
}

The heavy-lifting of avoiding capturing variables is for the function case, when we replace the current identifier for a fresh one, if need be.

⟨lambda-calc.js⟩+≡

Var.prototype.avoidCapture = function (avoid_names, used_names) {
  return this.clone();
}

Fn.prototype.avoidCapture = function (avoid_names, used_names) {
  let new_body = this.body.avoidCapture(avoid_names, used_names)
  let new_names = [];
  for (const v of this.vars) {
    if (avoid_names.has(v.name)) {
      let fresh_var = fresh_variable(v.name, avoid_names, used_names);
      new_names.push(fresh_var);
      new_body = new_body.subst(v, fresh_var);
    } else {
      new_names.push(v);
    }
  }
  return new Fn(new_names, new_body);
}

App.prototype.avoidCapture = function (avoid_names, used_names) {
  return new App(this.operator.avoidCapture(avoid_names, used_names),
                  this.operand.avoidCapture(avoid_names, used_names));
}

function fresh_variable(name, avoid, used) {
  let n;
  for (n = 0; avoid.has(name + n) || used.has(name + n); ++n) { }
  return new Var(name + n);
}

The set of free variables, and used names, have the simple and obvious algorithm.

⟨lambda-calc.js⟩+≡

Var.prototype.free_var_names = function () { return new Set([this.name]); }

Fn.prototype.free_var_names = function () {
  let recur = this.body.free_var_names();
  for (const n of this.vars)
    recur.delete(n.name);
  return recur;
}

App.prototype.free_var_names = function () {
  let operator_names = this.operator.free_var_names();
  for (const n of this.operand.free_var_names())
    operator_names.add(n);
  return operator_names;
}

Var.prototype.used_names = function () { return new Set([this.name]); }

Fn.prototype.used_names = function () {
  let recur = this.body.used_names();
  for (const n of this.vars)
    recur.add(n.name);
  return recur;
}

App.prototype.used_names = function () {
  let operator_names = this.operator.used_names();
  for (const n of this.operand.used_names())
    operator_names.add(n);
  return operator_names;
}

The only case for substitution we now need to take care of, is one binding shadowing another.

⟨lambda-calc.js⟩+≡

Var.prototype.equals = function (arg) { return this.name === arg.name; }
Var.prototype.subst = function (formal, actual) {
  return this.equals(formal) ? actual : this.clone();
}

Fn.prototype.subst = function (formal, actual) {
  if (this.vars.some(x => x.equals(formal))) {
    return this.clone();
  } else {
    return new Fn(this.vars, this.body.subst(formal, actual));
  }
}

App.prototype.subst = function (formal, actual) {
  return new App(this.operator.subst(formal, actual),
                  this.operand.subst(formal, actual));
}

Now we can implement the single-step, using the user supplied strategy.

⟨lambda-calc.js⟩+≡

Var.prototype.step = function () { return this.clone(); }

Fn.prototype.step = function () {
  return new Fn(this.vars, this.body.step());
}

App.prototype.step = function () {
  if (this.operator.is_steppable()) {
    return new App(this.operator.step(), this.operand);
  } else {
    if ((eager_strategy || this.operator.requires_eager())
        && this.operand.is_steppable())
      return new App(this.operator, this.operand.step());
    else
      return this.operator.apply(this.operand);
  }
}

Var.prototype.requires_eager = function () { return false; }
Fn.prototype.requires_eager = function () { return false; }
App.prototype.requires_eager = function () { return false; }

We have two utilities left, cloning, and determining if a variable is bound.

⟨lambda-calc.js⟩+≡

Var.prototype.clone = function () { return new Var(this.name); }
Fn.prototype.clone = function () {
  return new Fn(this.vars, this.body.clone());
}
App.prototype.clone = function () {
  return new App(this.operator.clone(), this.operand.clone());
}
Var.prototype.bind = function (vars) { this.free = !vars.has(this.name); }
Fn.prototype.bind = function (vars) {
  let new_vars = new Set(vars);
  for (const v of this.vars) new_vars.add(v);
  this.body.bind(new_vars);
}
App.prototype.bind = function (vars) {
  this.operator.bind(vars); this.operand.bind(vars);
}

Output

Pretty-printing

For the case of variable, we just print the name, and for the case of a lambda expression, we recursively print the body. We also need to escape HTML codes in names, as we will be modifying the ‘innerHTML’ property. And unfortunately we have a bit of a hack, where we carry a string down the pretty-print chain, which corresponds to how we can access the corresponding object for the click/hover events.

⟨lambda-calc.js⟩+≡

Var.prototype.pretty_print = function () {
  let VarElement = document.createElement("var");
  VarElement.term = this;
  this.element = VarElement;
  VarElement.innerText = this.name;
  return VarElement;
}

Fn.prototype.pretty_print = function () {
  let FnElement = document.createElement("span");
  FnElement.term = this;
  this.element = FnElement;

  let FnText = document.createElement("span");
  FnText.innerHTML = this.fnText;
  FnText.classList.add("fn");
  FnElement.appendChild(FnText);

  FnElement.append(" ");
  for (const v of this.vars) {
    FnElement.appendChild(v.pretty_print());
    FnElement.append(" ");
  }

  let FnArrow = document.createElement("span");
  FnArrow.innerHTML = this.arrowText;
  FnArrow.classList.add("arrow");
  FnElement.appendChild(FnArrow);
  FnElement.append(" ");

  FnElement.appendChild(this.body.pretty_print());
  return FnElement;
}

function setDisplay(fn, arrow) {
  Fn.prototype.fnText = fn; Fn.prototype.arrowText = arrow;
  for (const tag of document.getElementsByClassName("fn"))
    tag.innerHTML = fn;
  for (const tag of document.getElementsByClassName("arrow"))
    tag.innerHTML = arrow;
}
setDisplay("fn", "=&gt;");

We cannot just print the abstract-syntax tree of an application, as that is ambiguous about the parenthesisation, we first need to determine if a term needs parentheses. That is equivalent to determining whether each recursive term occurs below or above the concrete syntax of an application. As an example, let’s label $E_r$ level 0, $E_l$ level 1 and $E$ as level 2. Then the left-hand side of an application can be level 1 or above, and the right-hand side can only be level 2

⟨lambda-calc.js⟩+≡

App.prototype.pretty_print = function () {
  let AppElement = document.createElement("span");
  AppElement.term = this;
  this.element = AppElement;
  AppElement.classList.add("application");

  let OperatorElement = this.operator.pretty_print();
  if (this.operator.grammar_level < 1) {
    OperatorElement.prepend("(");
    OperatorElement.append(")");
  }
  AppElement.appendChild(OperatorElement);

  AppElement.append(" ");

  let OperandElement = this.operand.pretty_print();
  if (this.operand.grammar_level < 2) {
    OperandElement.prepend("(");
    OperandElement.append(")");
  }
  AppElement.appendChild(OperandElement);

  return AppElement;
}

Var.prototype.grammar_level = 2;
App.prototype.grammar_level = 1;
Fn.prototype.grammar_level  = 0;

We just need to make a convenience function for tying the input field to the output.

⟨lambda-calc.js⟩+≡

function tie_value(input, output) {
  while (output.hasChildNodes())
    output.removeChild(output.lastChild);

  let root = parse(input);
  let root_element = root.pretty_print();
  root.setup();
  root.bind(new Set());
  root.continuation = x => x;

  output.appendChild(root_element);
  addInteraction(output);
}
function tie(inputID, outputID) {
  tie_value(document.getElementById(inputID).value,
            document.getElementById(outputID));
}

Logic

First, for helping with parsing expressions, we will highlight applications, so that they are easier to parse.

⟨lambda-calc.js⟩+≡

function appOn(event, span, container) {
  event.stopPropagation();
  span.children[0].style.background = "lightblue";
  span.children[1].style.background = "lightgreen";
}

function appOut(event, span, container) {
  span.children[0].style.background = "";
  span.children[1].style.background = "";
}

And when we receive a button click on an application, we perform it, and prepend the result into the container.

⟨lambda-calc.js⟩+≡

function appClick(event, span, container) {
  if (event.button === 0) {
    event.stopPropagation();
    let new_term = span.term.perform();
    let new_element = new_term.pretty_print();
    new_term.setup();
    new_term.bind(new Set());
    new_term.continuation = x => x;
    container.insertBefore(document.createElement("br"), container.firstChild);
    container.insertBefore(new_element, container.firstChild);
    addInteraction(container);
  }
}

We need to wire these events up to the application terms.

⟨lambda-calc.js⟩+≡

function addInteraction(container) {
  for (const el of container.getElementsByClassName("application")) {
    el.onmouseover = ev => appOn(ev, el, container);
    el.onmouseout = ev => appOut(ev, el, container);
    el.onclick =  ev => appClick(ev, el, container);
  }
}

Extensions

Binding values

We will implement binding values using a variable (unimaginatively called ’let’) which takes a variable and a lambda term, binding the variable to it.

⟨lambda-calc.js⟩+≡

var Environment = new Map();

Var.prototype.is_global = function () {
  return this.free && // Local variables are not global
    Environment.has(this.name) // Only bound global variables
}

Var.prototype.is_steppable = function () {
  if (this.is_global()) {
    return true; // Need to expand
  } else {
    return false;
  }
}

{ let old_var_step = Var.prototype.step;
  Var.prototype.step = function () {
    if (this.is_global()) {
      return Environment.get(this.name);
    } else {
      return old_var_step.call(this,actual);
    }
  }
}

Binding variables happens using the let variable value syntax, by having a special variable, which overrides the apply method.

⟨lambda-calc.js⟩+≡

function LetVar1 () {
  Var.call(this, "let");
}
LetVar1.prototype = Object.create(Var.prototype);
LetVar1.prototype.constructor = LetVar2;

LetVar1.prototype.is_steppable = function () { return false; }
LetVar1.prototype.apply = function (variable) {
  if (variable.name !== undefined) {
    return new LetVar2(variable.name);
  } else {
    throw ["Unable to set ", variable];
  }
}

function LetVar2 (name) {
  Var.call(this, "let");
  this.assign_to = name;
}
LetVar2.prototype = Object.create(Var.prototype);
LetVar2.prototype.constructor = LetVar2

LetVar2.prototype.is_steppable = function () { return false; }
LetVar2.prototype.pretty_print = function () {
  let VarElement = document.createElement("var");
  VarElement.term = this;
  this.element = VarElement;
  VarElement.innerText = this.name;
  let SubScript = document.createElement("sub");
  SubScript.innerText = this.assign_to;
  VarElement.appendChild(SubScript);
  return VarElement;
}

LetVar2.prototype.apply = function (value) {
  Environment.set(this.assign_to, value);
  return value;
}

Environment.set("let", new LetVar1());

We will implement a few common combinators, some from the lecture notes.

⟨lambda-calc.js⟩+≡

Environment.set("Y", parse("fn f => (fn x => f (x x)) (fn x => f (x x))"));
Environment.set("id", parse("fn x => x"));
Environment.set("compose", parse("fn f g => fn x => f (g x)"));
Environment.set("true",  parse("fn x y => x"));
Environment.set("false", parse("fn x y => y"));
Environment.set("if", parse("fn p x y => p x y"));
Environment.set("pair", parse("fn x y => fn f => f x y"));
Environment.set("fst", parse("fn p => p (fn x y => x)"));
Environment.set("snd", parse("fn p => p (fn x y => y)"));
Environment.set("cons", parse("fn x y => fn f init => f x (y f init)"));
Environment.set("nil", parse("fn f init => init"));
Environment.set("fold", parse("fn f l init => l f init"));
Environment.set("map", parse("fn f l => fn g init => l (compose g f) init"));

Numbers

We cannot just add the infinite amount of integers to the environment, we will have to do something more cunning.

⟨lambda-calc.js⟩+≡

Environment.has = function (str) {
  return (!isNaN(Number(str))) || Map.prototype.has.call(this, str);
}

Environment.get = function (str) {
  if (!isNaN(Number(str))) {
    let n = Number(str);
    let operand = new Var("x");
    for (; n > 0; --n) {
      operand = new App(new Var("f"), operand);
    }
    return new Fn([new Var("f"), new Var("x")], operand);
  } else {
    return Map.prototype.get.call(this, str);
  }
}

We also define arithmetic operators.

⟨lambda-calc.js⟩+≡

Environment.set("succ", parse("fn n => fn f x => f (n f x)"));
Environment.set("add", parse("fn n m => fn f x => n f (m f x)"));
Environment.set("mul", parse("fn n m => fn f x => n (m f) x"));
Environment.set("pow", parse("fn n m => m n"));
Environment.set("pred", parse("fn n f x => n (fn g h => h (g f)) (fn u => x) (fn u => u)"));
Environment.set("eq0", parse("fn n => n (fn x => false) true"));

Symbol equality

For simplicity, we define an equals operator sym= which returns true if its two arguments are symbols, and have the same name, and returns false otherwise.

⟨lambda-calc.js⟩+≡

function SymEq1 () {
  Var.call(this, "sym=");
}
SymEq1.prototype = Object.create(Var.prototype);
SymEq1.prototype.constructor = SymEq1;

SymEq1.prototype.is_steppable = function () { return false; }
SymEq1.prototype.requires_eager = function () { return true; }
SymEq1.prototype.apply = function (var1) {
  if (var1.name !== undefined) {
    return new SymEq2(var1.name);
  } else {
    throw ["Non-symbol given to sym=", var1];
  }
}

function SymEq2 (name) {
  Var.call(this, "sym=");
  this.var1 = name;
}
SymEq2.prototype = Object.create(Var.prototype);
SymEq2.prototype.constructor = SymEq2

SymEq2.prototype.is_steppable = function () { return false; }
SymEq2.prototype.requires_eager = function () { return true; }
SymEq2.prototype.pretty_print = function () {
  let VarElement = document.createElement("var");
  VarElement.term = this;
  this.element = VarElement;
  VarElement.innerText = this.name;
  let SubScript = document.createElement("sub");
  SubScript.innerText = this.var1;
  VarElement.appendChild(SubScript);
  return VarElement;
}

SymEq2.prototype.apply = function (var2) {
  if (var2.name !== undefined) {
    if (this.var1 == var2.name) {
      return new Var("true");
    } else {
      return new Var("false");
    }
  } else {
    throw ["Non-symbol given to sym=", this.var1, var2];
  }
}

Environment.set("sym=", new SymEq1());

Error reporting

Parser errors

When we encounter a parsing error, we will return a pseudo-lambda term, which also has the pretty printing function, which finally prints the human readable error.

⟨lambda-calc.js⟩+≡

function ParseErrorTerm(states, values, bad_lexeme, lexer) {
  this.states = states;
  this.values = values;
  this.bad_lexeme = bad_lexeme;
  this.lexer = lexer;
};

Then we implement some of the functions called on terms

⟨lambda-calc.js⟩+≡

ParseErrorTerm.prototype.pretty_print = function () {
  let Error = document.createElement("div");
  Error.term = this;
  this.element = Error;
  let BadLexeme = document.createElement("p");
  BadLexeme.append("Bad lexeme encountered: ");
  BadLexeme.appendChild(this.bad_lexeme.description);
  BadLexeme.append(" at lexer index " + this.lexer.index);
  Error.appendChild(BadLexeme);
  return Error;
};
ParseErrorTerm.prototype.setup = function () {};
ParseErrorTerm.prototype.bind = function () {};
ParseErrorTerm.prototype.setup = function () {};

And something to get strings out of lexemes.

⟨lambda-calc.js⟩+≡

function mkEl(type, text) {
  let el = document.createElement(type);
  el.innerText = text;
  return el;
}

FnLexeme.prototype.description = mkEl("span", "fn");
ArrowLexeme.prototype.description = mkEl("span", "=>");
LParenLexeme.prototype.description = mkEl("span", "(");
RParenLexeme.prototype.description = mkEl("span", ")");
EndLexeme.prototype.description = mkEl("b", "eof");
VarLexeme.prototype.description = mkEl("var", "x");

Then finally catch the parse error, and return it, so that it will be added to the output HTML element.

⟨lambda-calc.js⟩+≡

function parse(str) {
  try {
    return parser.parse(str);
  } catch (parser_error) {
    return new ParseErrorTerm(parser_error[0], parser_error[1],
                              parser_error[2], parser_error[3]);
  }
};