Radul & Sussman (2009) -- The Art of the Propagator

The paper

A. Radul and G. J. Sussman, “The art of the propagator,” MIT CSAIL Technical Report MIT-CSAIL-TR-2009-002, 2009.

read the paper

This page is our reading of it, not a substitute for it.

Paper Summary

Traditional programming languages enforce a fundamental restriction: each storage location (variable, field, intermediate result) receives its value from exactly one source. This constraint means a single computation must be responsible for producing the complete value for any given place. Radul and Sussman ask: what happens if we relax this restriction and allow places to receive values from multiple sources?

The paper develops the propagator network as a computational model exploring this question. A propagator network consists of two kinds of entities: cells, which store accumulated information, and propagators, autonomous machines that continuously examine their input cells and add information to output cells based on deductions they can make. The key property is that cells accept information from multiple sources and are responsible for merging partial information into a coherent whole. When a cell’s content changes, it alerts neighboring propagators, which may then contribute further refined information — a reactive, monotonic convergence process.

The development proceeds through five stages of increasing sophistication, each building on the previous:

Stage 1: Basic propagation (S2). Cells store single values; propagators are lifted Scheme functions. A cell receiving a value it already holds does nothing; receiving a contradictory value signals an error. The authors demonstrate iteration via compound propagators (Heron’s method for square roots), establishing the wiring-diagram metaphor for network construction. The compound-propagator construct introduces lazy activation: a compound body is built only when its input cells first acquire values, enabling recursive network construction without infinite unfolding.

Stage 2: Partial information via intervals (S3). Cells store interval-valued approximations. When multiple sources contribute interval constraints, the cell intersects them — the merge operation for this domain. The building-height example (measuring via dropped barometer and shadow triangles) demonstrates that combining independent partial measurements produces a result more precise than either alone. The merge behavior is factored into cells: the cell decides how to combine, not the propagators.

Stage 3: Multidirectional constraint propagation (S4). By stacking a propagator with its inverse (e.g., product x y total installs both multiplier x y total and divider total x y), unidirectional computations become bidirectional constraints. Information flows in whichever direction has sufficient inputs. This enables backward refinement: knowing the building’s exact height refines the fall-time and barometer-height measurements retroactively. The cells’ monotonic merge ensures no oscillation — each refinement only narrows intervals.

Stage 4: Generic operations and merge (S5). The cell’s merge behavior is extracted into a generic function merge dispatched by the types of the old and new information. The contract is precise: merge returns eq?-identical to old content when the new is redundant, eq?-identical to new content when old is fully superseded, a fresh merged value when genuinely new information arrives, or a distinguished contradiction value when the information is inconsistent. The contradictory? predicate is also generic and extensible. Propagator arithmetic is upgraded to generic operations, enabling intervals and raw numbers to interoperate transparently.

Stage 5: Dependency tracking and truth maintenance (S6). This is the paper’s most substantial contribution, developed across three levels. First, provenance tracking (S6.1): values are decorated with the set of premises that justify them (the supported structure, called v&s internally). The merge operation on supported values selects the value with the fewest supporting premises, avoiding unnecessary dependency accumulation. Second, truth maintenance systems (S6.2): cells hold a TMS containing multiple v&s records, each justified independently. The strongest-consequence procedure merges all currently-believed values; a global worldview (the set of “in” premises) determines which premises are active. Users can kick-out! and bring-in! premises to explore alternate worldviews without recomputation — the TMS remembers all previously derived values. Third, implicit search (S6.3): the binary-amb propagator manufactures hypothetical premises and uses dependency-directed backtracking to explore choice spaces. When a contradiction is found, the system identifies the nogood set (the minimal set of premises responsible), records it to prevent recurrence, and backtracks to an alternative. This implements a distributed incremental implicit-SAT solver that integrates with the network’s ordinary computation.

The paper closes (S7) by identifying open problems: demand-driven (normal-order) propagation where cells “pull” needed information; per-component dependency tracking for compound data; and concurrent implementation where only individual cells need synchronization.

Key Concepts

• Cells as merge points. A cell accumulates information from multiple sources via a generic merge function. The merge contract (return old when redundant, new when superseding, fresh when genuinely informative, contradiction when inconsistent) ensures monotonic convergence. This is the central abstraction — cells own the lattice structure.

