temporal-coalgebra

plurigrid's avatarfrom plurigrid

Coalgebraic observation of derivation streams with final coalgebra bisimulation

⭐1stars🔀2forks📁View on GitHub🕐Updated Jan 9, 2026

When & Why to Use This Skill

The Temporal Coalgebra skill is a sophisticated formal verification tool designed for behavioral analysis and system equivalence testing. By leveraging mathematical frameworks like final coalgebra and bisimulation, it allows users to observe derivation streams and determine if two systems are observationally indistinguishable. This approach is particularly effective for verifying infinite structures, lazy-evaluated processes, and complex game semantics, ensuring that systems are correct by construction through rigorous behavioral mapping.

Use Cases

  • Protocol Verification: Comparing two different software implementations of a communication protocol to ensure they exhibit identical external behavior (bisimulation).
  • Infinite Stream Analysis: Monitoring and verifying the consistency of infinite data streams or lazy-evaluated sequences where traditional finite state testing is insufficient.
  • Game Theory & Security Modeling: Utilizing bisimulation checkers to verify attacker-defender strategies and ensure security properties are conserved across system states.
  • Automated Behavioral QA: Detecting subtle discrepancies between a system's theoretical specification and its actual execution traces using observation functors.
nametemporal-coalgebra
descriptionCoalgebraic observation of derivation streams with final coalgebra bisimulation
version1.0.0

Temporal Coalgebra Skill: Observation Duality

Status: ✅ Production Ready Trit: -1 (MINUS - validator/observer) Color: #2626D8 (Blue) Principle: Observe behaviors → Verify equivalence Frame: Final coalgebra with stream coalgebra traces


Overview

Temporal Coalgebra is the dual of algebra: where algebra constructs, coalgebra observes. Implements:

  1. Observation functor: O: Derivation → Observation
  2. Final coalgebra: νF for maximal bisimulation
  3. Stream coalgebra: Infinite traces with head/tail
  4. three-match integration: Game verification via bisimulation

Correct by construction: Two systems are equivalent iff they are bisimilar (observationally indistinguishable).

Core Formula

Coalgebra: (X, γ: X → F(X))   # State → Observable structure
Final:     νF = lim F^n(1)     # Greatest fixpoint

Bisimulation R ⊆ X × Y:
  (x, y) ∈ R ⟹ F(R)(γ_X(x), γ_Y(y))

For derivation observation:

# Observe derivation stream
observe(derivation) = { head: current_step, tail: rest_of_derivation }

# Two derivations are equivalent iff:
bisimilar?(d1, d2) == (observe(d1).head == observe(d2).head &&
                       bisimilar?(observe(d1).tail, observe(d2).tail))

Why Coalgebra for Verification?

  1. Behavioral equivalence: Same observations = same system
  2. Infinite structures: Streams, trees, processes
  3. Game semantics: Attacker/defender games are coalgebraic
  4. Lazy evaluation: Observe only what's needed

Gadgets

1. ObservationFunctor

Transform derivations into observations:

functor = TemporalCoalgebra::ObservationFunctor.new(
  source: :derivation_chain,
  target: :observation_stream
)
observation = functor.apply(derivation)
observation.head      # => current observable state
observation.tail      # => remaining stream (lazy)
observation.finite?   # => false (potentially infinite)

2. FinalCoalgebra

Construct the final coalgebra for type F:

final = TemporalCoalgebra::FinalCoalgebra.new(
  functor: stream_functor,
  approximation_depth: 100
)
final.carrier           # => νF (greatest fixpoint)
final.universal?(coal)  # => check if coal maps uniquely
final.unfold(seed)      # => generate infinite structure

3. BisimulationChecker

Verify behavioral equivalence:

checker = TemporalCoalgebra::BisimulationChecker.new
checker.add_system(:system_a, coalgebra_a)
checker.add_system(:system_b, coalgebra_b)

result = checker.check_bisimilar!
result[:bisimilar]         # => true/false
result[:distinguishing_trace]  # => if false, witness
result[:depth_checked]     # => how deep we verified

4. StreamCoalgebra

Work with infinite streams:

stream = TemporalCoalgebra::StreamCoalgebra.new(seed: 0x42D)
stream.head              # => first element
stream.tail              # => rest of stream
stream.take(10)          # => first 10 elements
stream.drop(5).head      # => 6th element
stream.map { |x| x * 2 } # => transformed stream
stream.zip(other_stream) # => paired stream

