Chapter 42Optional

Optimal Sharing and Graph Reduction

Prerequisites. Direct starred prerequisites: Chapter 41. No later core chapter depends on this route.

Consider the finite untyped term $M = (λ x . x x) ((λ y . y) z) .$ Its outer beta step copies the argument: $M ⟶_{β} ((λ y . y) z) ((λ y . y) z) .$ The two displayed residuals belong to one Lévy family: they descend from the single redex $(λ y . y) z$ in $M$ . Tree reduction may contract both copies and repeat that family’s work. Optimal sharing asks for a graph that represents the argument once and never duplicates a family contraction. The residual vocabulary is the one fixed in definition 41.11; here labels remember residual ancestry even when graph rewrites duplicate the surrounding representation.

One shared node, calculated

A directed-acyclic sharing skeleton already exposes the distinction. Let $r$ name the single node representing $(λ y . y) z$ , and let an application node have two edges pointing to $r$ : Mathematical diagram Diagram Two incoming edges represent two uses, but there is only one node to rewrite. This is ordinary graph sharing. Recognizing one Lévy family through later rewrites requires the labeled calculus introduced in the next section.

Definition 42.1 — The opening labeled term graph ¶

For finite untyped lambda terms $N, P$ , a labeled term graph in the opening fragment has the form $letgraph s^{a} = N in P,$ where $s$ is a graph-node name, $a \in N$ is a family label, and every free occurrence of $s$ in $P$ points to that single node. Readback expands the node name: $R_{let} (letgraph s^{a} = N in P) : = P [R_{let} (N) / s],$ with $R_{let}$ homomorphic on variables, abstractions, and applications. The shared-beta operation is ${contract}_{let} (letgraph s^{a} = (λ y . Q) R in P) : = letgraph s^{a} = Q [R / y] in P .$ Substitution in the node body is capture avoiding. The operation changes the body once and retains both the incoming edges and label $a$ . This finite fragment is an executable illustration, not the GAL fan calculus.

Referenced from 4 locations

The outer source contraction is represented by $\begin{aligned} H_{0} & : = letgraph s^{a} = (λ y . y) z in s s, \\ H_{1} & : = {contract}_{let} (H_{0}) = letgraph s^{a} = z in s s . \end{aligned}$

Proposition 42.2 — One graph contraction discharges both residuals ¶

The node name and family label of $H_{0}$ remain $s$ and $a$ in $H_{1}$ , and $R_{let} (H_{0}) ⟶_{β}^{*} R_{let} (H_{1}) .$ The readback path contracts exactly the two residuals created by the outer source contraction.

Referenced from 4 locations

Proof of Proposition 42.2 — One graph contraction discharges both residuals

Proof. Equation (42.1) changes only the stored body. Readback gives $\begin{aligned} R_{let} (H_{0}) & = ((λ y . y) z) ((λ y . y) z) \\ \overset{l e f t β}{⟶_{β}} z ((λ y . y) z) \\ \overset{r i g h t β}{⟶_{β}} z z \overset{r e a d b a c k}{=} R_{let} (H_{1}) . \end{aligned}$ Both occurrences of $s$ read the one updated body. ◻

The Gonthier–Abadi–Lévy graph interface

The imported result uses Gonthier, Abadi, and Lévy’s bus presentation of Lamping-style sharing graphs. The following convention fixes every object that appears in the theorem; it also records where the source remains diagrammatic.

Convention 42.3 — GAL graph system ¶

A bus is a finite ordered bundle of parallel wires. A GAL graph is a finite undirected port graph assembled from five node forms:

Node	Bus presentation	Role
root	one incident bus	closes a result or variable edge
void	one incident bus	terminates an unused branch
croissant	unary on a bus slice	creates one wire ex nihilo
bracket	terminal on two slices	combines two wires
fan	three buses, total arity $3 n$ at width $n$	shares a bus

A fan has one marked main level; the other bus levels carry no context mark. Its three buses have corresponding rightmost wires, and the incident ports on those wires are rightmost fan ports.

