dGoI Visualiser

A tool for web browsers (http://koko-m.github.io/GoI-Visualiser/) that simulates execution of the dynamic GoI abstract machine for the lambda-calculus.

What is the dynamic GoI abstract machine?

Given the graph representation of an untyped lambda-term, the dynamic GoI abstract machine simulates its evaluation by token-guided graph rewriting. An agent called "token" moves around the graph and triggers rewrites, using its own data. The machine can simulate four evaluation strategies: namely, call-by-name, call-by-need, left-to-right call-by-value, and right-to-left call-by-value.

Usage

1. Select an example, or enter your own closed lambda-term.
2. Select an evaluation strategy, or click the >> button if you are happy with the current strategy.
3. Click the ► button.

Un-checking the Draw button stops drawing graphs. An execution can be paused by the ❚❚ button, resumed by the ► button, and run step-by-step by the ►| button. The ↻ button refreshes the drawing.

Accepted terms

Only pure untyped lambda-terms are accepted, in the following grammar. You may need more parenthesis than you expect, especially for function application.

<var> := {variables}
<expr> ::= <var>  # variables
         | (\lambda <var>. <expr>)     # abstraction
         | (<expr> <expr>)             # application

Note that you will see the character λ as soon as you type \lambda.

What you see

• A graph, with the token indicated by the red edge.
  • Its Graphviz source is shown in the left gray box.
• The token data below the graph, whose top lines are always the latest:
  • The leftmost data is rewrite flag. The graph is rewritten whenever the flag is raised, i.e. set to <λ> or <!>.
  • The second data is computation stack, used to determine the order of evaluating a function and its argument.
  • The third data is box stack, used to manage duplication of sub-graphs wrapped in a dashed box.
  • The rightmost data is environment stack, used only in the call-by-name evaluation to manage duplication of sub-graphs without actually duplicating them.

In call-by-need, left-to-right call-by-value, and right-to-left call-by-value modes

The token triggers rewrites as it travels around a graph. At the end of a successful execution of the abstract machine, the token is at the bottom of the graph that represents the evaluation result of the given lambda-term.

For example, given a lambda-term (((λ f. λ x. (f x)) (λ w. w)) (λ z. z)), execution of the abstract machine yields the graph representation of the lambda-term (λ z. z).

The behaviour of the abstract machine is formally presented in [Muroya & Ghica, LMCS 2019].

In call-by-name mode

The token never triggers rewrites, and simply travels around a graph. At the end of a successful execution of the abstract machine, the token indicates a sub-graph that corresponds to the evaluation result of the given lambda-term.

For example, given a lambda-term (((λ f. λ x. (f x)) (λ w. w)) (λ z. z)), execution of the abstract machine yields precisely the same graph representation of the lambda-term, with the token stopping at the root of the sub-graph that represents (λ z. z).

The behaviour of the abstract machine can be found in [Muroya & Ghica, LMCS 2019, Fig. 17]. It is an adaptation of the Jumping Abstract Machine of [Danos & Regnier, ENTCS 1996].

For more information

Developers

• Steven Cheung for the preceding implementation
• Koko Muroya

An introduction to the dynamic GoI abstract machine

... is on youtube, which was given at Lambda World Cadiz 2018 for functional programmers. (Don't worry, the bug that appeared in the talk has been fixed!)

References

• Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: a Token-Guided Graph Rewriter. Logical Methods in Computer Science, 15(4), 2019. [pdf] This is an expanded version of the CSL'17 paper and the WPTE'17 paper.
• Koko Muroya and Dan R. Ghica. The dynamic Geometry of Interaction machine: a call-by-need graph rewriter. In CSL 2017. [pdf]
• Koko Muroya and Dan R. Ghica. Efficient implementation of evaluation strategies via token-guided graph rewriting. In WPTE 2017. [pdf]

Follow-up work

• OCaml visual debugger implemented by Jack Hughes

Libraries

This tool uses graph-viz-d3-js for generating diagrams, and lo-js for parsing terms.