Program Monoid

Programs = finite sequences of rho-instructions. Composition = sequential concatenation + normalization. Identity = empty program. The compositional substrate for future categories.

Program Monoid

Summary

Programs = finite sequences of rho-instructions. Composition = sequential concatenation + normalization. Identity = empty program. The compositional substrate for future categories.

Statement

%
\label{def:program-monoid}
The \textbf{program monoid} $\mathcal{P}$ is the set
of NF-equivalence classes of programs,
equipped with:
\begin{itemize}
    \item \textbf{Composition}: $[Q] \circ [P] := [\text{NF}(Q \cdot P)]$,
          where $Q \cdot P$ denotes concatenation
          and $\text{NF}$ denotes normalization.
    \item \textbf{Identity}: $[\varepsilon]$, the empty program.
\end{itemize}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 28
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch13-program-monoid.tex lines 133-145

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.ProgramMonoid
• Name: Tau.Denotation.ProgramMonoid

Dependencies

• Canonical: I.D07, I.D09, I.D02, I.T01

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.