1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
## Modal: a tree rewriting system
This repository contains a small implementation of Modal, a homoiconic tree‑rewriting language. Modal programs are collections of rewrite rules applied to a tree until no rule matches. See the original description for background and examples: [Modal in a Postcard](https://wiki.xxiivv.com/site/modal).
### Core concepts
- **Program**: an ordered list of rules. Rule order matters; the first matching rule is applied.
- **Tree**: symbolic S‑expressions (atoms and lists), serialized with parentheses.
- **Rule**: `<> left right`, where `left` and `right` are trees. Matching is structural.
- **Registers**: variables in patterns prefixed with `?` (e.g., `?x`). They bind to subtrees during a match and are substituted on the right side.
- **Evaluation**: scan the serialized tree left‑to‑right; at each node, try rules top‑to‑bottom; on first match, replace the matched subtree with the rule’s right side (with current bindings) and restart scanning from the beginning. Halt when a full scan finds no match.
### Syntax quick reference
- Atom: `word` or a quoted symbol like `(0)` used in number encoding.
- Tree: `(head tail...)` or nested pairs to encode lists, e.g., `(a (b (c ())))`.
- Rule: `<> (a bat) (a black cat)`.
- Register: `?name` in the left or right side; repeated occurrences must match the same subtree.
### Minimal operational semantics
1. Parsing: read tokens into an AST of `Atom(value)` or `List([nodes...])`.
2. Matching: `match(pattern, tree, env)`
- If `pattern` is a register `?r` and `?r` unbound: bind `env[r] = tree`.
- If `pattern` is a register `?r` and bound: require structural equality with `env[r]`.
- If both atoms: require exact equality.
- If both lists: same arity; match element‑wise recursively.
- Otherwise: fail.
3. Rewriting: substitute registers in the right‑hand side using `env`, producing a new subtree.
4. Driver loop:
- Linearize the AST positions in left‑to‑right preorder over the serialized form.
- For each position, try rules in order; on first success, perform rewrite and restart from the beginning.
- If no rewrite happened in a full pass, halt.
### Numbers and common encodings
- Natural numbers: unary parentheses around `0`:
- `0` = 0, `(0)` = 1, `((0))` = 2, `(((0)))` = 3, ...
- Lists: nested pairs ending with `()` (nil): `(a (b (c ())))`.
### Examples
Rules:
```modal
<> (copy ?a) (?a ?a)
<> (swap ?x ?y) (?y ?x)
```
Input and result:
```modal
(copy cat) (swap bat rat)
(cat cat) (swap bat rat)
(cat cat) (rat bat)
```
Conditionals via boolean tables and a ternary (see reference):
```modal
<> (ife #t ?t ?f) ?t
<> (ife #f ?t ?f) ?f
```
Unary subtraction:
```modal
<> ((?a) - (?b)) (?a - ?b)
<> (?a - 0) (difference ?a)
```
### Side effects and IO
The language core is pure rewriting. Implementations may expose host effects via special registers. The reference uses `?:` to emit symbols to the console (e.g., `(print (sum ?:))`). Treat such registers as implementation‑defined hooks that consume or produce host effects during rewriting. Keep them minimal and explicit.
### Implementation guide (porting to another language)
- Data model:
- AST types: `Atom`, `List`.
- Rule: `{ left: Node, right: Node }`.
- Environment: map from register name to bound `Node`.
- Parser:
- Tokenize `(` `)` and atoms; build AST; preserve atom spelling verbatim.
- Identify registers by leading `?` at parse or match time.
- Matcher:
- Structural recursion with immutable `env`; fail fast on arity/shape mismatch.
- Registers are single‑assignment within a match; repeated occurrences unify.
- Rewriter:
- Deep substitute registers in `right` using `env`; do not capture or mutate `env` across matches.
- Evaluator:
- Left‑to‑right scan order over the current tree; rule priority is program order.
- On rewrite, replace exactly the matched subtree, then restart scanning from the root.
- Terminate when a full scan applies zero rewrites.
- IO hooks (optional):
- Dispatch atoms/registers like `?:` to host functions with explicit semantics.
- Keep IO operations deterministic relative to rewrite steps.
### Determinism and termination
- Determinism depends on rule order; different orders may yield different results.
- Termination is not guaranteed; design rules with explicit base cases.
### Repository layout
- `modal.c`: reference implementation (C).
- `logic.modal`: sample rules/programs.
### Further reading
- Original write‑up and worked examples: [Modal in a Postcard](https://wiki.xxiivv.com/site/modal).
|