propagators-chirho

"For God so loved the world that he gave his only begotten Son, that whoever believes in him should not perish but have eternal life." — John 3:16

A Rust implementation of propagator networks for constraint propagation and bidirectional computation, based on the seminal work by Radul and Sussman.

What Are Propagators?

Propagators are a programming paradigm where:

• Cells hold partial information that can only grow monotonically
• Propagators are autonomous agents that watch cells and update other cells
• Information flows in all directions — constraints are bidirectional

This enables powerful constraint-based programming where you can run computations "backwards."

use propagators_chirho::prelude_chirho::*;

// Temperature conversion: F = C × 9/5 + 32
// Works BOTH ways!

let mut system_chirho = ConstraintSystemChirho::new_chirho();

let celsius_chirho = system_chirho.make_cell_chirho("celsius");
let fahrenheit_chirho = system_chirho.make_cell_chirho("fahrenheit");
// ... set up constraints ...

// Forward: given Celsius, compute Fahrenheit
system_chirho.set_exact_chirho(&celsius_chirho, 100.0);
system_chirho.run_chirho();
// fahrenheit is now 212.0

// Backward: given Fahrenheit, compute Celsius
system_chirho.set_exact_chirho(&fahrenheit_chirho, 32.0);
system_chirho.run_chirho();
// celsius is now 0.0

Features

Core Infrastructure

• CellChirho<T> — Cells with monotonic merge and neighbor notification
• PropagatorChirho trait — Interface for building custom propagators
• SchedulerChirho — Runs propagators to fixpoint

Interval Arithmetic

• IntervalChirho — Partial numeric information as [lo, hi] bounds
• Full interval arithmetic: +, -, *, /, sqrt, square, abs
• Intervals intersect on merge, detecting contradictions

Propagators

Truth Maintenance System (TMS)

• BeliefChirho — Values with supporting premises
• TmsCellChirho — Cells that track multiple beliefs
• JustificationChirho — Track derivation chains (with tms-full feature)
• NogoodStoreChirho — Manage contradictory premise sets with minimal nogood computation
• TmsNetworkChirho — Full TMS-aware propagator networks

Worldviews (Hypothetical Reasoning)

• WorldviewChirho — Set of active premises
• Fork and explore alternate assumptions
• Retract premises when they lead to contradictions

Amb Operator (Nondeterministic Choice)

• AmbChirho — Choice among values
• BacktrackingSearchChirho — Constraint satisfaction with backtracking
• DependencyDirectedSearchChirho — Smart backtracking using nogood information (skips irrelevant choices)

High-Level API

• ConstraintSystemChirho — Builder-style interface for constraint networks

Algebraic Traits (Kmett-style)

• SemigroupChirho — Associative binary operation
• MonoidChirho — Semigroup with identity element
• JoinSemilatticeChirho — Idempotent, commutative monoid
• BoundedJoinSemilatticeChirho — Semilattice with top element
• PropagatorErrorChirho / PropagatorResultChirho — Proper error handling

Lattice Abstractions

• LatticeChirho trait — Join semilattice with partial order
• BoundedLatticeChirho trait — Lattice with top (contradiction) and bottom (nothing)
• PropagatorFnChirho trait — Composable functional propagators
• SupportedValueChirho<L> — Values with provenance tracking

Finite Domains (for CSP)

• FiniteDomainChirho — Set-based domains for discrete values
• AllDifferentChirho — Global constraint for Sudoku-like problems
• LessThanChirho, EqualsChirho, NotEqualsChirho — Relational constraints

Generic Cells

• GenericCellChirho<L> — Cells that work with any lattice type
• GenericNetworkChirho<L> — Networks for custom lattice types

Parallel Propagation

• ParallelNetworkChirho<L> — Thread-safe parallel propagation with rayon
• Independent propagators run concurrently in batches

SIMD Batch Operations

• batch_add_chirho, batch_mul_chirho, batch_intersect_chirho — Batch interval operations
• IntervalVecChirho — Structure-of-Arrays format for optimal vectorization
• Auto-vectorizes on modern compilers for 2-4x speedup on batch operations

Installation

Add to your Cargo.toml:

