Algebraic architecture theory helps understand software changes reliably
Foundations of Algebraic Architecture Theory: A Rising Sea of Geometry, Transport, Comparison, and Reconstruction
Software EngineeringProgramming Languages
Summary
Software changes made by AI need to be examined carefully to see what parts stay the same and where problems might appear. The authors develop Algebraic Architecture Theory (AAT) to capture the structure and rules that software must follow, helping to reconstruct and compare different versions. Their main result shows how local pieces relate to the whole, making it easier to detect if something breaks globally or can be fixed. This theory also helps classify changes, diagnose issues, and transport information accurately between versions.
What this means in practice
- •For software engineers: Identify and classify operation-preserving software changes to ensure global consistency from local modifications during AI-assisted development.
- •For devops teams: Diagnose and repair software inconsistencies by detecting where local software updates fail to extend globally using obstruction criteria.
A theory result. No direct application yet.
Authors
Hiroyuki Nakahata
Abstract
AI-generated software changes make it increasingly important to determine what a change preserves, where local consistency fails to extend globally, and which alternatives remain. We develop the foundations of Algebraic Architecture Theory (AAT) from Atoms, typed primitive facts, and Laws, equations that objects must satisfy. A reading specifies what counts as structure and which operations and laws to preserve. The main reconstruction theorem identifies the category of full geometries and all their structure-preserving morphisms with an independently defined category of local models, up to equivalence. Objects are recovered up to isomorphism and morphisms between fixed endpoints uniquely. The theory addresses gluing, diagnosis, transport, classification of changes, and reconstruction. From finite Atom families we construct cores closed under operations and geometries with sites and coefficients. We give conditions under which a Cech obstruction detects the existence of a global state and, through comparison with repair semantics, a global repair. We compare diagnoses and give a finite criterion for uniform invariance given computable finite data. Transport along exact changes has a universal property and commutes with base change on exact pointed pullback squares. Comparisons of routes generated from the same square, finite comparison diagram, and geometry factor into an invertible comparison and an idempotent normalization. We characterize when observations determine comparison preservation and classify compatible lifts. Encodings of lens and protocol semantics preserve and reflect laws and recover semantics-preserving morphisms. Applications classify and count operation-preserving changes and extend morphisms uniquely from finite tables. Corresponding Lean declarations are listed in the appendix.