appendix sectionsignatures

Encodings and binding theorem boundaries

LF encodings and adequacy

Framework signature.: The exact Edinburgh LF calculus has signatures, contexts, dependent families over LF objects, annotated object abstraction and application, and beta–eta conversion. It has no family-variable product, recursion, pattern matching, induction, user rewrite rule, or object destructor.
Locally reconstructed.: For the implicational and intrinsic STLC signatures, the chapter proves code inversion, substitution compositionality, encoding soundness, canonical decoding, inverse equations, and the precise signature-extension failure of surjectivity. The proof works only for represented contexts and conclusions generated by the declared object syntax.
Imported framework results.: Canonicalization, uniqueness up to alpha-equivalence, and decidable LF checking and equality are imported for that exact calculus. Adequacy is not inherited automatically from those framework results; it is proved separately for each displayed signature.
Representation comparison.: De Bruijn, locally nameless, PHOAS, and contextual representations discharge the same renaming/substitution obligation through different local invariants. No theorem about one representation is transferred to another merely because their STLC images coincide.

Signature.: The atom set is countably infinite; only finite permutations act. Every nominal element is finitely supported. Name abstraction is the quotient generated by fresh swapping, and nominal STLC contexts have distinct atom labels.
Locally reconstructed.: Fresh comparison, the fresh-representative lemma, typing equivariance, the abstraction-support formula, freshness induction, the recursion principle, substitution support, substitution typing, and the nominal/de Bruijn commuting square are proved for the displayed syntax.
Imported boundary.: Existence of least finite supports and the nominal abstraction construction come from Gabbay–Pitts for finite-permutation sets. These claims do not include dependent nominal types, name-case, a fresh-name effect, or conservativity of a proof assistant implementation.
Executable evidence.: The companion checks four atoms and a deterministic fresh-choice strategy. Its explicit exhaustion result is not the mathematical fresh-atom theorem and proves none of the preceding induction, recursion, preservation, or adequacy claims.

Simply typed.: The first calculus has ordinary variables, modal variables for open objects, contextual types, boxes, box elimination, closures, and explicit contextual substitutions. Strong normalization applies to the union of its displayed principal reductions and commuting conversions.
Dependent canonical.: The second calculus has normal and atomic LF syntax, contextual products, meta-abstraction and contextual application, closures, and normal/atomic simultaneous-substitution components. Its typing rules invoke hereditary substitution and do not reuse the simply typed reduction relation.
Theorems.: Raw hereditary substitutions terminate with a result or finite failure; formation, checking, synthesis, and equality are decidable. Preservation requires every printed existence, formation, and underapproximation premise. The chapter does not infer preservation merely from raw termination and does not transfer strong normalization from the simply typed calculus.
Beluga boundary.: The paired context-schema invariant and the lambda recursive-call failure are source-inspection and finite-model scope evidence. They are not proofs of LF adequacy, CMTT normalization, hereditary-substitution termination, or Beluga compiler correctness.