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

A summary of the paper and how gen uses 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.

How gen uses this

gen-scope

Monotonic convergence for circular attributes (Radul S2-S4, merge contract). circular { carrier; } f declares an attribute computed as a least fixed point. The carrier states the lattice: a bottom to start from, an order leq, a finite height, and whether the order is over a quotient of the values. The evaluator iterates f from bottom until the value stops changing, within a bound derived from the declared heights. This is a single-cell propagator network: the cell’s value is the attribute, the propagator is f, and quiescence is convergence. Radul’s merge contract, where each step refines or repeats the cell’s content, is the monotonicity the carrier declares.

Cells with several sources (Radul S3, multiple-source merge). A scope graph node receives values from several places: inherited attributes from the parent chain, synthesized attributes from children, attributes reached over import edges, and collection attributes aggregated across a traversal. collectionAttr traverses imports, children, siblings, ancestors or labelled edges and combines the extracted values, like Radul’s interval-intersection pattern where several independent measurements refine one estimate.

Concrete mapping:

• circular { carrier; } f = 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 = cell content caching (S2, a cell returns its stored content without recomputation)

gen-dispatch

Quiescence of rule dispatch (Radul S2 scheduling, S7 quiescence). dispatch is a pure, one-shot function of rules and context: a given context always yields the same actions. Iteration belongs to the caller, which threads the domain state through repeated dispatch with a gen-scope circular attribute and reads the actions at the fixpoint. The fixpoint is Radul’s quiescence: no rule adds new information to the context. Because the actions are recomputed from the converged state, they do not depend on the path the iteration took, and dispatch keeps no record of which rules already fired.

gen-graph

Monotonic convergence for edge maps (Radul S2-S4, monotonic accumulation). fixpoint { maxIter; } step seed iterates an edge-map transformation until it stops changing. It fails with an error naming the withdrawn edge when a step removes an edge the current map holds, which encodes Radul’s principle that cell content only grows. The edge map is a cell, step is a propagator, seed is the initial state, and convergence is quiescence.

Concrete mapping:

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

Further directions

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. gen’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 gen encounters a conflict (e.g., two aspects setting the same NixOS option contradictorily), it fails 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). gen’s information flow is primarily top-down: entity declarations produce scope graph nodes, rules fire forward, class content flows 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.

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 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.