ch:pure-type-systems: ch:pure-type-systems

Problem and result. Check the four product axes of a finite PTS specification and one bounded conversion case. The accepted run has five outcomes: it recognizes the polymorphic identity in ${\lambda }_2$, rejects its outer product in ${\lambda }_{\to }$, recognizes the second product of exercise 60.2 in ${\lambda }_{2\omega }$, and rejects the $\mathsf{Vec}:\prod _{n:\mathsf{Nat}}\ast$ family declaration required by the third product when $r_P$ is absent. Its fifth outcome accepts an application whose types agree only after the bounded conversion stage.

Representation. Represent sorts, variables, products, abstractions, applications, and the finite context directly. Four Boolean fields select the lambda-cube triples. Each successful inference returns its synthesized type, the optional sort of that type, and the complete ordered Axis trace. The beta-normal entry point rejects redexes. Both entry points first verify that input binder identifiers are globally unique and disjoint from free identifiers. Globally fresh names make the printed traces easy to compare with chapter derivations, but require the preflight scan and restrict substitution. De Bruijn indices remove the freshness precondition; their cost is index shifting in substitution and beneath products and abstractions.

First complete version. Implement context lookup, alpha-aware comparison using paired binder environments, capture-free substitution under the checked freshness invariant, and structural inference. Product and lambda cases compute the required axis from their two premise sorts. The ${\lambda }_2$ identity returns the generated trace [(*,*,*); (Box,*,*)].

Remaining cases. Remove the polymorphic flag for ${\lambda }_{\to }$ and require the rejection to name $(◻,\ast ,\ast )$. Add the operator-kind annotation $\ast \to \ast$, then the higher-order polymorphic product from exercise 60.2 under the ${\lambda }_{2\omega }$ specification. Test the dependent family against a specification without $r_P$. The higher-order product case also compares independently named alpha-equivalent product types. Compare the complete ordered successful traces, not mere axis membership. Then add developOnce, which contracts every redex visible in a compared type without recursively developing redexes created by contraction. Check an application rejected by structural type equality but accepted after this single development stage. Development may duplicate a binder identifier across sibling subterms, but developed expressions are passed only to alpha-aware comparison, never to substitution; global freshness is an input invariant rather than an output invariant of developOnce.

A failing version. If enabled returns True for Polymorphic independently of the specification, the second oracle line changes to FAIL. If it confuses Operator and Dependent, the third or fourth line fails.

Acceptance test. Run the four appendix E commands. Require the exact five PASS lines, the summary All 5 Chapter 60 corpus cases passed., and audit result [].

Mathematical boundary. The run checks the finite beta-normal lambda-cube fragment plus one visible redex under its explicit fresh-name invariant. It does not implement general beta-conversion or prove weakening, substitution, subject reduction, normalization, or decidability for an arbitrary PTS. It illustrates the product-formation and classifier invariant used by theorem 60.27, not the theorem’s general decision procedure.