The full one-step relation $G ⟶_{GAL} G^{'}$ is contextual closure of the six bus-rule schemes in GAL Figure 2: compatible facing fans annihilate; fans at different marked levels commute into the rectangular fan wiring; facing brackets annihilate to straight bus wires; facing croissants disappear; and a bracket or croissant propagates through a fan by splitting over its two branches. Bus widths determine every parallel copy and boundary connection. The basic system excludes the optional garbage-collection rules discussed in GAL §3.2, before the operator decomposition of §3.3. A graph normal form has no instance of any of these six schemes. Write $⟶_{GAL}^{*}$ for reflexive-transitive closure. This definition imports the incidence diagrams of GAL Figure 2 rather than redrawing a selectively simplified rule set.

Referenced from 4 locations

Definition 42.4 — Diagrammatic translation ¶

For a finite untyped lambda term $P$ , $G (P)$ is the graph produced by the inductive diagrams of GAL §4.1:

A variable is a bus of width three, with one result edge and one edge bearing its variable name.
For $P Q$ , place $G (P)$ and $G (Q)$ side by side. The upper fan sends the call into $P$ , routes the reply to the result, and routes the argument request to $Q$ ; the adjacent croissant creates the null offset for that call. For each variable free in both subterms, a lower fan merges the two named buses while retaining their distinct offsets.
For $λ x . P$ , feed the bus named $x$ back through the abstraction fan. If $x \notin FV (P)$ , terminate that branch with a void. Put a bracket on every other free-variable bus so that its address is restored on leaving the scope; the dual croissant removes that offset when the bus returns.

The second stage forgets edge directions, moves variable names to roots, and adds roots to the result and free-variable edges. Left, middle, and right within every bus are those shown in the diagrams; they are not quotient data. The source explicitly calls this translation informal because a set-theoretic definition would first have to construct those left/right bus positions. Accordingly, $G$ here names that fixed diagrammatic translation and no theorem below is claimed for an independently invented graph encoding.

Referenced from 6 locations

A graph is reachable and well formed for $P$ when $G (P) ⟶_{GAL}^{*} G$ . This reachability condition, rather than an unchecked local degree test, is the domain of the imported readback theorem.

Definition 42.5 — Access-path readback ¶

An access path starts at the top root with a star-free context and follows directed bus edges whose adjacent contexts agree, except for the source’s shunt step that transfers a suffix between the input and output contexts. Readback $R (G)$ follows all downward paths consistent on every wire except the rightmost one. Each rightmost fan encountered contributes an application, abstraction, or variable node according to its orientation. A variable is bound by the abstraction reached with the same left context; nested abstractions have distinct left-spine lengths. If the minimal search for a root diverges, readback is the unsolvable Böhm tree $Ω$ .

For graphs reachable from $G (P)$ , access-path shunting makes this procedure independent of arbitrary input offsets. Thus $R$ is a partial procedure on arbitrary port graphs but is the readback used by GAL Theorem 3 on the reachable graphs quantified over below.

Referenced from 3 locations

Labels, readback, and qualified optimality

Labels are placed on rightmost wires of $G (P)$ . They commute through every node except a rightmost fan and concatenate when graph reduction joins labeled edges, with concatenation reversed when the edge orientation is reversed. When a label is caught between two facing rightmost fans, contraction copies that label to the outgoing rightmost wires. That caught word is the redex label. We write $G \to_{GAL : (u, v)}^{a} G^{'}$ when one step of the full GAL relation contracts the facing rightmost-fan ports $u, v$ with redex label $a$ . The parameterized arrow is a subrelation of $⟶_{GAL}$ ; $⟶_{GAL}^{*}$ always closes the full six-scheme relation.

For the opening term, the translation and readback obligations form the following worked calculation. Let $G_{0} = G (M)$ . The translated application/abstraction interaction reaches $G_{1}$ , whose readback is the outer source contractum. A rightmost-fan contraction then reaches $G_{2}$ : $\begin{aligned} G_{0} & ⟶_{GAL}^{*} G_{1} \to_{GAL : (u_{a}, v_{a})}^{a} G_{2}, \\ R (G_{0}) & = M, \\ R (G_{1}) & = ((λ y . y) z) ((λ y . y) z) ⟶_{β} z ((λ y . y) z) ⟶_{β} z z = R (G_{2}) . \end{aligned}$ The first line states graph incidence and label propagation; the remaining lines are readback. A finite certificate may record $⟨ (u_{a}, v_{a}), a, R (G_{1}) ⟶_{β}^{*} R (G_{2}) ⟩$ , but the record is not evidence that $u_{a}, v_{a}$ face in a translated graph.

Theorem 42.6 — Readback and family nonduplication, imported ¶

For every finite untyped lambda term $P$ :

$R (G (P)) = P$ modulo alpha-equivalence.
If $G (P) ⟶_{GAL}^{*} G$ and $G ⟶_{GAL}^{*} G^{'}$ , then $R (G) ⟶_{β}^{*} R (G^{'})$ . If such a reachable $G$ is a graph normal form, $R (G)$ is beta-normal.
During reduction, no two redexes of rightmost fans have the same label. Hence graph reduction never duplicates contraction of one Lévy family.

Referenced from 8 locations

Proof of Theorem 42.6 — Readback and family nonduplication, imported

Imported proof. Source boundary. Clauses 1 and 2 are GAL Theorem 3 and clause 3 is Theorem 4, both in the local author copy at printed p. 11. Theorem 4’s proof sketch continues onto p. 12 [GAL92]. Their translation is explicitly diagrammatic and informal; definition 42.4 preserves that boundary. Theorem 4 calls the resulting reductions optimal, but the adjacent qualification matters: family work is not duplicated, yet a reduction may still evaluate a subterm later found useless. A normal-order strategy, such as leftmost-outermost, avoids that useless work. Thus family nonduplication does not make every scheduler time- or space-optimal. ◻

Exercise 42.1 ¶

★★☆ Apply definition 42.4 to $(λ x . x x) ((λ y . y) z)$ . List the variable buses before the second translation stage, identify the fan that merges the two uses of $x$ , and state where a bracket or void would be inserted in $λ x . λ w . x$ . Which part of the answer depends on the source’s left/middle/right bus convention?

Referenced from 3 locations

Exercise 42.2 ¶

★★☆ For the worked $G_{0}, G_{1}, G_{2}$ calculation, separate three claims: graph reachability, uniqueness of the redex label, and the ordinary beta readback path. Name the definition or theorem clause that licenses each claim. Then explain why replacing $⟶_{GAL}^{*}$ by a closure of rightmost-fan steps alone would invalidate the graph-normal-form clause.

Referenced from 3 locations

Parallel beta is not a machine cost

The lower bound of Asperti and Mairson concerns simply typed terms, not the untyped GAL signature. We therefore freeze its separate vocabulary.

Definition 42.7 — Asperti–Mairson cost signature ¶

Simple types and explicitly typed terms are $A, B ::= o ∣ A ⟶ B, P, Q ::= x^{A} ∣ λ x : A . P ∣ P Q .$ Let $Bool : = o ⟶ o ⟶ o$ . Type and term size are $\begin{aligned} | o | & = 1, & | A ⟶ B | & = 1 + | A | + | B |, \\ | x^{A} | & = | A |, & | λ x : A . P | & = 1 + | P |, & | P Q | & = 1 + | P | + | Q | . \end{aligned}$ A parallel beta step contracts all residuals in one Lévy family simultaneously; a parallel normalization is a sequence of such family steps. A first-class machine model is Turing-complete with at most polynomial simulation slowdown; logarithmic-cost register machines qualify, whereas unit-cost counter machines do not. Finally, $K_{0} (n) = n, K_{j + 1} (n) = 2^{K_{j} (n)} .$ For fixed $j$ , $K_{j}$ is one level of the Kalmár-elementary hierarchy.

Referenced from 2 locations

Optimal Sharing and Graph Reduction

The lower bound uses four facts whose scopes must remain visible. The first two turn term size into a family-step bound. The last two turn a hypothetical unit-cost implementation into a forbidden decision procedure.

Proposition 42.8 — Prerequisite package for the cost obstruction ¶

Fix $ℓ \geq 0$ and a deterministic Turing machine $M$ . The Asperti–Mairson construction has the following properties.

For every explicitly typed term $F$ , typed eta-expansion followed by the sharing-graph translation produces a graph $Φ (F)$ satisfying $[P h i (F)] \leq 2 | F |$ .
Every fan in $Φ (F)$ has atomic type. Hence fan propagation creates no lambda or application node, and a family contraction removes one lambda–application pair. A normalization of $F$ therefore has at most $2 | F |$ parallel beta steps.
For each input word $x$ , there is a higher-order formula $φ_{x}$ of size $O (| x |)$ such that $φ_{x}$ is true if and only if $M$ accepts $x$ within $K_{ℓ + 1} (| x |)$ steps. The powerset hierarchy in the formula is bounded by a level depending on $ℓ$ , not on $x$ .
The formula $φ_{x}$ compiles to a closed explicitly typed term ${\hat{φ}}_{x} : Bool$ . There is a constant $c = c (M, ℓ)$ , independent of $x$ , such that $| {\hat{φ}}_{x} | \leq c | x |$ , and ${\hat{φ}}_{x}$ normalizes to $λ t : o . λ f : o . t$ if and only if $M$ accepts $x$ .

Referenced from 3 locations

Optimal Sharing and Graph Reduction

Proof of Proposition 42.8 — Prerequisite package for the cost obstruction

Proof. For (i), eta-expand a variable of type $A ⟶ B$ until every fan is at the base type $o$ . Propagating a fan through the expansion duplicates only the expansion tree. If a bound variable $x : A$ occurs $μ (x)$ times, the translation first removes $(μ (x) - 1) | A |$ copied type contributions from the term representation and then adds at most $(1 + μ (x)) | A |$ graph nodes. Summing over the nontrivial variables gives $[Φ (F)] \leq | F | - \sum_{x} μ (x) | A_{x} | + \sum_{x} (1 + μ (x)) | A_{x} | = | F | + \sum_{x} | A_{x} | \leq 2 | F | .$ This is Theorem 3.12 of Asperti and Mairson. The eta-expansion forces atomic fan types. It is not counted as a beta reduction of the input.

For (ii), atomic fans cannot meet a lambda or application at functional type. No reduction can consequently create either kind of node. Each family contraction removes one node of each kind, so their number is bounded by $[Φ (F)]$ . This is their Theorem 3.13 together with (i).

For (iii), encode the finite base set as a Boolean tuple and encode its iterated powersets by typed Church lists. Membership, subset, and equality at level $j + 1$ are obtained by iterating the level- $j$ operations over that list. A bounded computation tableau for $M$ is then a higher-order formula: one quantified relation records the transition relation, and another records its reflexive transitive closure. With $M$ and $ℓ$ fixed, all universe levels are constants; only the input tableau contributes to the linear size. This reconstructs their Theorem 5.1.

For (iv), compile disjunction, conjunction, negation, and implication to their Church Boolean terms. Compile a quantifier over a finite type to iteration over the corresponding list: universal quantification folds conjunction from $true$ , and existential quantification folds disjunction from $false$ . Abstracting the repeated constructors prevents their copies from enlarging the term. Thus the compiled term has size at most $c | x |$ , while its Boolean normal form records the truth of $φ_{x}$ . This is their Theorem 4.3 and Corollary 5.2. The four constructions and bounds are exactly those used below; no claim about a scheduler or a graph representation has entered them. ◻

The statement and construction are Asperti–Mairson Theorem 5.3 on printed p. 24 [AM01]. Unit cost per family step would give a linear implementation-time bound and therefore contradict the theorem. The separation is between a semantic family count and all concrete work assigned to its implementation; it does not identify which bookkeeping operation pays the lower bound.

Corollary 42.10 — Transfer to Lamping graph reduction, imported ¶

For every fixed $ℓ \geq 0$ , there is a family $E_{n} : Bool$ normalizing in $O (n)$ parallel beta steps for which Lamping’s graph-reduction algorithm requires $Ω (K_{ℓ} (n))$ local graph-interaction steps.

Referenced from 2 locations

Optimal Sharing and Graph Reduction

Proof of Corollary 42.10 — Transfer to Lamping graph reduction, imported

Imported proof. This is Asperti–Mairson Corollary 5.4 on printed p. 24. It counts interactions of lambda, application, and fan nodes together with the croissant/bracket interactions that manage indices. The transfer uses their observation that Lamping’s local graph operations form a first-class machine with polynomial overhead. It is a theorem about that algorithm, not an automatic lower bound for every graph reducer or runtime representation. ◻

Corollary 42.11 — Ordinary versus parallel beta, imported ¶

Fix $ℓ \geq 0$ . If $b_{E}$ and $p_{E}$ denote, respectively, the ordinary and parallel beta steps in a normalization of $E$ , there is an infinite family of normalizing terms with $b_{E} = Ω (K_{ℓ} (p_{E})) .$

Referenced from 2 locations

Optimal Sharing and Graph Reduction

Proof of Corollary 42.11 — Ordinary versus parallel beta, imported

Imported proof. This is their Corollary 5.6 on printed p. 25. It separates the number of family contractions from ordinary beta work before any graph representation or scheduler is chosen. Neither corollary is a wall-clock, memory-use, or parallel-speedup claim; those require a concrete implementation, allocation policy, scheduler, machine, and measurement protocol. ◻

Exercise 42.3 ¶

★★☆ Compute $K_{0} (3), K_{1} (3), K_{2} (3)$ . Then make a four-column ledger for parallel beta steps, ordinary beta steps, local Lamping interactions, and wall-clock time. Place the theorem and two corollaries of section 42.4 in the strongest columns they justify, and state one additional hypothesis needed to move any claim into the wall-clock column.

Referenced from 3 locations

What the executable certificate establishes

The Kappa companion checks the opening let-graph and a finite certificate syntax. A certificate endpoint is a natural-number identifier tagged left-rightmost, right-rightmost, or auxiliary. A trace entry is $((u, r_{u}), (v, r_{v}), a, [t_{0}, \dots, t_{k}]),$ where $u \neq v$ , the endpoint tags are opposite rightmost tags, $a \in N$ , $k \geq 1$ , and each $t_{i} ⟶_{β} t_{i + 1}$ is a root contraction or one compatible congruence step, modulo alpha-equivalence. A trace is accepted only when its labels are pairwise distinct. The maintained invariant is that accepted entries have distinct endpoints, opposite tags, a nonempty verified beta path, and a label not used by any earlier accepted entry.

This format audits supplied finite data. It does not decide whether two endpoints are incident to facing fans in a GAL graph, whether the graph lies in the image of $G$ , or whether a label reached them by GAL propagation. Those are semantic premises of theorem 42.6.

None of these problems is a prerequisite for a later chapter.

Suggested first pass.

Compute the opening readbacks, audit the GAL import boundary, separate the three cost measures, and only then extend the certificate checker.

Exercise 42.4 ¶

★★☆ Fill the three fields of the opening certificate $⟨ (u_{a}, v_{a}), a, R (G_{1}) ⟶_{β}^{*} R (G_{2}) ⟩ .$ Give the complete two-step ordinary-beta path to $z z$ , using $⟶_{β}$ for each contraction.

Referenced from 3 locations

Exercise 42.5 ¶

★★★ Reconstruct the use of GAL Theorem 3 in theorem 42.6. State both reachability hypotheses, explain why full graph reduction rather than the labeled-fan subrelation is required, and identify the point where the source supplies only a proof sketch. Then give a reduction strategy under which Theorem 4’s useless-work caveat is discharged.

Referenced from 3 locations

Exercise 42.6 ¶

★★☆ Construct a certificate whose endpoint tags, beta path, and fresh label all pass the finite checker but whose endpoints do not belong to one graph. Which premise of theorem 42.6 is absent? Explain why acceptance must not be reported as an optimality proof.

Referenced from 3 locations

Exercise 42.7 ¶

★★☆ Suppose a reducer reports ten family contractions, ten thousand local graph interactions, and eight milliseconds. Classify each number using section 42.4. State why none of the three determines either of the others without a simulation and cost relation.

Referenced from 3 locations

Exercise 42.8 ¶

★★★ Practical project.optimal-sharing-auditor Implement the labeled term graph of definition 42.1, its shared-beta operation, and readback in Kappa. Maintain the node-name and family-label invariants through contraction. Then implement the finite certificate checker of section 42.5, maintaining its four entry invariants after every accepted item. Check the preserved node name, preserved label, and complete readback calculation of proposition 42.2. Include one crossed-binder beta step that requires freshening. Reject an invalid tag pair, an empty or non-beta path, and a repeated label independently. A typechecking mutation must target each invariant, and each isolated negative case must fail. Appendix E records the commands and appendix F develops the checker.

Referenced from 4 locations