Lectures onType Theory
ch:subject-dependent-self: recursive polarity
appendix sectiontutorials

ch:subject-dependent-self: recursive polarity

Exercise 94.5.

Problem and invariant. Check polarity of a single recursive variable and equality of displayed/substituted subject tags. Every accepted recursive occurrence must be positive.

Two representations. Signed syntax paths produce rich diagnostics; the selected Boolean-sign traversal is smaller and sufficient for the named positive, negative, and double-negative probes.

First complete version. Add constants and the recursive variable, then products at unchanged polarity and arrows with a flipped domain sign. Add finite subject tags and explicit equality before the five output oracles.

Observable result. The run ends All 5 Chapter 94 corpus cases passed.

A failing version. Preserve polarity in the arrow domain. The negative-arrow oracle changes to FAIL; the test exits 1.

Acceptance and boundary. Run all four commands and require exact stdout plus []. The traversal checks printed side conditions; it does not establish preservation or strong normalization.

Search the book

Type to search the local edition.