# 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

```text
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:

```text
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`