Registry · Definition I.D14 established formalized

I.D14 — Program Monoid

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

Book I Part 3 Ch. 13

Dependency Graph

Depends on (4)

I.D07 I.D09 I.D02 I.T01

Depended on by (10)

I.D22 I.D77 I.D79 I.D84 I.L02 I.R35 I.T03 I.T37 I.T46 I.X02

Lean Formalization

Module: TauLib.BookI.Denotation.ProgramMonoid

Symbol: Tau.Denotation.ProgramMonoid