ego#

Analyzes alpha equivalence in untyped lambda calculus terms. The OCaml and Nim implementations keep the 4 binding representations independent:

• named variables
• de bruijn indices
• locally nameless terms
• explicit substitutions

each representation implements parsing conversion, pretty printing, free variable analysis, alpha equivalence, capture avoiding substitution and normalisation according to its own binding semantics

Surface syntax#

x                  variable
\x. x              abstraction
\x. \y. x y        nested abstraction
(\x. x) y          application
[x := y] t         explicit substitution

Application is left associative and abstraction bodies extend to the right while names match [a-zA-Z][a-zA-Z0-9_'-]* accordingly

Representation contracts#

Named terms store textual binders and resolve references through explicit environments whereas substitution performs freshness generation and capture checks

De Bruijn terms encode bound references as lexical indices and retain free variables separately and shifting is required when terms cross binder boundaries.

Locally nameless terms encode bound references as indices and free references as names. Opening and closing enforce scope transitions; conversion and operations reject terms that are not locally closed.

Explicit substitution terms retain substitutions in the syntax tree and reduction propagates substitutions through variables, applications as well abstractions while preserving alpha equivalence and delayed capture avoidance

interfaces#

All 4 implementations expose the same semantic operations:

parse
pretty_print
free_variables
alpha_equivalent
substitute
normalize
convert_from_named
convert_to_named

The OCaml modules are Named, Debruijn, Locally_nameless, and Explicit_subst. The Nim modules use distinct variant types for each term representation and expose equivalent operations

Automata renderer#

This will convert automaton and transducer JSON into Graphviz DOT, SVG, PNG, or PDF. Input states may be plain identifiers or objects with labels and accepting state metadata. Transitions also accept explicit labels or read, write and action