• Propagators as autonomous deduction agents. Propagators are stateless functions triggered by cell changes. They examine inputs and add information to outputs. The network’s behavior emerges from the collective action of many simple propagators, not from a centralized controller.

• Monotonic information accumulation. Information in cells only grows (in the lattice-theoretic sense). Intervals narrow, dependency sets refine, but no information is retracted. This guarantees convergence: the network quiesces when no propagator can contribute new information.

• Generic merge as the extensibility mechanism. New partial information domains (numbers, intervals, supported values, TMSes) are added by extending the merge generic function and the arithmetic generic operations. Cells and propagators remain unchanged.

• Truth maintenance for worldview management. TMSes allow cells to hold multiple justified values simultaneously. Querying under different worldviews (premise subsets) is O(TMS-size), not O(network-recomputation). The system remembers all derivations, making worldview switching cheap.

• Dependency-directed backtracking. When contradictions arise, the nogood set identifies which premises are responsible. The binary-amb propagator performs resolution: if both hypotheses lead to contradictions, their nogood sets are pairwise-unioned to derive a new nogood not involving either hypothesis. This implements propositional resolution within the network.

• Quiescence as the stability criterion. The network is “done” when no propagator can add new information to any cell. This is not explicitly computed — it emerges from the reactive scheduling. Quiescence corresponds to reaching a fixed point in the lattice of cell states.

• Compound propagators for modularity. compound-propagator delays body construction until inputs are available, enabling recursive network definitions without infinite unfolding. This is the propagator analogue of lazy evaluation.

Implementation Mapping

Current Usage in Gen Ecosystem

gen-scope (Minor)

Monotonic convergence for circular attribute iteration (Radul S2-S4, merge contract). gen-scope’s circular attribute combinator iterates a function on a node’s attribute value until the result stabilizes (checked by eq). This is structurally identical to a single-cell propagator network where the cell’s value is the attribute, the propagator is the iteration function, and quiescence is convergence. The monotonicity requirement — iteration must converge rather than oscillate — directly follows from Radul’s merge contract: each iteration step must produce information that either refines (narrows) the previous value or equals it.

Cells accepting multiple sources as design influence on scope graph merging (Radul S3, multiple-source merge). Scope graph nodes receive attribute contributions from multiple sources: inherited attributes from the parent chain, synthesized attributes from children, import-edge attributes from referenced scopes, and collection attributes aggregated across traversal. This multi-source model is conceptually a cell receiving information from multiple propagators. The collectionAttr combinator in particular — traversing imports, children, siblings, or ancestors and combining extracted values via a merge function — mirrors Radul’s interval-intersection pattern where multiple independent measurements refine a shared estimate.

Concrete mapping:

• circular { init; eq; maxIter } = single-cell propagator with quiescence check (S2 scheduling + S5 merge contract)
• collectionAttr { traverse; extract; combine } = multi-source cell with domain-specific merge (S3 interval intersection pattern)
• inherit' parent-chain resolution = unidirectional propagation following structural edges (S2 basic propagation)
• _eval memoization cache = cell content caching (S2, a cell returns its stored content without recomputation)

gen-derive (Minor)

Quiescence as stability criterion for fixpoint loop (Radul S2 scheduling, S7 quiescence discussion). gen-derive’s fixpoint iterates rule dispatch until the context stabilizes: eq oldCtx newCtx returns true, meaning no rule produced new information. This is precisely Radul’s quiescence condition — the network (set of rules) has reached a state where no propagator (rule) can add new information to any cell (the context). The fired set that prevents identified rules from re-firing across iterations is analogous to a propagator recognizing that its output cell already contains the information it would contribute (the “adding redundant information does nothing” branch of the merge contract).

Monotonic context widening (Radul S3-S4, monotonic merge). gen-derive’s combine function merges old context with extracted feedback. The invariant that context only grows (new keys added, no keys removed) mirrors Radul’s monotonic information accumulation in cells. Non-monotonic steps (context shrinking) would correspond to Radul’s contradiction case.

Concrete mapping:

• fixpoint convergence loop = propagator network scheduling to quiescence (S2)
• eq stability check = quiescence detection (S7, “no propagator can add new information”)
• fired set = merge contract’s redundancy branch (“adding nothing already known does nothing”)
• combine = merge function on context domain (S5 generic merge)
• maxIter = safety bound against non-convergent networks (not in paper; gen-derive’s practical addition)

gen-graph (Minor)

