ch:mutable-value-semantics: ch:mutable-value-semantics

Problem and invariant. Decide whether two finite access paths are independent. Maintain the invariant that both component lists are stable: every array index is literal. After that global check, acceptance requires a first pair of components known to select distinct tree children; reaching the end of either path means overlap.

Two representations. Use a root identifier and a list of components. Components are fields, constant indices, or unknown indices. Keeping unknown indices distinct from constants makes the conservative rejection branch inspectable. A trie shares common prefixes and accelerates a many-path audit, but obscures the first pairwise divergence; lists follow the metatheoretic induction and are preferable for this six-case corpus.

First complete version. First reject either path unless its complete component list is stable. After that check, different roots are independent. For a shared root, consume equal fields or equal constant indices; accept at distinct fields or distinct constant indices; and reject when either list ends. Return a verdict carrying its reason rather than recomputing an explanatory walk after the Boolean decision. Both independent and the printed reason must project from that one verdict.

Remaining cases in proof order. Add equal fields, distinct fields, equal constants, distinct constants, and either-list exhaustion. Then test unknown indices both below a shared prefix and below different roots. These last cases are emphasized in lemma 49.6 because runtime equality cannot be ruled out syntactically.

Observable result. The corpus prints six named PASS lines: two accepted divergences, equal-path and prefix rejections, nested unknown-index rejection, and different-root unknown-index rejection. The four rejections compute and print their decisive reason. The run then prints All 6 Chapter 49 corpus cases passed.

A failing version. Change the unknown-index branch of the global stability check from false to true. The program still type-checks and audits cleanly, but the different-root unknown-index oracle fails.

Acceptance test. Run the four Appendix E commands with packaged Kappa v0.3.0. Require a silent check, a passing inline test, the exact seven-line transcript, and an empty audit. Restore the accepted source after the mutation and repeat all four commands.

Mathematical boundary. The checker assumes well-typed finite tree paths. It does not construct a Swiftlet typing derivation, evaluate an array index, or prove that accepted paths have disjoint pointer-store representations. The relevant metatheorem is lemma 49.6; this finite execution illustrates its case split but does not prove it.