ch:relational-parametricity: ch:relational-parametricity

Problem and result. Build the finite relation calculator required by exercise 10.10. The finished program computes both counter implementations through $c_2$, checks their output relation, checks identity and graph instances with arrow lifting, and rejects a singleton fixed-point relation because it omits the bottom pair.

Representation. Use one Kappa datatype Value with bottom, natural, and natural–Boolean-pair cases. A relation is a decidable Kappa function Value -> Value -> Bool; a RelatedPair list supplies the finite inputs over which an arrow-lifting instance is checked. This split keeps the counter invariant exact while recording the finite witnesses that the run actually enumerates. A normalized System F abstract syntax with beta-class representatives would track the chapter more literally, but it would bury the relation operations under an evaluator. The tagged values are the smaller adequate surrogate for this project.

First complete version. Implement structural equality on Value. Define identity by that equality and define a graph by comparing the output of its supplied function with the proposed right endpoint. Define arrowHolds to visit every supplied RelatedPair, first checking the domain relation and then checking the two function outputs in the codomain relation. The first end-to-end probe uses the pair NatValue 2/NatValue 3 in the graph of successor.

Counter obligations. Define the counter relation by relating NatValue n to PairValue n False. Check the initial pair directly. Check the two step inputs traversed by $c_2$, and check observer inputs at zero, one, and two, with arrowHolds. Run $c_2$ independently with the natural and pair operations. Require both outputs to be NatValue 2, then check their beta-identity surrogate. Each output line names the precise witness or finite witness family used.

Graph and fixed-point cases. Use the successor graph pairs at zero, one, and two to check the graph-lemma square. For the fixed-point boundary, use the singleton relation containing only NatValue 3/NatValue 3. The identity functions pass the enumerated arrow check, but the relation fails the separate strictness test because Bottom/Bottom is absent. This separates the failed premise from the otherwise successful finite arrow instance.

A failing version. Apply mutant-ignore-strictness.patch to a disposable copy. It deletes only the bottom-pair conjunct in fixedPointRelationValid. The mutant still checks, but the fixed-point oracle prints FAIL and the conditional final line becomes Chapter 10 corpus failed.

Acceptance test. Run Kappa check, test, run, and audit on corpus.kp. Require all ten named PASS lines, the exact final line All 10 Chapter 10 corpus cases passed., one passing harness test, and audit []. Then apply the preserved mutation and require check success together with test failure on both the strictness oracle and the aggregate.

Mathematical boundary. The program exhausts only its displayed witness lists. It does not quantify over all closed beta-classes, so it proves neither the abstraction theorem, the graph lemma, nor the full counter arrow obligations. Its identity function is the finite value surrogate, not a semantic identity-extension lemma. Its bottom test exposes strictness but supplies no chains, least upper bounds, continuity proof, or admissibility proof.