appendix sectionrules

GAL sharing graphs and the parallel-beta cost signature

A GAL bus is an ordered bundle of wires. Graphs use root, void, croissant, bracket, and fan nodes. At bus width $n$ , a fan has total arity $3 n$ and one marked main level. The full relation $⟶_{GAL}$ is contextual closure of the six bus schemes in Gonthier–Abadi–Lévy Figure 2, without their optional garbage rules; $⟶_{GAL}^{*}$ is its reflexive-transitive closure. A labeled rightmost-fan contraction is written $G \to_{GAL : (u, v)}^{a} G^{'}$ . The parameterized relation is a subrelation of the full graph step, not the relation whose closure defines graph normality.

The diagrammatic term translation is fixed by three clauses: a variable is a width-three bus; application combines the function and argument graphs with an upper call fan and one lower fan for every shared free variable; abstraction feeds the bound-variable bus through an abstraction fan, uses a void when the binder is absent, and brackets every remaining free-variable bus. A second stage forgets directions, moves names to roots, and adds roots. Readback follows access paths consistent on all but the rightmost wire and reconstructs syntax at rightmost fans. These are the precise imported diagrammatic objects of convention 42.3, definition 42.4, definition 42.5.

For the separate typed cost result, $A, B ::= o ∣ A ⟶ B, P, Q ::= x^{A} ∣ λ x : A . P ∣ P Q,$ with $Bool = o ⟶ o ⟶ o$ , and $\begin{aligned} | o | & = 1, & | A ⟶ B | & = 1 + | A | + | B |, \\ | x^{A} | & = | A |, & | λ x : A . P | & = 1 + | P |, \\ | P Q | & = 1 + | P | + | Q | . \end{aligned}$ One parallel beta step contracts one complete Lévy family. The elementary hierarchy is $K_{0} (n) = n$ and $K_{j + 1} (n) = 2^{K_{j} (n)}$ .