appendix sectionsignatures

Scoped operations and explicit substitution

Signature.: Chapter 23 fixes two endofunctor signatures $(Σ, Γ)$ . The exact source syntax is $T = μ G$ for $(G H) A = A + Σ (H A) + Γ (H (H A))$ , hence $Var : A \to T A$ , $Op : Σ (T A) \to T A$ , and $Scope : Γ (T (T A)) \to T A$ . For polynomial signatures, an ordinary symbol has parameter/response data $(P_{o}, R_{o})$ and a scoped symbol has ordinary-parameter/scoped-position data $(P_{s}, Q_{s})$ .
Elementwise scoped node.: A polynomial scoped node is represented by ${Scope}_{s} (p; X; m; k)$ , where $p : P_{s}$ , $m : Q_{s} \to T X$ , and $k : X \to T A$ , modulo the reindexing equation of definition 23.4. The canonical-representative bijection with the nested $Γ (T (T A))$ constructor is lemma 23.5. This elementary identification is part of the syntax development in chapter 23; it is not the later categorical monad-isomorphism theorem of the source paper.
Substitution and monad.: For the polynomial presentation (23.4), the well-founded elementwise induction principle is corollary 23.7; it is derived under the explicit hypothesis that the displayed nested signature has a monic convergent initial chain. No general initial-algebra existence theorem is claimed. Explicit substitution is definition 23.9. It recurses through ordinary response branches but, at a scoped node, preserves the ordinary parameters and owned computations and composes only the explicit outside continuation. Well-definedness with respect to reindexing is lemma 23.10. The substitution identity and composition equations are theorem 23.11; return and bind therefore satisfy the monad laws by corollary 23.12.
Comparisons.: The idiom and Kleisli-arrow constructions in section 23.6 are explicit one-way translations from the scoped monad. Their required equations are proved locally in proposition 23.15, proposition 23.16; no converse reconstruction is claimed. For higher-order operations, the comparison starts after the fork computations have been translated sortwise to terms ${\hat{ψ}}_{q} : T B_{q}$ . A coproduct carrier then homogenizes fork-result sets, so heterogeneity alone is not an obstruction. The exact remaining continuation criterion is proposition 23.18: natural families $(R \to Y) \to (X \to Y)$ are precisely precomposition by adapters $X \to R$ . The nonempty-carrier/empty-response instance is the local counterexample. This is a signature comparison only, not a theorem about the elaboration calculus of chapter 24.
Metatheorem boundary.: This chapter has no operational handler language. It therefore states no preservation, progress, no-unhandled-operation, handler-safety, or operational adequacy theorem. The source paper’s scoped-algebra semantics and categorical representation/isomorphism theorem are not imported. The modular higher-order elaboration of chapter 24 is a separate calculus, and none of its theorems is transferred to $T$ .
Executable evidence.: The Kappa companion under artifacts/ch29-scoped-operations/ defunctionalizes a finite fragment to make ordinary parameters, scoped bodies, and continuations independently observable. Its accepted corpus and three mutation failures test the implementation. They do not prove reindexing well-definedness, substitution composition, the monad laws, or any handler theorem.