Composition literature: what the representation must support

Our broader goal is to understand future computational behavior represented by finite rules with bounded local access and allocation. The composition question asks what work remains when constraint fragments have been prepared independently. This review compares published results that separate semantic summaries, representation maintenance, and version history. It supplies research direction, not a new lower bound.

Compilation: answering a query versus constructing a result

Darwiche and Marquis’s A Knowledge Compilation Map (2002), Sections 3–5 and Tables 5 and 7, distinguishes succinctness, supported queries, and transformations. Its bounded conjunction means polynomial-time conjunction of two compiled inputs; it does not mean bounded local work. A common variable order matters for OBDDs. A polynomially small equivalent representation need not have a polynomial-time compilation algorithm. This is a refreshed comparator already used in our earlier SAT boundary note, not a newly discovered principle.

Question for us: which transformations must a stored fragment support, in which encoded size, and with what charge for preparation and deferred answers?

Canonicity can change the cost of composition

Van den Broeck and Darwiche’s On the Role of Canonicity in Knowledge Compilation (2015), Theorems 1 and 3 and Table 2, distinguishes compressed canonical SDDs from uncompressed SDDs. Relative to a fixed vtree, compression can increase size from polynomial to exponential in the number of variables. Binary conjunction, conditioning on a literal, and forgetting one variable have different guarantees for the two representations. These separations do not establish the same obstruction when the vtree may change.

Our inference: a cost imposed by a chosen normal form must be distinguished from work required to answer the underlying query. Canonical mathematical representations also do not provide free shared pointer identities between independently prepared heaps. The next comparison should identify whether any proposed FPRD benefit actually requires canonicity, compression, or a common decomposition.

Persistence: which operations are being made persistent?

Collette, Iacono, and Langerman’s Confluent Persistence Revisited (2011 preprint; SODA 2012), Section 2 and Corollary 7, provides a transformation for bounded-indegree linked structures. Modification and pointer traversal take logarithmic amortized time; modifications use constant additional space. A merge must not contain the same node twice; explicitly copying a structure pays its size. The underlying model permits mutable fields, integers, and version bookkeeping.

Our inference: this does not make a semantic compatibility test cheap merely because two version roots can be combined. It is also not already an implementation by immutable finite-tag records with bounded worst-case local work. Physical sharing of nodes and overlap of constraint variables are separate obligations to check.

Dynamic logic: useful structural promises, different work measure

Datta and collaborators’ Reachability is in DynFO, Theorems 1–2 and Sections 2–4, maintains relations with first-order update formulas. Simultaneous updates of auxiliary relations measure logical or parallel complexity; they do not bound sequential record accesses or allocations per change. Consequently, a DynFO result cannot be imported as a bounded-local-work implementation without a resource translation.

Datta and collaborators’ A Strategy for Dynamic Programs: Start over and Muddle through (2019), Theorem 6.1, treats each fixed MSO query on graphs remaining within a fixed treewidth bound. Its Theorem 6.3 composes logical types through a center and petals. Petals overlap only in the center; each has bounded interface size and a private identifier there; every relation tuple is inside the center or a petal. A transformed query runs on the center enriched by type information. This is a structural composition theorem, not an arbitrary-overlap or constant-time persistent-join theorem.

Our inference: compatible decompositions and interfaces deserve scrutiny. A structural promise must survive the permitted join, and finding, aligning, or maintaining its decomposition must be charged.

What this changes in the investigation

The completed affine comparison remains closed. Its probe lower bound and paid normalization construction should not become an automatic invitation to optimize another constant.

The worked canonical-output diagnostic now separates required future observations from optional normalization requirements in that fixed-vtree example. Its large explicit output does not force expensive assignment queries, and unrestricted stored preparation defeats an allocation-only post-preparation bound. The next question is whether independently small representations need a shared variable order or decomposition to compose efficiently. No new general theorem is claimed.

For each candidate we need an explicit contract: allowed joins and future queries; actual input and stored size; preparation; composition and deferred query work; historical allocation; and model-specific observations. A published theorem may close a candidate, suggest a construction, or expose a missing hypothesis. Each is useful progress. The reviewed statements are imported theorems checked against primary text. No new mathematical theorem, formal verification, finite experiment, or novelty claim is made here; this is a focused review, not an exhaustive survey.