Monotonic convergence model underlies fixpoint iteration (Radul S2-S4, monotonic accumulation). gen-graph’s fixpoint { seed, step, maxIter } iterates edge-map transformations until stable. The monotonicity enforcement (throwing on edge-count shrinkage) directly encodes Radul’s principle that cell content only grows. The edge map is a cell; step is a propagator; seed is the initial “nothing” state; convergence is quiescence.

Concrete mapping:

• graph.fixpoint = single-cell propagator network (S2) with monotonicity invariant (S3-S4)
• graph.compose = compound propagator combining two edge-map sources (S4 multidirectional)
• graph.transitiveClosure = iterative refinement to quiescence (S2 Heron’s method pattern, applied to reachability)
• graph.unionEdges = merge (set union) on the edge-map semilattice (S5 generic merge on the set domain)

Relevance to Den v2 HOAG Pipeline

Den v2’s demand-driven HOAG over scope graphs embodies the propagator model at an architectural level, even though the implementation uses Nix lazy evaluation rather than an explicit propagator scheduler.

Scope nodes as cells. Each scope graph node accumulates attribute values from multiple sources: policies contribute effects, aspects contribute class content, pipes deliver collection data, and neededBy injects reverse-edge aspects. This is Radul’s core insight — places receiving values from multiple sources. The node’s attribute computation (_eval) serves as the merge point, combining contributions according to domain-specific rules (list concatenation for collections, evalModules merge for class content, set union for edges).

Policies and aspects as propagators. Policies are autonomous functions that examine their scope context (input cells) and produce effects (output contributions). When a policy fires and enriches a scope’s context, other policies sensitive to that context may fire in turn — exactly the reactive alert-propagators chain from Radul S2. The gen-derive fixpoint loop manages the scheduling, but the conceptual model is a propagator network where policies push information through scope nodes.

Monotonic scope graph expansion. The scope graph only grows: spawn adds nodes, edge adds edges, enrich adds declarations, inject adds modules. No operation retracts information. drop is modeled as a constraint (pruning resolution paths) rather than retraction, preserving monotonicity. This directly implements Radul’s monotonic accumulation principle — the scope graph state is a lattice value that only ascends.

Quiescence as pipeline termination. The den v2 pipeline terminates when no policy can fire new effects and no neededBy scan discovers new reverse edges. This is Radul’s quiescence: the network of policies has reached a state where no propagator can contribute new information. The finite declaration set (hosts, users, aspects are user-declared and bounded) guarantees that the ascending chain through scope graph states has finite height, ensuring quiescence is reached.

Pipe convergence as multi-source merge. Den v2’s pipe system — pipe.from, pipe.gather, pipe.ascend, pipe.source, pipe.target, pipe.channel — routes collection data through scope nodes. Multiple pipes may contribute to the same collection on the same node, requiring merge. This is Radul’s interval-intersection pattern generalized: multiple independent sources contribute partial information to a cell, and the cell’s merge strategy (list concatenation, attrset merge, or custom combine) produces the aggregate result.

Demand-driven as “pull” propagation. Radul’s S7 identifies demand-driven propagation as an open problem: propagators that “pull” needed information rather than eagerly pushing all deductions. Den v2 addresses this through Nix’s native lazy evaluation — attributes are thunks that compute only when demanded. gen-scope’s _eval cache means each attribute is computed at most once, and only if demanded. This realizes the demand-driven propagation that Radul identifies as future work, using the host language’s laziness as the scheduling mechanism.

Appendix: Follow-up Work

Unexploited Ideas

Truth Maintenance Systems for worldview management (S6.2). The TMS mechanism — cells holding multiple justified values, queryable under different worldview subsets — has no analogue in the gen ecosystem. Den v2’s scope graph holds a single worldview (the full set of declared entities and aspects). A TMS-backed scope graph could support: “what does this configuration look like if we remove host X?” or “what changes if we add aspect Y?” without re-evaluating the entire graph. Each worldview would be a premise set; the TMS would cache all derivations across worldviews.

Dependency-directed backtracking for configuration conflict resolution (S6.3). When den v2 encounters a conflict (e.g., two aspects setting the same NixOS option contradictorily), the current approach is to error with a diagnostic. Radul’s dependency-directed backtracking could instead identify the minimal set of premises (entity declarations, aspect includes) that cause the conflict, and either report a precise nogood set or automatically explore alternative configurations. The binary-amb mechanism could power “try aspect A; if it conflicts, fall back to aspect B” semantics.