5. ThreeMatchBisimulation

Integration with three-match for game verification:

game = TemporalCoalgebra::ThreeMatchBisimulation.new(
  attacker: player_a,
  defender: player_b,
  three_match_gadget: gadget
)
game.play_round!
game.defender_wins?      # => strategies are bisimilar
game.attacker_wins?      # => found distinguishing move
game.gf3_conserved?      # => trit sum = 0

Commands

# Observe derivation chain
just coalgebra-observe

# Check bisimulation
just coalgebra-bisim system_a system_b

# Generate stream from seed
just coalgebra-stream 0x42D 20

# Verify game equivalence
just coalgebra-game

API

require 'temporal_coalgebra'

# Create observation system
obs = TemporalCoalgebra::Observer.new(
  trit: -1,
  functor: :stream
)

# Observe derivation
stream = obs.observe(derivation_chain)

# Check equivalence
bisim = obs.bisimilar?(stream_a, stream_b)

# Integrate with three-match
game_result = obs.verify_game(three_match_gadget)

Integration with GF(3) Triads

Forms valid triads with ERGODIC (0) and PLUS (+1) skills:

temporal-coalgebra (-1) ⊗ coequalizers (0) ⊗ topos-adhesive-rewriting (+1) = 0 ✓
temporal-coalgebra (-1) ⊗ unworld (0) ⊗ gay-mcp (+1) = 0 ✓
temporal-coalgebra (-1) ⊗ glass-bead-game (0) ⊗ cider-clojure (+1) = 0 ✓
temporal-coalgebra (-1) ⊗ acsets (0) ⊗ rubato-composer (+1) = 0 ✓
  • coequalizers (0) - Uses coalgebraic bisimulation to establish behavioral equivalence before quotienting
  • bisimulation-game (-1) - Game-theoretic bisimulation testing
  • topos-adhesive-rewriting (+1) - Rewriting preserves observational equivalence

Mathematical Foundation

Coalgebra Definition

Coalgebra for F: (X, γ: X → F(X))
  - X is carrier (state space)
  - γ is structure map (observation)
  - F is endofunctor (observation type)

Stream Functor

F(X) = A × X    (head × tail)
νF ≅ A^ω       (infinite sequences)

Bisimulation

R is bisimulation ⟺
  ∀(x,y) ∈ R: (γ_X(x), γ_Y(y)) ∈ F(R)

Behavioral equivalence: x ∼ y ⟺ ∃R bisimulation. (x,y) ∈ R

Coinduction Principle

To prove P(ν F), show:
  P is F-consistent: P(x) ⟹ P(tail(x))
  P(seed) holds

Example Output

─── Temporal Coalgebra Observation ───
Source: Derivation chain (length ∞)
Functor: Stream (head × tail)

Observation:
  head: { seed: 0x42D, color: #2626D8, trit: -1 }
  tail: <lazy stream>

Bisimulation Check:
  System A: derivation_chain_1
  System B: derivation_chain_2
  
  Depth 0: heads match ✓
  Depth 1: tails match ✓
  Depth 2: tails match ✓
  ...
  Depth 100: tails match ✓

Result: BISIMILAR (observationally equivalent)
GF(3) Trit: -1 (MINUS/Observer)

─── Three-Match Integration ───
Game: Attacker vs Defender
Rounds: 12
Winner: Defender (strategies bisimilar)
GF(3) conserved: true

Skill Name: temporal-coalgebra Type: Observation / Bisimulation Verification Trit: -1 (MINUS) Color: #2626D8 (Blue) GF(3): Forms valid triads with ERGODIC + PLUS skills Dual: Algebra (construction) ↔ Coalgebra (observation)

Scientific Skill Interleaving

This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:

Time Series

  • aeon [−] via Ran_K
    • Temporal/coalgebraic time series

Bibliography References

  • linear-algebra: 112 citations in bib.duckdb

Cat# Integration

This skill maps to Cat# = Comod(P) as a bicomodule in the equipment structure:

Trit: -1 (MINUS)
Home: Span
Poly Op: ×
Kan Role: Adj
Color: #FF6B6B

GF(3) Naturality

The skill participates in triads satisfying:

(-1) + (0) + (+1) ≡ 0 (mod 3)

This ensures compositional coherence in the Cat# equipment structure.