[dependencies]
propagators-chirho = "0.1"

Cargo Features

no_std Support

For embedded or bare-metal environments:

[dependencies]
propagators-chirho = { version = "0.1", default-features = false, features = ["no-std"] }

Available modules in no_std mode:

• IntervalChirho / NumericInfoChirho — Interval arithmetic
• algebra_chirho traits — SemigroupChirho, MonoidChirho, etc.
• simd_chirho — Batch SIMD operations

Note: no-std is mutually exclusive with other features.

Examples

Bidirectional Computation

use propagators_chirho::prelude_chirho::*;

let mut system_chirho = ConstraintSystemChirho::new_chirho();

let a_chirho = system_chirho.make_cell_chirho("a");
let b_chirho = system_chirho.make_cell_chirho("b");
let c_chirho = system_chirho.make_cell_chirho("c");

// Constraint: a + b = c
system_chirho.add_adder_chirho(&a_chirho, &b_chirho, &c_chirho);

// Forward: 3 + 4 = ?
system_chirho.set_exact_chirho(&a_chirho, 3.0);
system_chirho.set_exact_chirho(&b_chirho, 4.0);
system_chirho.run_chirho();
// c = 7

// Backward: 3 + ? = 7
system_chirho.set_exact_chirho(&a_chirho, 3.0);
system_chirho.set_exact_chirho(&c_chirho, 7.0);
system_chirho.run_chirho();
// b = 4

Interval Propagation

use propagators_chirho::{IntervalChirho, NumericInfoChirho};

// "The value is between 20 and 30"
let partial_chirho = NumericInfoChirho::interval_chirho(20.0, 30.0);

// "Actually, it's between 25 and 35"
let more_info_chirho = NumericInfoChirho::interval_chirho(25.0, 35.0);

// Merge: intersection is [25, 30]
let refined_chirho = partial_chirho.merge_chirho(&more_info_chirho);

Pythagorean Theorem (Backwards!)

use propagators_chirho::prelude_chirho::*;

let mut system_chirho = ConstraintSystemChirho::new_chirho();

let a_chirho = system_chirho.make_cell_chirho("a");
let b_chirho = system_chirho.make_cell_chirho("b");
let c_chirho = system_chirho.make_cell_chirho("c");

// a² + b² = c²
system_chirho.add_pythagorean_chirho(&a_chirho, &b_chirho, &c_chirho);

// Given c=13 and a=5, find b
system_chirho.set_exact_chirho(&c_chirho, 13.0);
system_chirho.set_exact_chirho(&a_chirho, 5.0);
system_chirho.set_interval_chirho(&b_chirho, 0.0, f64::INFINITY);  // b > 0
system_chirho.run_chirho();
// b = 12 (since 5² + 12² = 13²)

Truth Maintenance

use propagators_chirho::{BeliefChirho, TmsCellChirho, WorldviewChirho, NumericInfoChirho};

let cell_chirho = TmsCellChirho::new_chirho("temperature");

// Add beliefs from different sources
cell_chirho.add_belief_chirho(BeliefChirho::with_premises_chirho(
    NumericInfoChirho::exact_chirho(25.0),
    vec!["sensor_a".to_string()].into_iter().collect(),
    "sensor A reading",
));

cell_chirho.add_belief_chirho(BeliefChirho::with_premises_chirho(
    NumericInfoChirho::exact_chirho(26.0),
    vec!["sensor_b".to_string()].into_iter().collect(),
    "sensor B reading",
));

// Query under different worldviews
let wv_a_chirho = WorldviewChirho::new_chirho().assume_chirho("sensor_a".to_string());
let value_a_chirho = cell_chirho.content_in_worldview_chirho(&wv_a_chirho);
// value_a = 25.0

Running Examples

cargo run --example temperature_chirho   # Bidirectional temperature conversion
cargo run --example pythagorean_chirho   # Pythagorean theorem
cargo run --example electrical_chirho    # Electrical circuit analysis
cargo run --example sudoku_chirho        # Sudoku solver

Performance

Features

Enable high-performance arena mode for ~2x faster network operations:

[dependencies]
propagators-chirho = { version = "0.1", features = ["arena"] }

