Computation, locality & knowledge
Rewriting and confluence; trace monoids for concurrency; sheaves and cohomological gluing; Formal Concept Analysis and ologs — locality, knowledge and data fusion. (Beyond the book.)
Three engineering questions sit just past the abstract algebra: when are two programs the same?, do locally valid claims fit together globally?, and how do you represent knowledge so it can be transferred and checked, not merely written down? This module collects the machinery that answers them — rewriting and confluence, trace monoids, sheaves and their obstructions, and the data-oriented trio of Formal Concept Analysis, ologs, and functorial migration. Each construction hands you a decision procedure or a verifiable object, not just a vocabulary.
Rewriting: reducing expressions to a canonical form
A presentation of a monoid lists generators and relations \(\ell = r\). To compute with it, orient each relation as a one-way rule \(\ell \to r\) — a license to rewrite. This is an abstract rewriting system (ARS): a set \(A\) with a “reduces-to” relation \(\to\). Write \(\xrightarrow{*}\) for its reflexive-transitive closure (“reduces in any number of steps”) and \(\xleftrightarrow{*}\) for the equivalence it generates (“interconvertible”).
Intuition. The rules are simplification moves on an expression — a compiler optimization or an algebraic simplifier: “an idempotent op done twice equals once,” “this pair of instructions may be swapped,” “this step followed by its inverse cancels.” A normal form is an expression to which no move applies: fully reduced. The dream is that reducing two expressions and comparing the results decides whether they are the same.
This needs two properties. First, normal forms must exist: the system is terminating (strongly normalizing) if there is no infinite chain \(x_0 \to x_1 \to \cdots\) — proved by a reduction order, a well-founded measure that every rule strictly decreases. Second, normal forms should be unique, the subtler half handled next.
Pitfall. A normal form is canonical only relative to the rule set and its chosen orientation. Re-orient a relation and you may get a different “fully reduced” expression. Canonicity is a property of the procedure, not a Platonic fact about the expression.
Confluence and completion: deciding equivalence
Termination gives existence; confluence gives uniqueness. A system is confluent when any two divergent reduction paths can be reconciled: if \(x \xrightarrow{*} y\) and \(x \xrightarrow{*} z\), then both reach a common \(w\). As the figure shows, divergent computations close back up into a diamond — the Church–Rosser property — so the order in which you apply rules cannot change the final normal form.
Checking confluence directly is infinite (it quantifies over all pairs of paths). The escape is to weaken it. Local confluence asks the diamond to close only for one-step divergences, and these arise from finitely many critical pairs — the genuine overlaps between left-hand sides of rules. So local confluence is checkable.
Theorem (Newman’s lemma, 1942). For a terminating system, local confluence implies confluence. (Short modern proof: Huet.)
This is the load-bearing result: it converts an infinite check into a finite one. A confluent and terminating system is called convergent, and a convergent system is a decision procedure for \(\xleftrightarrow{*}\) — reduce both sides, compare normal forms. When a presentation is not yet confluent, Knuth–Bendix completion (1970) tries to repair it: orient the equations into terminating rules, then for every non-joinable critical pair add a rule that joins it. Three outcomes are possible — it halts with a convergent system, it fails (a critical pair cannot be oriented), or it runs forever.
Pitfall. Because the word problem for general presented monoids is undecidable (Novikov–Boone), no terminating completion can exist for those instances. Completion is a semi-decision procedure: “no result yet” is never evidence that two terms are equivalent or that they differ.
In the synthesis. Newman’s lemma plus Knuth–Bendix is exactly the toolkit behind RD2’s canonical recipe forms. A library of allowed recipe edits is the rewriting relation \(\to\); deciding whether two process descriptions are the same recipe becomes “reduce both and compare.” The undecidability barrier (P11’s canonical-decomposition program meets a hard wall) is what makes the next construction valuable: it is a fragment where the wall disappears.
Trace monoids: the algebra of harmless reorderings
The undecidable general case has a famous tractable island: suppose the only relations are commutations — some pairs of operations may swap, others may not. This is exactly concurrency, where instructions touching disjoint registers or memory reorder freely (an out-of-order CPU or instruction scheduler exploits this) while instructions contending for the same location do not.
Definition (Trace monoid). Fix an alphabet \(\Sigma\) of operations and a symmetric, irreflexive independence relation \(I \subseteq \Sigma \times \Sigma\). The trace monoid is the quotient of the free monoid \(\Sigma^*\) by allowing exactly the independent pairs to commute: \[ M(\Sigma, I) = \Sigma^* \big/ \{\, ab = ba \mid (a,b) \in I \,\}. \] Its elements are traces (operation-words up to allowed swaps); the complement \(D = (\Sigma\times\Sigma)\setminus I\) is the dependence relation.
This is Mazurkiewicz’s model from concurrency theory; the same algebraic object is Cartier–Foata’s free partially commutative monoid. A trace has a unique Foata normal form — a canonical factorization into maximal blocks of operations that could all fire simultaneously. Two words denote the same trace iff they share this normal form, and the test runs in low-degree polynomial time.
Key. The trace-monoid word problem is decidable, and efficiently so — same Foata form ⟺ same trace. Restricting relations to pure commutations buys back the computability that general presentations lose.
Equivalently, a trace is a labelled partial order on operation occurrences — a dependence graph recording exactly which steps must precede which. This is the same partial-order-of-events picture that string diagrams in a premonoidal category draw, now reduced to a decidable combinatorial object.
In the synthesis. The trace monoid is the precise recipe algebra for RD2/RD3: declare \(I\) from genuine physical independence, and recipes-up-to-reordering come with a fast equivalence test. It is the decidable refinement of the premonoidal process category (RD1) — central, reorderable operations populate \(I\); effectful, order-sensitive ones populate \(D\). The closest existing chemistry bridge is tracelets (Behr, ACT 2019), minimal derivation traces for reaction-rule rewriting.
Pitfall. Independence must be genuine symmetric commutation of whole operations. If one step changes a precondition of another — a write-after-read or any order-sensitive interaction — the pair is dependent. Wrongly placing such a pair in \(I\) silently identifies executions that are not equivalent.
Note (process algebra). When systems must model live interaction rather than static reordering, the escalation is process algebra: CSP (Hoare), CCS (Milner), and the π-calculus (Milner–Parrow–Walker), which adds name mobility. These are languages of prefixing, choice, parallel composition, and channel synchronization, with equivalences such as bisimulation. Trace monoids capture which reorderings are harmless; process algebras model the interaction itself.
Sheaves: local validity and the obstruction to gluing
Now turn from processes to claims. A finding is rarely valid everywhere — a robot’s local map holds only near where it was observed, a sensor reading only within its field of view, a measurement only within its calibrated range. Sheaf theory is the mathematics of data indexed by context, and of whether local data (overlapping local maps, say) assemble into global data (one consistent map).
A presheaf \(F\) on a space \(X\) is a contravariant functor from open sets to \(\mathbf{Set}\): to each open \(U\) it assigns the sections \(F(U)\) (data valid on \(U\)), and to each inclusion \(V \subseteq U\) a restriction map \(\rho^U_V : F(U) \to F(V)\), functorially. The germ near a point is the stalk \(F_x = \varinjlim_{U \ni x} F(U)\), a colimit over shrinking neighborhoods.
A presheaf merely files data by context; a sheaf additionally guarantees local-to-global coherence. For every open cover \(U = \bigcup_i U_i\):
- (Locality) two sections of \(F(U)\) that agree on every \(U_i\) are equal;
- (Gluing) a family of sections \(s_i \in F(U_i)\) that agree on all overlaps \(U_i \cap U_j\) comes from a unique global section \(s \in F(U)\).
Intuition. Think of each open set as a region of validity. Restriction zooms a global claim down to a sub-region. The gluing axiom says: if your local claims are pairwise consistent wherever their regions overlap, they fuse into one consistent global claim — and only one. A presheaf without gluing is a filing cabinet; a sheaf is a filing cabinet that certifies its contents cohere.
The decisive insight is that gluing can fail in a structured, measurable way: every pair of overlapping regions can agree, yet no global section restricts to all of them at once — a quantity that drifts as you travel around a loop of overlaps. Sheaf cohomology measures this. For a sheaf of abelian groups, \(H^n(X,F)\) are the right-derived functors of the global-sections functor \(\Gamma(X,-) = F(X)\) (computable via Čech cohomology). Then:
- \(H^0(X,F) = F(X)\) — what globally exists;
- a class in \(H^1(X,F)\) is precisely the obstruction to gluing compatible local sections into a global one. \(H^1 = 0\) means every locally consistent family glues.
In the synthesis. Sheaves are the genuine formal home of P6 — locality and scope of validity. A claim valid only in one processing window is literally a section over that open set, and whether such claims cohere is the gluing question. Robinson’s sheaf-theoretic data fusion (Topological Signal Processing, 2014; “Sheaves are the canonical data structure for sensor integration,” 2017) makes this quantitative for RD6: model heterogeneous, partially-consistent sources as sections; fusion is finding a global section; the degree of agreement is the consistency radius (distance to the nearest global section), with \(H^1\)-type obstructions when exact gluing fails.
Bridge. This is the abstract engine behind two materials modules. Overlapping, non-identical assays of one formulation — different instruments, operators, or scales reporting the “same” quantity — are a fusion problem in exactly Robinson’s sense; see measurement, calibration, and data fusion. And a finding that holds only inside a processing window is a section whose scope must be declared and whose coherence with neighboring claims is the gluing test that organizes an R&D knowledge system. The consistency radius is a real, computable number you can put on a dashboard.
Pitfall. Not every “data-indexed-by-context” assignment is a sheaf. A failure to glue — or a non-unique gluing — is real information about inconsistency, not a defect to engineer away.
Knowledge as a verifiable object: FCA, ologs, migration
The last cluster makes knowledge itself a structured object (P10) along three orthogonal axes: derive conceptual structure from data (FCA), represent it composably and checkably (ologs), and move it across domains with guarantees (migration).
Formal Concept Analysis — structure from an incidence table
Start from a raw table — say a data-mining feature matrix: rows are objects (records, devices, users), columns are attributes, a cross marks “has.” A formal context is \(\mathbb{K} = (G, M, I)\) — objects \(G\), attributes \(M\), incidence \(I \subseteq G \times M\). The derivation operators \[ A' = \{\, m : \forall g \in A,\ (g,m) \in I \,\}, \qquad B' = \{\, g : \forall m \in B,\ (g,m) \in I \,\} \] send a set of objects to the attributes they all share and a set of attributes to the objects having them all. Together they form an antitone Galois connection — the order-reversing adjunction from foundations.
Definition (Formal concept). A pair \((A,B)\) with \(A' = B\) and \(B' = A\): a maximal rectangle of crosses. \(A\) is the extent (the cluster of objects), \(B\) the intent (their exact shared attributes); both are closed under \((-)''\).
Theorem (basic theorem of FCA, Wille). Ordered by extent inclusion, the concepts of any context form a complete lattice — the concept lattice — and every complete lattice arises this way. Attribute implications \(B_1 \Rightarrow B_2\) (read off, e.g., the Duquenne–Guigues stem base) surface the dependency rules latent in the table.
In the synthesis. FCA turns a formulation–property table into a navigable concept lattice (RD6, P10): nodes are named clusters and the implications expose structure–property rules bottom-up. It is established in chemistry / SAR; applying it to materials and formulation tables is a genuine gap. The construction directly realizes degeneracy and fibers (P4) — a concept’s extent is the fiber of “exactly these properties.”
Pitfall. FCA needs exact binary incidence, so continuous-valued attributes must first be scaled (binned) — and the scaling shapes the lattice. Concept lattices also grow combinatorially and reflect the chosen, possibly noisy incidence exactly.
Ologs and functorial data migration
An olog (ontology log; Spivak–Kent, 2012) is a category used directly as knowledge representation: objects are types (boxes — “an order,” “a customer”), morphisms are aspects (arrows — “…was placed by…”), and imposed commuting diagrams are facts. This is an entity–relationship model read categorically. An instance is a functor to \(\mathbf{Set}\).
Key. Because an olog is literally a category, knowledge is typed, composable, and verifiable — a fact is a checkable path equality (two arrow-paths asserted equal), not an informal link in a semantic network. It doubles as a database schema.
That last remark is the bridge to transfer. A schema is a small category \(\mathcal{S}\); an instance is a functor \(I : \mathcal{S} \to \mathbf{Set}\) (each type to its set of rows, compatibly with relations). A functor \(F : \mathcal{S} \to \mathcal{T}\) between schemas induces three canonical ways to move populated data — an adjoint triple \[ \Sigma_F \dashv \Delta_F \dashv \Pi_F, \] where \(\Delta_F\) pulls back / re-indexes along \(F\), its left adjoint \(\Sigma_F\) pushes forward freely (via joins, possibly creating rows), and its right adjoint \(\Pi_F\) pushes forward constrained (via matching, possibly discarding rows). This is implemented in CQL (Categorical Query Language).
In the synthesis. This realizes P7/RD4 — transfer-as-functoriality. Ologs supply the schemas; functorial migration moves populated knowledge with adjoint guarantees, so the transfer is structure-preserving by construction. Ologs are already applied to hierarchical materials (Giesa–Spivak–Buehler), and CQL has integrated a real materials database (Brown–Spivak–Wisnesky, OQMD, 2019). The open part is the tacit, experimental know-how slice — structured databases migrate well today; undocumented judgement does not yet.
Pitfall. The three migrations are not interchangeable: \(\Delta\) projects, \(\Sigma\) can create rows, \(\Pi\) can constrain rows away. The adjointness tells you which is correct — choosing wrong silently fabricates or discards data.
Bridge. Functorial migration is the principled alternative to ad-hoc ETL when porting findings between labs, lines, or product families — the backbone of horizontal deployment in an R&D knowledge system. It is the data-engineering face of the same transfer-as-functor story told categorically elsewhere.
How the three combine
The three knowledge tools are orthogonal axes of one account (P10), each covering a weakness of the others:
| Tool | What it provides | Direction |
|---|---|---|
| Ologs + migration | composability & verifiability — facts are checkable diagram equalities; viewpoints align by functors \(\Sigma_F \dashv \Delta_F \dashv \Pi_F\) | top-down schema |
| FCA | derived conceptual structure — the Galois connection computes latent types and implications from raw incidence | bottom-up from data |
| Sheaves (\(H^1\)) | declared scope & consistency — every claim carries its region of validity; gluing tests global coherence | local-to-global |
Run together, a knowledge object is a composable, verifiable structure (olog + migration) whose conceptual content is derived from and audited against data (FCA — the lattice can seed or check the olog’s hierarchy) and whose every assertion carries a declared scope with computable consistency diagnosis (sheaves and \(H^1\)). That is the precise meaning of “knowledge as a composable verifiable object with declared scope” (P10) — with RD2’s decidable recipe algebra supplying the matching account for processes.
Recap
- Rewriting orients relations into rules; termination gives existence of normal forms, confluence gives uniqueness, and convergent = terminating + confluent is a decision procedure for recipe equivalence (RD2).
- Newman’s lemma reduces confluence to finitely many critical pairs for terminating systems; Knuth–Bendix repairs confluence but is only a semi-decision procedure — the general monoid word problem is undecidable.
- Trace monoids \(M(\Sigma,I)\) are the decidable island: quotient the free monoid by genuine commutations, and Foata normal form decides equivalence in polynomial time (RD2/RD3).
- Sheaves formalize locality (P6): claims are sections over their region of validity; \(H^1\) is the obstruction to gluing, and the consistency radius quantifies data fusion (RD6) — directly serving measurement and the R&D system.
- FCA derives a concept lattice from an incidence table; ologs make knowledge a verifiable category; functorial migration (\(\Sigma_F \dashv \Delta_F \dashv \Pi_F\)) transfers populated data with adjoint guarantees (P7/P10, RD4/RD6).
Part of a four-document set: the ARiSE draft (problem + AI solution), this modular Mathematics reference, the companion materials reference, and the synthesis. Generated from modular Markdown with a custom static-site builder.
Mathematics is typeset with MathJax (loaded once from a CDN with Subresource Integrity; needs network on first view). Diagrams are inline SVG and follow the light/dark theme. Keyboard: / search · [ ] prev/next · t theme.