Index of everything on this site: https://ai.hiina.space/index.md
A Covenant circle is an interaction net. Seals (triangles inscribed in small circles) are agents, their vertices are ports, and straight chords between vertices are wires. Running the circle means rewriting it: when two seals face each other eye to eye, they react by a fixed local rule and the circle redraws itself. There are only three seal types, Lafont's interaction combinators, which are universal. The semantics is purely topological, so the drawer can lay the circle out with any symmetry without changing its meaning: flair is free. Covenant is the photograph-of-ink design, and its parser turns connectivity, the hardest part of diagram recognition, into a perfect-matching problem.
| Visual element | Meaning |
|---|---|
| Boundary ring, with notches ("gates") | The net's interface; free ports; the result is read from the gates |
| Seal: triangle inscribed in a small circle, plain | γ (constructor), 1 principal + 2 auxiliary ports |
| Seal with an inner crescent | δ (duplicator), 1 + 2 ports |
| Small circle with one tick and a cross | ε (eraser), principal port only |
| Filled dot ("eye") on one vertex | That vertex is the principal port |
| CCW from the eye: first vertex, second vertex | aux1, aux2 (so mirroring a seal swaps them) |
| Straight chord between two ports | A wire; every port has exactly one |
| Chord joining two eyes | An active pair, which will react |
| Seal size, position, rotation, chord crossings | Nothing |
Model and evaluation. This is the symmetric variant of Lafont's interaction combinators (Lafont 1997; the symmetric form studied by Mazza). A net is a set of agents plus a perfect matching on all ports and gates. Annihilation, for two agents of the same type α ∈ {γ, δ}: α(a, b) ⋈ α(c, d) → wires a–c and b–d. Commutation: γ(x, y) ⋈ δ(r₁, r₂) → γ'(r₁, a, b), γ''(r₂, c, d), δ'(x, a, c), δ''(y, b, d), where each new agent's principal points outward to the listed port and a, b, c, d are fresh internal wires. Erasure: ε ⋈ α(a, b) → ε at a and ε at b, and ε ⋈ ε → nothing. Interaction nets are strongly confluent, so every reduction order gives the same normal form, and the animation can fire every active pair at once with no scheduling rule to explain. Normal form is reached when no chord joins two eyes.
The λ-calculus compiles in the standard way: λx.M is a γ whose principal is the term's root, with aux1 = body and aux2 = x; application M N is a γ whose principal attaches to M, with aux1 = result and aux2 = N; δ shares variables and ε discards them. The honest caveat is that this plain encoding is correct only for terms where duplicators never need to tell each other apart. The general case needs labelled duplicators, as in Lamping's optimal reduction and in HVM.
Worked example: (λx.x) y. A boundary ring has two gates, Y at 1 o'clock and R at 5 o'clock. Inside are two plain γ seals side by side, eyes facing across the centre and joined by a horizontal chord. The left seal L is λx.x: its two aux vertices are joined by a short chord, the "identity knot". The right seal A is the application: its aux1 (lower-right vertex) runs to R and its aux2 (upper-right vertex) runs to Y.
┌──────── gate Y
aux1 │ aux2
┌────○ ○
│ ╲ ╱
│ ● ═════ ● ● = eye (principal), ═ = active pair
│ ╱ L:γ ╲ A:γ
└────○ ○
aux2 │ aux1
└──────── gate RIn text form, each wire name appears exactly twice and gates once:
gates R Y
γ(w, k, k) # L
γ(w, R, Y) # A| Step | What happens | Net after |
|---|---|---|
| 1 | The single active pair is L–A via w; annihilation connects k–R and k–Y | R–k–Y |
| 2 | Both seals vanish and wire k collapses | One chord R–Y |
| 3 | No eyes remain: normal form; the result gate is wired to the input gate | The answer is y |
On paper, the two facing triangles dissolve into a single chord sweeping down the right side of the ring. A second example shows growth: δ(w, R₁, R₂) facing γ(w, X, Y), with all four aux ports going to gates, commutes in one step into four seals, two γ's facing R₁ and R₂ and two δ's facing X and Y, cross-wired by four chords. A pair has been copied, and the circle visibly gains a square of seals.
Mishaps. A dangling or forked port (zero chords, or two or more) is a linearity violation, so the circle refuses to run and the port pulses red. A chord passing within ε of a third port is flagged as ambiguous, not guessed. A non-terminating net (a δ–γ pair feeding itself) grows until the step or agent budget runs out, and the circle fills with seals until they press against the boundary, then freezes. A "vicious circle", a cycle whose principal ports all point along it, never reduces and is shown greyed as inert.
Parsing. From an image, which is the reason for the
design: rectify using the boundary ring; find seals with Hough circles
in a radius band; take each seal's three vertices where its inner
triangle meets its circle, the eye as the filled blob nearest a vertex,
and the interior mark (none, crescent or cross) from a three-class
template or tiny CNN. Ports and gates then form a known point set P,
typically 10 to 40 points. For every pair (i, j), score straight-line
ink coverage by sampling the segment and taking the fraction of dark
pixels within the stroke width. Since each port has exactly one chord,
take the maximum-weight perfect matching on those scores (Edmonds'
blossom algorithm, for example
networkx.max_weight_matching), and accept it if every
chosen edge clears about 0.85 coverage (guess) and the runner-up
matching is clearly worse; otherwise ask the user. This sidesteps
arrowhead detection entirely, because direction comes from eyes, and it
handles crossings, because each candidate is a straight segment between
known points. The weak points are curved chords (disallowed for now;
skeleton tracing could add them), chords grazing other ports, and an eye
dot confused with an ink blot. A trained seal detector on synthetic nets
is a reasonable upgrade; a VLM is not, since wire topology is exactly
what FlowLearn shows it gets wrong. In VR, strokes give chords directly,
with endpoints snapped to the nearest port.
New versus borrowed. Interaction nets and combinators come from Lafont (1990, 1997), the symmetric variant from Mazza, the λ-encoding and its labelling caveat from Lamping, rewriting as a visible game from Alligator Eggs, vertices as attachment points from Rithmatic bindpoints, and rewriting rings from VIPR. The seal-and-chord notation and the perfect-matching chord parser are new; the design pass had not seen either elsewhere. Untested: whether chord coverage stays separable at about 40 ports in a phone photo.
Text licensed CC BY 4.0 (attribution: Hiina, ai.hiina.space). Source: https://github.com/hiinaspace/ai-hiina-space