Throughout this series, I've described cognitive architectures, language extensions, belief systems, evolution engines, and collective intelligence. But how do we know any of it actually works? How do we reason precisely about what these systems do?
The answer is formal semantics. In this final post, I'm presenting the operational semantics for the key constructs in the Mnemonic Hive specification—mathematical definitions that specify exactly how agents execute, beliefs are revised, and memories are managed.
This might seem like academic indulgence. It's not. Without formal semantics, we're just hand-waving. With them, we can prove properties, verify implementations, and build tools that understand our language at a deep level.
Why Operational Semantics?
Operational semantics tells us how programs execute, step by step. For a given expression and state, it tells us exactly what the next state will be. This is different from denotational semantics (what does a program mean mathematically?) or axiomatic semantics (what properties can we prove about a program?).
I've chosen small-step structural operational semantics (SOS) because:
- It closely matches implementation—each rule becomes code
- It handles concurrency naturally through interleaving
- It makes reasoning about intermediate states possible
- It's the industry standard for defining language behavior
The Semantic Domains
First, we need to define what values our system manipulates:
v ∈ Value ::= unit (* Unit value *)
| n (* Integer *)
| r (* Float *)
| b (* Boolean *)
| s (* String *)
| [v₁, ..., vₙ] (* List *)
| {k₁: v₁, ..., kₙ: vₙ} (* Map *)
| belief(content, conf, truth) (* Belief value *)
| memory(id, content, tier, ...) (* Memory entry *)
| goal(id, desc, status, ...) (* Goal value *)
| aid (* Actor ID *)
| mid (* Memory ID *)And the stores that hold system state:
σ ∈ Store = Location → Value (* Heap *)
μ ∈ MemoryStore = MemoryId → MemoryEntry (* Memory tiers *)
β ∈ BeliefStore = Topic → Set<Belief> (* Belief index *)
ι ∈ IntentionStore = GoalId → Intention (* Active intentions *)Memory Operations
Let's start with the semantics of memory operations. The remember expression stores a new memory entry:
mid = fresh_id()
embedding = embed(content)
entry = MemoryEntry {
id: mid,
content: content,
embedding: embedding,
tier: tier,
truth_category: truth,
confidence: conf,
created_at: now(),
...
}
μ' = μ[mid ↦ entry]
───────────────────────────────────────────────────────── (E-Remember)
⟨remember { content: s, tier: t, ... }, σ, μ⟩ → ⟨Ok(mid), σ, μ'⟩Reading this: given a remember expression with content s and tier t, in state (σ, μ), we generate a fresh memory ID, compute the embedding, create the entry, and produce a new memory store μ' with the entry added. The result is the memory ID wrapped in Ok.
The shorthand form infers the tier from truth category and confidence:
tier = infer_tier(truth, conf)
─────────────────────────────────────────────────────────── (E-Remember-Infer)
⟨remember s as mtype with confidence c, σ, μ⟩
→ ⟨remember { content: s, confidence: c, tier: tier }, σ, μ⟩
where infer_tier(Absolute, c) = if c ≥ 0.9 then Persistent else LongTerm
infer_tier(Contextual, c) = if c ≥ 0.6 then LongTerm else ShortTerm
infer_tier(Opinion, _) = LongTerm
infer_tier(Inferred, c) = if c ≥ 0.6 then LongTerm else ShortTermThis captures the policy I described in earlier posts: absolute truths with high confidence go to persistent storage; lower confidence facts start in short-term and must earn their way up.
Belief Revision Semantics
The AGM belief revision operations from Part 3 get precise definitions:
Expansion (adding consistent belief)
¬∃b' ∈ β. contradicts(belief, b')
β' = β ∪ {belief}
─────────────────────────────────────────────────────────── (E-Expand)
⟨beliefs.add(belief), σ, μ, β⟩ → ⟨Ok(belief.id), σ, μ, β'⟩If no existing belief contradicts the new one, simply add it.
Revision (adding possibly contradicting belief)
contradicted = {b | b ∈ β, contradicts(evidence, b)}
to_remove = {b | b ∈ contradicted,
b.confidence.overall() < evidence.confidence}
to_update = contradicted \ to_remove
β' = (β \ to_remove)
β'' = update_confidence(β', to_update, evidence)
─────────────────────────────────────────────────────────── (E-Revise)
⟨beliefs.revise(evidence), σ, μ, β⟩ → ⟨updated_list, σ, μ, β''⟩Find all contradicted beliefs. Remove those with lower confidence than the new evidence. Update the confidence of the rest through Bayesian updating. This precisely captures the minimal change principle from AGM theory.
The BDI Agent Cycle
The most complex semantics are for the BDI agent execution cycle. An agent configuration includes beliefs, desires, intentions, sensors, and effectors:
AgentConfig = ⟨
beliefs: BeliefStore,
desires: GoalQueue,
intentions: IntentionStack,
sensors: List<Sensor>,
effectors: Map<String, Effector>,
tick_rate: Duration
⟩The complete cycle proceeds through five phases:
Perception Phase
observations = []
for sensor in Ag.sensors:
obs = sensor.sense()
observations = observations ++ obs
messages = Ag.mailbox
Ag' = Ag with { mailbox: [] }
─────────────────────────────────────────────────────────── (E-Perceive)
⟨Ag⟩ →_perceive ⟨Ag', observations ++ messages⟩Gather observations from all sensors and collect pending messages.
Belief Revision Phase
for obs in observations:
match obs:
Fact(content, source, conf) →
β' = β.add(believe content with conf from source)
Event(desc, time) →
μ' = μ.remember(desc as Event)
Contradiction(bid, evidence) →
β' = β.revise(evidence)
─────────────────────────────────────────────────────────── (E-Revise-Phase)
⟨Ag, observations⟩ →_revise ⟨Ag'⟩Update beliefs based on observations. Facts become beliefs, events become memories, contradictions trigger revision.
Deliberation Phase
options = []
for desire in Ag.desires.active():
context = Ag.beliefs.query(desire.motivation)
if applicable(desire, context):
goal = desire_to_goal(desire, context)
options = options ++ [goal]
scored = [(g, evaluate(g, Ag.beliefs)) | g ← options]
sorted = sort_by_score_desc(scored)
selected = take(sorted, available_slots)
─────────────────────────────────────────────────────────── (E-Deliberate)
⟨Ag⟩ →_deliberate ⟨Ag, selected⟩Consider active desires, score them against current beliefs, select the best ones.
Planning Phase
for goal in selected:
if ¬Ag.intentions.has_plan_for(goal):
plan = Ag.planner.generate(goal, Ag.beliefs)
if plan.confidence > threshold:
intention = Intention::new(goal, plan)
Ag.intentions.commit(intention)
─────────────────────────────────────────────────────────── (E-Plan)
⟨Ag, selected⟩ →_plan ⟨Ag'⟩Generate plans for goals that don't have them, commit as intentions if confidence is sufficient.
Execution Phase
action = Ag.intentions.select_action()
match action:
None → skip
Some(act) →
result = execute(act, Ag.effectors)
Ag.intentions.record_result(act, result)
if result.success:
Ag.intentions.advance_step()
else:
Ag.intentions.handle_failure(result)
─────────────────────────────────────────────────────────── (E-Execute)
⟨Ag⟩ →_execute ⟨Ag', result⟩Execute the next action, record results, advance on success or handle failure.
The Complete Cycle
⟨Ag₀⟩ →_perceive ⟨Ag₁, observations⟩
⟨Ag₁, observations⟩ →_revise ⟨Ag₂⟩
⟨Ag₂⟩ →_deliberate ⟨Ag₃, selected⟩
⟨Ag₃, selected⟩ →_plan ⟨Ag₄⟩
⟨Ag₄⟩ →_execute ⟨Ag₅, result⟩
wait(tick_rate)
─────────────────────────────────────────────────────────── (E-BDI-Cycle)
⟨Ag₀⟩ →_bdi ⟨Ag₅⟩This is the heartbeat of a cognitive agent: perceive → revise → deliberate → plan → execute, forever.
Hive Coordination
When multiple agents coordinate, we need semantics for hive-level operations:
Goal Marketplace
capable = [a | a ∈ hive.agents, a.can_handle(goal)]
bids = parallel([a.bid(goal) | a ← capable], timeout)
winner = select_best(bids, criteria)
send(winner, AssignGoal(goal))
─────────────────────────────────────────────────────────── (E-Goal-Market)
⟨hive.broadcast_goal(goal)⟩ → ⟨winner, assigned_goal_id⟩Goals are broadcast to capable agents, who bid, and the best bid wins.
Stigmergic Traces
trace = StigmergicTrace {
agent_id: agent.id,
action: action,
outcome: outcome,
strength: if outcome.success then 0.5 + 0.5 * quality else 0.2,
location: action_space.embedding,
timestamp: now()
}
μ' = μ.remember(trace.to_string(), type: Stigmergy)
─────────────────────────────────────────────────────────── (E-Leave-Trace)
⟨stigmergy.leave_trace(agent, action, outcome), μ⟩ → ⟨unit, μ'⟩Agents leave traces in memory that other agents can sense and follow.
Memory Promotion and Demotion
Memories move between tiers based on confidence and usage:
promotable = {m | m ∈ μ.short_term,
m.confidence.overall() ≥ 0.6 ∧
m.confidence.corroboration_count ≥ 2}
for m in promotable:
μ.short_term = μ.short_term \ {m}
m' = m with { tier: LongTerm }
μ.long_term = μ.long_term ∪ {m'}
─────────────────────────────────────────────────────────── (E-Promote-ST-LT)
⟨promote_short_to_long(), μ⟩ → ⟨count(promotable), μ'⟩Short-term memories with sufficient confidence and corroboration get promoted to long-term. The criteria are explicit: at least 0.6 confidence and at least 2 corroborating sources.
Concurrency Model
Actors execute in isolation:
(* Actors do not share mutable state *)
∀ A₁, A₂ ∈ Σ. A₁ ≠ A₂ ⟹ A₁.state ∩ A₂.state = ∅
(* Message passing is the only communication *)
∀ A₁, A₂ ∈ Σ. communicate(A₁, A₂) ⟹ ∃ msg. A₁ →_send(msg) → A₂This guarantees no data races: actors can only communicate through messages, and their states are fully disjoint.
Why This Matters
These formal definitions aren't just documentation. They enable:
Verification. We can prove properties about agent behavior. For example, we can prove that belief revision maintains consistency, or that the BDI cycle eventually terminates.
Implementation guidance. Each rule maps directly to code. The implementer knows exactly what behavior is required.
Debugging. When something goes wrong, we can trace through the rules to understand exactly how the system got into that state.
Tool support. Language servers, debuggers, and optimizers can be built that understand these semantics precisely.
The Complete Picture
Across this series, I've presented:
- Part 1: The Mnemonic Hive vision—cognitive architecture for AI with persistent memory and genuine beliefs
- Part 2: Language extensions—agents, beliefs, and memories as first-class citizens in Simplex
- Part 3: Epistemic architecture—how agents know what they know
- Part 4: Continuous learning—how hives improve over time
- Part 5: Collective intelligence—how agent swarms exhibit emergent behavior
- Part 6 (this post): Formal semantics—the mathematical foundation that makes it all precise
Together, this constitutes a complete specification for cognitive AI systems. Not hand-waving about "AI agents" and "memory systems," but precise definitions of what these systems are and how they behave.
The implementation work continues. But the specification is complete. When we build the Simplex runtime with Mnemonic Hive support, we'll know exactly what we're building.
This concludes the Simplex Evolution Series. For more on Simplex, see simplex.senuamedia.com. For the Memory system, see memory.senuamedia.com.