Provenance tracking for attribution (S6.1). The supported value structure — every computed result tagged with the premises that justify it — would enable answering “why does this NixOS option have this value?” by tracing the support set back through scope graph edges to the original entity declarations and aspect content. gen-bind’s provenance metadata is a step in this direction but operates at the binding level, not at the value level.

Multidirectional constraint propagation for bidirectional entity inference (S4). Currently, den’s information flow is primarily top-down: entity declarations produce scope graph nodes, policies fire forward, class content emits downward. Radul’s bidirectional constraints would enable bottom-up inference: knowing a NixOS option’s required value could propagate backward to constrain which aspects must be included, or knowing a user’s required home-manager configuration could infer which host they must be assigned to.

Per-component dependency tracking for compound values (S7). Radul notes that tracking separate dependencies for each component of a pair (or interval bound) eliminates spurious dependency accumulation (the overlap anomaly, Figure 2). In the gen ecosystem, collection attributes aggregate complex structures — tracking per-field dependencies rather than per-aggregate dependencies would enable finer-grained cache invalidation and more precise provenance reporting.

Potential New Libraries or Features

gen-tms: Truth maintenance for Nix attrsets. A library providing: mkTms {} (empty TMS), addSupported tms value premises (add justified value), query tms worldview (strongest consequence under premise subset), nogoods tms (discovered contradictions). Would enable multi-worldview configuration analysis without re-evaluation. Scope: ~300 lines core, ~100 lines gen-scope adapter. Interacts with gen-scope (TMS-backed cells) and gen-derive (nogood-guided backtracking). Complexity: medium — the TMS data structures are straightforward, but integrating with Nix’s lazy evaluation (where “alerting propagators” means invalidating thunks) requires careful design.

Provenance-tracked merge for gen-scope collections. Extend collectionAttr with an optional trackProvenance = true mode that wraps contributed values in { value; source = nodeId; path = [...]; } records. When enabled, the aggregate carries attribution metadata through the merge. Scope: ~80 lines in gen-scope, backward-compatible (new optional parameter). Interacts with gen-bind’s existing provenance infrastructure.

Bounded fixpoint with semantic bounds for gen-derive. Beyond the iteration-count maxIter, add support for semantic bounds: bound = ctx: builtins.length (builtins.attrNames ctx) <= maxContextSize. The fixpoint terminates when either eq detects convergence or bound is exceeded. This mirrors Radul’s compound-propagator pattern where construction is gated on meaningful content. Scope: ~30 lines in gen-derive.

Research Directions

Demand-driven propagation with explicit interest tracking. Radul’s S7 proposes representing “pulls” as explicit requests indicating interest in information. In the gen ecosystem, Nix’s laziness provides implicit demand-driven evaluation, but there is no mechanism for a scope node to declare “I am interested in attributes X and Y from my imports, but not Z.” Explicit interest declarations could enable selective attribute computation in gen-scope — skipping expensive attributes that no downstream consumer demands. This connects to Mokhov 2018’s minimal/constructive build systems.

Concurrent propagator evaluation for fleet-scale scope graphs. Radul’s S7 observes that only individual cells need synchronization in a concurrent propagator network. For fleet-scale den configurations (hundreds of hosts, thousands of aspects), concurrent evaluation of independent subtrees could dramatically reduce evaluation time. Nix’s evaluator is single-threaded, but a multi-process architecture — each process evaluating an independent scope subtree, coordinating via IPC on shared cells — could exploit the propagator model’s natural concurrency. The challenge is identifying independent subtrees in a scope graph with import edges.

Merging worldviews for configuration diff and migration. Given two TMS-backed worldviews (e.g., current production configuration and proposed change), computing the “diff” — which cells’ strongest consequences change — would enable safe configuration migration. The nogood machinery could identify configurations that would introduce contradictions. This extends Radul’s worldview switching from diagnostic exploration to operational tooling.

Interval-valued configuration attributes. Radul’s interval arithmetic enables reasoning about ranges rather than exact values. For capacity planning (CPU allocation between 2-4 cores, memory between 4-8GB), interval-valued attributes in gen-scope could propagate constraints bidirectionally — a host’s total memory constrains its users’ allocations, and user requirements constrain the host’s minimum. The collectionAttr combinator with interval-merge would implement this directly.