use propagators_chirho::arena_chirho::ArenaNetworkChirho;

let mut net_chirho = ArenaNetworkChirho::new_chirho();
let a_chirho = net_chirho.make_cell_chirho();
// ... faster due to contiguous storage and no Rc overhead

Benchmarks

Interval Primitives: propagators-chirho vs inari

IEEE 754-2019 Compliance: When Does It Matter?

inari provides IEEE 754-2019 compliant interval arithmetic. We don't. Here's when that matters:

What IEEE compliance guarantees:

• The true mathematical result is always within the computed interval
• Proper directed rounding (round toward ±∞)
• Correct handling of NaN, infinities, subnormals
• Reproducible results across platforms

What we sacrifice for speed:

• Use default round-to-nearest (may miss true value by ULP in edge cases)
• Simpler NaN/infinity handling
• Potentially tighter intervals that could theoretically exclude the true value

Bottom line: For constraint propagation and bidirectional computation (our primary use case), IEEE compliance is unnecessary overhead. If you need verified numerical computation, use inari and accept the 28-51x slowdown.

Network Propagation

Comparison to Other Systems

Running Benchmarks

# Basic benchmarks
cargo bench

# With arena mode
cargo bench --features arena

# Comparison against other libraries (requires tmp-chirho/)
cd tmp-chirho/comparison-bench-chirho && cargo bench

Testing

cargo test                                          # Run all tests
cargo test --features arena                         # Test arena mode
cargo test --features parallel                      # Test parallel mode
cargo test --features serde                         # Test serialization
cargo test --features "parallel,serde,arena,tracing,tms-full"  # All std features
cargo test --test property_tests_chirho             # Property-based tests

Formal Verification (Kani)

cargo kani --features kani    # Run Kani proofs for interval arithmetic laws

Architecture

┌─────────────────────────────────────────────────────────────────┐
│                     Constraint System                            │
├─────────────────────────────────────────────────────────────────┤
│                                                                  │
│   ┌──────────┐      ┌──────────────┐      ┌──────────┐         │
│   │ Cell A   │─────▶│  Propagator  │─────▶│ Cell C   │         │
│   │ [3, 5]   │      │   a + b = c  │      │ [7, 12]  │         │
│   └──────────┘      └──────────────┘      └──────────┘         │
│        ▲                   ▲                   │                │
│        │                   │                   │                │
│   ┌──────────┐             │                   │                │
│   │ Cell B   │─────────────┘                   │                │
│   │ [4, 7]   │◀────────────────────────────────┘                │
│   └──────────┘         (bidirectional!)                         │
│                                                                  │
├─────────────────────────────────────────────────────────────────┤
│                         Scheduler                                │
│   • Maintains queue of alerted propagators                      │
│   • Runs until fixpoint (no more changes)                       │
└─────────────────────────────────────────────────────────────────┘

Mathematical Foundations

Partial Information Lattice

           Contradiction (⊤)
                 ↑
      ┌─────────┴─────────┐
      ↑                   ↑
 Interval [a,b]    Interval [c,d]  ...
      ↑                   ↑
      └─────────┬─────────┘
                ↑
           Nothing (⊥)

Key Properties

• Monotonicity: Information can only increase (intervals narrow)
• Confluence: Order of propagator execution doesn't affect final result
• Soundness: Propagated intervals always contain the true value

References

1. Radul, A., & Sussman, G. J. (2009). The Art of the Propagator. MIT CSAIL Technical Report. https://dspace.mit.edu/handle/1721.1/44215

2. Radul, A. (2009). Propagation Networks: A Flexible and Expressive Substrate for Computation. PhD Thesis, MIT. https://dspace.mit.edu/handle/1721.1/54635

3. Stallman, R. M., & Sussman, G. J. (1977). Forward Reasoning and Dependency-Directed Backtracking. Artificial Intelligence, 9(2).

4. de Kleer, J. (1986). An Assumption-based TMS. Artificial Intelligence, 28(2).

5. Moore, R. E. (1966). Interval Analysis. Prentice-Hall.

License

MIT License

Gloria in excelsis Deo 🕊️