ch:logical-frameworks: ch:logical-frameworks
Problem and result. Decode canonical inhabitants of the intrinsic STLC LF signature and expose the exact canonical-head failures. The run decodes identity and application, rejects an underapplied
Representation. Use a bounded canonical grammar with de Bruijn variables and fully applied LamHead and AppHead constructors. Pass an explicit context and a fixed signature flag recording whether inspect is declared. Before decoding, validate every variable annotation, lambda body type, function type, and argument type. Keep UnderappliedLam as a raw arity failure. A general implementation would replace the fixed signature flag by a table of constant telescope declarations.
First complete version. Decode a bound variable and a fully applied lambda. The represented identity is LamHead Atom Atom (Bound 0 Atom) and decodes to an object lambda of type Atom -> Atom. Render the decoded tree and computed type; do not print a fixed success description.
Remaining cases. Decode application recursively, propagating the first failed subobject. Reject the short lambda before body decoding and an internally inconsistent lambda during canonical checking. Under the extended signature, accept InspectHead as canonical but report it as exotic to the STLC decoder. That last test implements the signature-relative boundary of proposition 61.28.
A failing version. Mapping every unknown result head to its argument makes the fourth line FAIL; treating an underapplied head as an object lambda makes the third line FAIL. Both mutations fabricate an inverse case absent from the object syntax.
Acceptance test. Require the four named PASS lines, the exact recorded adequacy summary, silent checking, and audit [] under the appendix E commands.
Mathematical boundary. The finite run illustrates canonical-head inversion. It does not prove LF normalization, eta-long uniqueness, or either adequacy bijection.