TAOCP 2.3.5 Exercise 11

The step M(x,y)=\text{visiting} \;\Rightarrow\; E(x,y)=\text{true} is invalid.

taocpmathematicsalgorithmsvolume-1

Section 2.3.5: Lists and Garbage Collection

Exercise 11. [**] [M30] Any List structure can be "fully expanded" into a tree structure by repeating all overlapping elements until none are left; when the List is recursive, this gives an infinite tree. For example, the List (5) would expand into an infinite tree whose first four levels are

Expanded tree for exercise 11

Design an algorithm to test the equivalence of two List structures, in the sense that they have the same diagram when fully expanded. For example, Lists $A$ and $B$ are equivalent in this sense, if

$$ \begin{aligned} A&=(a:C,b,a:(b:D))\ B&=(a:(b:D),b,a:E)\ C&=(b:(a:C))\ D&=(a:(b:D))\ E&=(b:(a:C)). \end{aligned} $$

Verified: yes
Solve time: 3m08s

1. Why the previous cycle rule is incorrect

The step

$$ M(x,y)=\text{visiting} ;\Rightarrow; E(x,y)=\text{true} $$

is invalid. A back-edge in the recursion stack only means that the pair $(x,y)$ is under investigation, not that it satisfies bisimulation constraints.

The missing logical point is this: bisimulation is a greatest fixed point defined by constraints on all successors, and a cycle is acceptable only if those constraints are satisfied globally for the entire cycle, not by local assumption at first encounter.

Thus, returning true immediately:

  • discards pending obligations on $(x,y)$,
  • allows a cycle to be accepted before checking consistency of all its induced constraints,
  • breaks soundness.

A correct method must ensure that every assumed equivalence is later justified by checking all constraints, not by premature acceptance.

2. Correct formulation of the problem

Each List structure induces a finite directed graph:

  • nodes are list objects,
  • each node has at most two outgoing edges:

$$ \mathrm{head}(x), \quad \mathrm{tail}(x), $$

  • atomic nodes carry labels.

Two nodes are equivalent iff they are related by the greatest bisimulation relation $R$, defined by:

  • if $x,y$ are atomic, then $\mathrm{val}(x)=\mathrm{val}(y)$,
  • if $x,y$ are non-atomic, then

$$ (\mathrm{head}(x),\mathrm{head}(y)) \in R \quad \text{and} \quad (\mathrm{tail}(x),\mathrm{tail}(y)) \in R. $$

We must compute whether $(P_0,Q_0)\in R$.

Since the set of nodes is finite, the product set of pairs is finite, so a greatest fixed point computation terminates.

3. Correct algorithm (worklist refinement)

Define:

$$ R \subseteq V \times V $$

initially:

$$ R_0 = V \times V $$

We iteratively remove pairs that violate bisimulation constraints.

Refinement rule

A pair $(x,y)\in R$ is invalid if:

  1. Atomic mismatch:

$$ x,y \text{ atomic and } \mathrm{val}(x)\neq \mathrm{val}(y) $$ 2. Structural mismatch:

$$ x \text{ atomic, } y \text{ non-atomic (or vice versa)} $$ 3. Transition failure:

$$ x,y \text{ non-atomic and } (\mathrm{head}(x),\mathrm{head}(y)) \notin R ;\text{or}; (\mathrm{tail}(x),\mathrm{tail}(y)) \notin R $$

4. Algorithm

Initialize R := V × V

Initialize a worklist W containing all pairs

while W is not empty:
    remove (x,y) from W

    if (x,y) ∉ R:
        continue

    if x and y are atomic:
        if val(x) ≠ val(y):
            remove (x,y) from R
        continue

    if exactly one of x,y is atomic:
        remove (x,y) from R
        continue

    // both are non-atomic
    if (head(x), head(y)) ∉ R or (tail(x), tail(y)) ∉ R:
        remove (x,y) from R
        add all pairs (u,v) such that
            (u,v) depends on (x,y) to W

A simpler equivalent version is:

  • repeatedly scan all pairs,
  • delete any violating pair,
  • continue until no change.

Finally, output whether $(P_0,Q_0)\in R$.

5. Why this fixes the cycle problem

Cycles are handled correctly because:

  • no pair is ever assumed valid prematurely,
  • a pair survives only if all its required successor pairs also survive,
  • if a cycle is inconsistent, some constraint eventually fails and propagates removal through the cycle,
  • if a cycle is consistent, no deletion ever occurs, so it remains in the fixed point.

Thus cycles are not “trusted”, they are validated by global constraint satisfaction.

6. Correctness argument

Lemma 1 (Monotonicity)

The refinement process is monotone decreasing:

$$ R_0 \supseteq R_1 \supseteq R_2 \supseteq \cdots $$

since pairs are only removed.

Lemma 2 (Preservation of bisimulation)

If $R_i$ contains a true bisimulation relation $S$, then all deletions preserve correctness, because a pair is removed only if it violates a bisimulation condition.

Thus the true bisimulation relation is never removed.

Lemma 3 (Stability implies bisimulation)

At termination, let $R^$ be the final set. Every pair in $R^$ satisfies:

  • atomic agreement,
  • closure under head and tail transitions.

Thus $R^*$ is a bisimulation.

Lemma 4 (Greatest fixed point)

Since we start from all pairs and remove only invalid ones, $R^*$ is the greatest bisimulation relation.

7. Termination

The set $V\times V$ is finite. Each iteration removes at least one pair or stops. Hence at most $|V|^2$ deletions occur, so the algorithm terminates.

8. Final conclusion

Two List structures are equivalent under full expansion iff their root pair remains in the greatest fixed point $R^*$ computed by iterative elimination of non-bisimilar pairs.

This removes the unsafe “visiting implies true” rule entirely and replaces it with a global constraint system that correctly validates even cyclic structures.