Chapter 13: The Program Monoid — Composition as a Theorem

In standard category theory, composition of morphisms is an axiom: one postulates that for morphisms f : A → B and g : B → C, the composite g ∘ f : A → C exists and is associative. In τ, composition is a theorem. We define programs as finite sequences of ρ-instructions, introduce normalization, and prove that composition — defined as concatenation followed by normalization — is associative. The proof passes through the NF-Confluence Lemma: any two reduction paths to normal form yield the same result. The resulting program monoid is the compositional substrate on which the category structure of Part XII will be built.