AI 中文总结
本文发展代数架构理论（AAT）基础，通过原子、定律和解读定义结构，提出重建定理，并涵盖粘合、诊断、传输、比较与重建，为AI生成软件变更分析提供形式化框架。
AI 中文摘要
AI生成的软件变更使得确定变更所保留的内容、局部一致性在何处无法扩展到全局、以及哪些替代方案仍然可用变得日益重要。我们从原子（Atoms）、类型化原始事实（typed primitive facts）以及定律（Laws，即对象必须满足的方程）出发，发展代数架构理论（AAT）的基础。一个解读（reading）指定了什么构成结构，以及要保留哪些操作和定律。主要重建定理将完全几何（full geometries）的范畴及其所有保结构态射与一个独立定义的局部模型范畴等价地识别，直至等价。对象在同构意义下被恢复，固定端点之间的态射被唯一恢复。该理论涉及粘合、诊断、传输、变更分类和重建。从有限原子族我们构造在操作下封闭的核心，以及带有位点和系数的几何。我们给出了Čech障碍检测全局状态存在性的条件，并通过与修复语义的比较，检测全局修复的存在性。我们比较诊断，并给出在可计算有限数据下均匀不变性的有限判据。沿精确变更的传输具有泛性质，并在精确尖拉回方块上与基变换交换。从同一方块生成的路线、有限比较图和几何的比较分解为一个可逆比较和一个幂等规范化。我们刻画了观测何时决定比较保持性，并分类兼容提升。透镜和协议语义的编码保持并反映定律，并恢复保持语义的态射。应用分类并计数保持操作的变更，并从有限表唯一扩展态射。附录中列出了相应的Lean声明。
英文摘要
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.
Comments285 pages, 4 figures. Also archived on Zenodo with the same source: https://doi.org/10.5281/zenodo.22913488
