Finite-graph Boolean semantic subtyping

The calculus ${\lambda }_{\mathsf{FG}}$ has finite monomorphic type trees built from $0$, basic tags, products, arrows, union, and complement; top and intersection are derived Boolean operations. Terms are constants, variables, pairs and projections, explicitly interfaced abstractions, application, and binder typecase. A written interface is nonempty and is well shaped when it has one arrow, or when no domain in a multi-arrow interface contains an arrow atom other than $\mathsf{Fun}=0\to 1$. There are no type variables, records, recursion, effects, nondeterminism, or sum constructors.

Type equivalence is equality of interpretations in the hereditary finite-graph domain of definition 9.5, definition 9.6; subtyping is semantic inclusion. The $\mathrm{\Omega }$ output is outside every type and records a failed call. The chapter does not assign a graph element to each program value and proves no denotational adequacy theorem for terms. The calculus meets the semantic order through typing side conditions; preservation, progress, and safety are proved separately by exact value types and structural tests. The marker $\mathrm{\Omega }$ is not a run-time program term. There is no separate term equality or type-conversion judgment.

Weak left-to-right call-by-value reduction has exactly beta, pair projection, and the two structural typecase roots under the contexts of definition 9.18. Abstraction bodies and unselected branches do not reduce.

Boolean subtyping reduces to emptiness in corollary 9.8. Finite simulations decide emptiness and semantic subtyping by theorem 9.16. Structural rules, exact value inversion, preservation, progress, and safety are lemma 9.27, lemma 9.29, theorem 9.32, theorem 9.33. The supplied-interface synthesizer is sound, complete, terminating, and least up to semantic equivalence by theorem 9.35. No normalization or unannotated principal-inference theorem is claimed.

The pinned Kappa corpus executes the finite subtype procedure and eight grouped conformance cases under the exact limitations recorded in appendix E. Its directory is artifacts/ch20-semantic-subtyping/. It is implementation evidence, not a mechanized proof and not native-backend parity evidence.