TauLib · API Book I

TauLib.BookI.Denotation.ProgramMonoid

TauLib.Denotation.ProgramMonoid

The program monoid: instruction sequences, normal forms, and composition.

Registry Cross-References

  • [I.D14] Instruction Set — Instruction, Program

  • [I.L02] Normal Form Confluence — normalize_compose

  • [I.T03] Program Monoid — compose_assoc, compose_id

Mathematical Content

Programs are finite sequences of two instruction types:

  • rho_inst: apply ρ (increments depth for non-omega objects)

  • sigma_inst g h: swap seeds g and h

Every program’s effect on a TauObj is completely determined by:

  • The net seed permutation (composition of all sigma swaps)

  • The total rho count (number of rho_inst instructions)

This yields a normal form, and NF-equivalence is decidable. The program monoid is the quotient by NF-equivalence.

Tau.Denotation.Instruction

source inductive Tau.Denotation.Instruction :Type

[I.D14] The two instruction types.

  • rho_inst : Instruction
  • sigma_inst : Kernel.Generator → Kernel.Generator → Instruction Instances For

Tau.Denotation.instDecidableEqInstruction

source instance Tau.Denotation.instDecidableEqInstruction :DecidableEq Instruction

Equations

  • Tau.Denotation.instDecidableEqInstruction = Tau.Denotation.instDecidableEqInstruction.decEq

Tau.Denotation.instDecidableEqInstruction.decEq

source def Tau.Denotation.instDecidableEqInstruction.decEq (x✝ x✝¹ : Instruction) :Decidable (x✝ = x✝¹)

Equations

  • One or more equations did not get rendered due to their size.
  • Tau.Denotation.instDecidableEqInstruction.decEq Tau.Denotation.Instruction.rho_inst Tau.Denotation.Instruction.rho_inst = isTrue ⋯
  • Tau.Denotation.instDecidableEqInstruction.decEq Tau.Denotation.Instruction.rho_inst (Tau.Denotation.Instruction.sigma_inst a a_1) = isFalse ⋯
  • Tau.Denotation.instDecidableEqInstruction.decEq (Tau.Denotation.Instruction.sigma_inst a a_1) Tau.Denotation.Instruction.rho_inst = isFalse ⋯ Instances For

Tau.Denotation.instReprInstruction.repr

source def Tau.Denotation.instReprInstruction.repr :Instruction → Nat → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.Denotation.instReprInstruction

source instance Tau.Denotation.instReprInstruction :Repr Instruction

Equations

  • Tau.Denotation.instReprInstruction = { reprPrec := Tau.Denotation.instReprInstruction.repr }

Tau.Denotation.Program

source@[reducible, inline]

abbrev Tau.Denotation.Program :Type

A program is a finite sequence of instructions. Equations

  • Tau.Denotation.Program = List Tau.Denotation.Instruction Instances For

Tau.Denotation.execInstruction

source **def Tau.Denotation.execInstruction (i : Instruction)

(x : Kernel.TauObj) :Kernel.TauObj**

Execute a single instruction on a TauObj. Equations

  • Tau.Denotation.execInstruction Tau.Denotation.Instruction.rho_inst x = Tau.Kernel.rho x
  • Tau.Denotation.execInstruction (Tau.Denotation.Instruction.sigma_inst a a_1) x = Tau.Denotation.sigma a a_1 x Instances For

Tau.Denotation.execProgram

source **def Tau.Denotation.execProgram (p : Program)

(x : Kernel.TauObj) :Kernel.TauObj**

Execute a program (left-to-right: first instruction applied first). Equations

  • Tau.Denotation.execProgram p x = List.foldl (fun (acc : Tau.Kernel.TauObj) (i : Tau.Denotation.Instruction) => Tau.Denotation.execInstruction i acc) x p Instances For

Tau.Denotation.NormalForm

source structure Tau.Denotation.NormalForm :Type

A program normal form: net seed permutation function + rho count.

  • seedMap : Kernel.Generator → Kernel.Generator
  • rhoCount : Nat Instances For

Tau.Denotation.countRho

source def Tau.Denotation.countRho :Program → Nat

Count the number of rho instructions in a program. Equations

  • Tau.Denotation.countRho [] = 0
  • Tau.Denotation.countRho (Tau.Denotation.Instruction.rho_inst :: rest) = 1 + Tau.Denotation.countRho rest
  • Tau.Denotation.countRho (Tau.Denotation.Instruction.sigma_inst a a_1 :: rest) = Tau.Denotation.countRho rest Instances For

Tau.Denotation.NormalForm.id

source def Tau.Denotation.NormalForm.id :NormalForm

The identity normal form. Equations

  • Tau.Denotation.NormalForm.id = { seedMap := fun (g : Tau.Kernel.Generator) => g, rhoCount := 0 } Instances For

Tau.Denotation.NormalForm.compose

source def Tau.Denotation.NormalForm.compose (nf1 nf2 : NormalForm) :NormalForm

Compose two normal forms. Equations

  • nf1.compose nf2 = { seedMap := fun (g : Tau.Kernel.Generator) => nf2.seedMap (nf1.seedMap g), rhoCount := nf1.rhoCount + nf2.rhoCount } Instances For

Tau.Denotation.execNF

source **def Tau.Denotation.execNF (nf : NormalForm)

(x : Kernel.TauObj) :Kernel.TauObj**

Execute a normal form on a TauObj (simplified: just apply rho count times). Equations

  • Tau.Denotation.execNF nf x = Tau.Orbit.iter_rho nf.rhoCount { seed := nf.seedMap x.seed, depth := x.depth } Instances For

Tau.Denotation.Program.compose

source def Tau.Denotation.Program.compose (p q : Program) :Program

Program composition is concatenation. Equations

  • p.compose q = p ++ q Instances For

Tau.Denotation.compose_assoc

source theorem Tau.Denotation.compose_assoc (p q r : Program) :(p.compose q).compose r = p.compose (q.compose r)

[I.T03] Composition is associative.

Tau.Denotation.compose_id_left

source theorem Tau.Denotation.compose_id_left (p : Program) :Program.compose [] p = p

The empty program is a left identity.

Tau.Denotation.compose_id_right

source theorem Tau.Denotation.compose_id_right (p : Program) :p.compose [] = p

The empty program is a right identity.

Tau.Denotation.exec_compose

source **theorem Tau.Denotation.exec_compose (p q : Program)

(x : Kernel.TauObj) :execProgram (p.compose q) x = execProgram q (execProgram p x)**

Executing a concatenation is the same as executing sequentially.

Tau.Denotation.exec_nil

source theorem Tau.Denotation.exec_nil (x : Kernel.TauObj) :execProgram [] x = x

The empty program is the identity.

Tau.Denotation.exec_rho

source theorem Tau.Denotation.exec_rho (x : Kernel.TauObj) :execProgram [Instruction.rho_inst] x = Kernel.rho x

A single rho instruction applies rho.

Tau.Denotation.exec_sigma

source **theorem Tau.Denotation.exec_sigma (s t : Kernel.Generator)

(x : Kernel.TauObj) :execProgram [Instruction.sigma_inst s t] x = sigma s t x**

A single sigma instruction applies sigma.

Tau.Denotation.rho_count_compose

source theorem Tau.Denotation.rho_count_compose (p q : Program) :countRho (p.compose q) = countRho p + countRho q

[I.L02] Normal form confluence: the rho count of a composed program is the sum of the individual rho counts.

Tau.Denotation.rho_count_nil

source theorem Tau.Denotation.rho_count_nil :countRho [] = 0

The rho count of the empty program is 0.