day dreams of Big O

license: public domain cc0 

Axiomatic Cost Algebra & Axiomatic SDK Design Document (Revised)

Semantic performance modeling for a total functional core, with principled extensions

---

1. Purpose and Positioning

Modern performance is chaotic:

• speculative execution
• dynamic JIT rewriting
• GC pauses
• branch predictor failures
• cache unpredictability
• thermal throttling
• NUMA effects
• network congestion

These make empirical testing unavoidable.

But empirical testing without a semantic foundation is blind.

This document defines a static, architecture‑agnostic cost algebra and an axiomatic SDK that together form:

Stage 1 of a multi‑stage performance model

A layer that captures semantic cost structure before any compiler, JIT, or hardware effects enter the picture.

This algebra is not meant to replace empirical testing.
It is meant to replace ignorance — to give us a principled, compositional understanding of program cost before runtime chaos takes over.

---

2. Design Philosophy

2.1 Semantic vs empirical performance

We distinguish:

• Semantic cost
  Determined by program structure, independent of hardware.

• Empirical cost
  Determined by runtime behavior, hardware, and environment.

The algebra models only the first.
Future work will bridge to the second.

2.2 Space vs time resources

Resources fall into two categories:

Resource Type	Examples	Peak Meaningful?	Accumulated Meaningful?
Space-like	memory, VRAM, file handles, thread count	✔ yes	✔ yes
Time-like	CPU, network, disk, GPU compute	✘ no (static)	✔ yes

This distinction is fundamental:

• Space resources have meaningful peak usage because they represent capacity.
• Time resources have meaningful accumulated usage because they represent work.

Peak CPU usage is not a semantic property of a program.
Peak memory usage is.

2.3 Total core + partial extension

We define:

• a total functional core with guaranteed termination
• a partial extension that introduces non‑termination via domain lifting

This keeps the algebra clean while allowing real-world expressiveness.

---

3. Cost Algebra

3.1 Cost vector

Each fragment carries a cost vector:

Cost = {
  cpu_accum      :: BigO
  mem_peak       :: BigO
  mem_alloc      :: BigO
  net_accum      :: BigO
}

Where:

• cpu_accum = accumulated CPU work
• mem_peak = peak live memory
• mem_alloc = total allocated bytes
• net_accum = total network bytes

3.2 Big‑O domain

BigO = OConst | OLogN | ON | ONLogN | ON2 | OCustom String

3.3 Composition rules

Sequential composition

cpu_accum(F ; G)  = cpu(F) + cpu(G)
mem_peak(F ; G)   = max(mem_peak(F), mem_peak(G))
mem_alloc(F ; G)  = mem_alloc(F) + mem_alloc(G)
net_accum(F ; G)  = net(F) + net(G)

Branching

cpu_accum(if) = max(cpu(F), cpu(G))
mem_peak(if)  = max(mem_peak(F), mem_peak(G))
...

Loops / structural recursion

cpu_accum(loop n F) = n * cpu(F)
mem_alloc(loop n F) = n * mem_alloc(F)
mem_peak(loop n F)  = mem_peak(F)

3.4 Total vs partial cost

TotalCost a = Finite Cost a
PartialCost a = TotalCost a | MayDiverge Cost | DivergesOnly

---

4. Axiomatic SDK (Clone of Haskell’s base)

We build a clean, total, pure SDK that mirrors the conceptual structure of Haskell’s base but is:

• smaller
• fully cost‑annotated
• free of GHC magic
• predictable
• analyzable

4.1 Structure

Axiomatic.Prelude
Axiomatic.Core.Bool
Axiomatic.Core.Int
Axiomatic.Core.Maybe
Axiomatic.Core.Either
Axiomatic.Core.List
Axiomatic.Data.Foldable
Axiomatic.Data.Traversable
Axiomatic.Control.Applicative
Axiomatic.Control.Monad
Axiomatic.Cost.Algebra
Axiomatic.Cost.Inference

4.2 Example: List map

map f xs

cpu_accum = n * cpu(f) + O(n)
mem_alloc = O(n)
mem_peak  = O(n)
net_accum = O(1)

4.3 Example: Monad bind for lists

xs >>= f

cpu_accum = Σ cpu(f(x)) + cost of concatenation
mem_alloc = O(n^2) in worst case
mem_peak  = O(n)

---

5. Why This Algebra Matters (Even If Performance Is Chaotic)

5.1 It captures semantic structure

Even if runtime constants vary wildly, the shape of cost is stable.

5.2 It enables static comparison of implementations

You can tell:

• which version allocates fewer objects
• which version fuses loops
• which version avoids quadratic behavior

5.3 It detects semantic performance bugs

• accidental O(n²)
• exponential recursion
• unnecessary traversals
• hidden allocations

5.4 It forms the foundation for future tooling

• static analyzers
• cost certificates
• optimization passes
• JIT hints
• performance regression detection

5.5 It is the only stable layer in a chaotic world

Hardware changes.
JITs change.
Caches change.
Predictors change.

Semantic structure does not.

---

6. Future Work: Bridging Semantic Cost to Real Performance

This algebra is Stage 1 of a multi-stage model.

6.1 Compiler/JIT performance profiles

Define a spec for each compiler/JIT:

• inlining behavior
• fusion rules
• unboxing
• specialization
• allocation strategies

This maps algebraic primitives to compiler-level costs.

6.2 Hardware class performance envelopes

Define hardware profiles:

• CPU throughput
• memory bandwidth
• cache hierarchy
• network latency

This maps compiler-level costs to real-world latency/throughput.

6.3 Rate/QoS modeling

Layer a rate model on top:

• requests per second
• concurrency
• tail latency
• saturation points

This maps per-call semantic cost to system-level behavior.

6.4 Empirical validation

Long-term testing remains essential:

• varied workloads
• chaos testing
• real hardware
• real JIT behavior

But now it is grounded in a semantic model.

---

7. Summary

This algebra is not a silver bullet.
It does not predict exact runtime performance.
It does not eliminate empirical testing.

But it does:

• provide a principled semantic foundation
• allow static reasoning about cost
• detect structural performance bugs
• enable comparison of implementations
• support future compiler/hardware modeling
• give meaning to performance before runtime chaos enters

It is the missing semantic layer in modern performance engineering.

---