ch:linear-types: ch:linear-types
Problem and result. Implement the finite two-context checker and file-token evaluator. The nine cases accept tensor swap, equal-residual branches, copying after bang elimination, and
Representation. Represent the unrestricted context as ordinary lookup data and thread the linear context as a residual list returned by checking. Represent the machine heap as a finite set of live file tokens. Annotating each syntax node with a pre-chosen context split would simplify checking, but would move the principal algorithmic decision out of the implementation.
First complete version. Implement variables and tensor. Check the function or first tensor component, pass its residual to the second component, and return the second residual. Require the final residual to be empty for a closed linear program.
Remaining cases. Add sums with equality of branch residuals, bang introduction over an empty linear context, and bang elimination into the unrestricted context. Then add open, read, and close transitions while checking that each live token is returned or consumed exactly once.
A failing version. Give the second tensor component the original linear context rather than the first component’s residual. A variable consumed by the first component is then available again. The mutation remains typechecking and audit-clean, but the duplication and positive split oracles fail.
Acceptance test. Require all nine named outcomes, the inline test, mutation rejection, a final empty live-token set for
Mathematical boundary. The program checks final residual emptiness and the final live-token set on the named finite cases; it emits no per-step ownership trace. It does not prove substitution, preservation, progress, cleanup, or cut elimination.