vm.fail
Alpha equivalence checker for arbitrary lambda terms
2.2 kB
68 lines
1# ego
2
3Analyzes alpha equivalence in untyped lambda calculus terms. The OCaml
4and Nim implementations keep the 4 binding representations independent:
5
6- named variables
7- de bruijn indices
8- locally nameless terms
9- explicit substitutions
10
11each representation implements parsing conversion, pretty printing, free
12variable analysis, alpha equivalence, capture avoiding substitution and
13normalisation according to its own binding semantics
14
15## Surface syntax
16
17```text
18x variable
19\x. x abstraction
20\x. \y. x y nested abstraction
21(\x. x) y application
22[x := y] t explicit substitution
23```
24
25Application is left associative and abstraction bodies extend to the right while names
26match `[a-zA-Z][a-zA-Z0-9_'-]*` accordingly
27
28## Representation contracts
29
30Named terms store textual binders and resolve references through explicit
31environments whereas substitution performs freshness generation and capture checks
32
33De Bruijn terms encode bound references as lexical indices and retain free
34variables separately and shifting is required when terms cross binder boundaries.
35
36Locally nameless terms encode bound references as indices and free references as
37names. Opening and closing enforce scope transitions; conversion and operations
38reject terms that are not locally closed.
39
40Explicit substitution terms retain substitutions in the syntax tree and reduction
41propagates substitutions through variables, applications as well abstractions while
42preserving alpha equivalence and delayed capture avoidance
43
44## interfaces
45
46All 4 implementations expose the same semantic operations:
47
48```text
49parse
50pretty_print
51free_variables
52alpha_equivalent
53substitute
54normalize
55convert_from_named
56convert_to_named
57```
58
59The OCaml modules are `Named`, `Debruijn`, `Locally_nameless`, and
60`Explicit_subst`. The Nim modules use distinct variant types for each term
61representation and expose equivalent operations
62
63## Automata renderer
64
65This will convert automaton and transducer JSON into Graphviz
66DOT, SVG, PNG, or PDF. Input states may be plain identifiers or objects with
67labels and accepting state metadata. Transitions also accept explicit labels or
68`read`, `write` and `action`