ch:inductive-types: ch:inductive-types

Problem and invariant. Construct the polarity traversal required by the seminar. Maintain the invariant that every recursive occurrence is visited with positive sign, and retain a constructor path when the traversal finds a negative occurrence.

Two representations. One can use a signed syntax-tree traversal, or a datatype-description language whose constructors enforce positivity. The companion uses the signed traversal and returns a Boolean. The complete project enriches the negative result with the path requested in the exercise.

First complete version. Implement atoms and recursive occurrences, extend through products, then reverse the sign at arrow domains. After each stage, add one positive case and one nearby malformed case before extending the syntax.

Observable result. The accepted corpus accepts the natural-number, list, and W-tree signatures, and rejects $(D\to D)\to D$ while accepting $D\to D$ as a whole constructor type. It prints four named PASS lines and then All 4 Chapter 73 corpus cases passed. A rejected input is represented by a false decision or None; the main oracle negates that result when rejection is expected.

A failing version. Preserve rather than reverse the sign in an arrow domain. The nested negative input $(D\to D)\to D$ is then accepted. This mutation still typechecks, but the named rejection oracle fails, so the inline test harness exits nonzero.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact five-line run transcript, and an empty audit. Restore the accepted source after replaying the mutation and repeat all four commands.

Mathematical boundary. The program decides the finite representation and cases just described. It does not prove polynomial set soundness in proposition 73.44 or normalization of the inductive extension; those claims remain mathematical results with the stated boundaries.