interactive interaction net compiler and reducer

  ╭─────╮
╭─┴─╮ ╭─┴─╮
│ ζ │ │ δ │  
╰┬─┬╯ ╰┬─┬╯
 │ ╰───╯ │
 ╰───────╯

• THEORY
• ARCHITECTURE

no ai was used for any part of this project

• Install a current Effekt version and its JS dependencies as per the instructions
  • You can ignore LLVM, as we do not support it for now

the nix setup is untested except for running CI

nix develop # open shell with installed dependencies
nix run     # run main entry
nix build   # build project

effekt --backend js-web app/main.effekt

If building has finished successfully, Effekt will give you a link you can open in a browser (recommended: modern desktop firefox).

You can enter terms in the left panel (see THEORY for the syntax). Multiple lines will be interpreted as multiple constructors or multiple lambda terms. You can then render the input by clicking the render button. Pan/zoom the produced graph by dragging/clicking your mouse. Step the reducer by pressing step. Change the source language by pressing the mode button.

The rendered triangles are mapped to the following: Light triangles = constructors, dark triangles = duplicators.

effekt --backend js app/main.effekt

The TUI only supports lambda terms (see THEORY for the syntax). Enter a term and press enter to compile. Step reduction with an exclamation mark !. Normalize with @. Exit with Ctrl+c.

effekt --backend js test/main.effekt

Remember the THEORY: for now this only supports a very small subset of the lambda calculus (we do not even label duplicators)! Though at least the linear lambda calculus is supported.

• x => x (identity)
• x => y => x (k, notice the erasure via nilary duplicator)
• x => x x => x (parsed as two separate identities)
• (x => (x x) x => x) (duplication of identity, reduces to identity)
• s => z => (s (s (s (s z)))) (church 4, nesting of duplicators)
  • (effekt might crash with b_k_0 is not defined here)

• a+(a-) (cycle)
• a+(b+, b-) (lambda identity)
• a+(b+, c-) a-[d-, e+] b-(a+, a-) c+(a+, a-) d+(a+, a-) e-(a+, a-) (unfolding)

• sometimes you have to resize the window first in order for the canvas size to be interpreted correctly (otherwise the agents can appear stretched/squeezed)
• the parser emits successfully parsed parts of the term eagerly, so if there's some garbage after correctly parsed code, it will not complain
• non-binary duplication is not fully supported for now
• if you leave the site open for too long, your memory will eventually run out

Multiple external resources were used for this project. If code was taken from other projects, it's clearly stated as such either in a comment at the top of the file or above the respective code snippet.

For one, the theory is influenced by the papers mentioned in my resource collection. The parsers and lexers are copied almost verbatim from the compiler frontend casestudy in Effekt's documentation (MIT). Several formulas and ideas (see net/layout) are inspired by the Haskell graph-rewriting library by Jan Rochel (MIT).