将信念演化与类型理论结合，构建可验证的动态知识推理系统
ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
- 用轨迹索引类型建模事件驱动的执行过程，支持精确归纳推理
- 证明信念修正满足全部8条AGM公理，且在Coq中完成34个完整证明
- 揭示路径依赖信念演化与函子一致性间的根本矛盾，适合逻辑与认知计算研究者
我们提出ZX-Calculus（知识演化演算），作为马丁-洛夫依赖类型理论（MLTT）的保守扩展，融合轨迹索引类型、预层非单调语义与构造性AGM信念修正。配套提供Coq形式化（34个完整证明；核心结果无外延假设）。(I) 轨迹类型：FinTrace(s0,sn) 是有类型执行轨迹的归纳族，与Star(Step)同构但不判别相等；TraceElim 显式暴露事件标签e:Event，支持事件驱动归纳。证明了轨迹可达性对应、确定性重放及通过可还原性候选与传递引理的范式框架（RC-elim待定；其余核心结果均经Coq验证）。(II) 预层语义：轨迹索引命题是自由轨迹偏序范畴Tf上的反变预层。分离定理（显式反例）区分了证明论单调性与语义非单调性。项模型为初始CwF（语法泛性，非经典完备性）。(III) AGM信念修正：给出构造性部分交收缩算法，并验证满足(C1)-(C4)。所有八条AGM公理（R1)-(R8)均为定理。R7与R8的证明使用析取深入度引理，其构造性推导自成体系。(IV) 整合：B^AGM 不满足序列修正的函子复合律BP-comp（显式反例，Coq验证）。引入单步修正系统（SSRS），证明B^AGM 是有效SSRS（Coq验证），并表明其足以支撑轨迹态射、收缩刻画与修正见证。BP-comp失效揭示路径依赖信念修正与函子一致性间存在未被识别的根本张力。
原文摘要 · Abstract (English)
We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision. A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results). (I) Trace types. FinTrace(s0,sn) is an inductive family of typed execution traces. FinTrace and Star(Step) are isomorphic as path types but not judgementally equal; TraceElim exposes the event label e:Event explicitly, giving a more ergonomic interface for event-driven induction. We prove the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework via reducibility candidates with a Transport Lemma (RC-elim deferred; all other Core results are Coq-verified). (II) Sheaf semantics. Trace-indexed propositions are contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem (explicit countermodel) distinguishes proof-theoretic monotonicity from semantic non-monotonicity. The term model is an initial CwF (syntactic universal property, not classical completeness). (III) AGM belief revision. We give an explicit constructive partial meet contraction algorithm verified against (C1)-(C4). All eight AGM postulates (R1)-(R8) are theorems. Proofs of R7 and R8 use the Disjunctive Entrenchment Lemma, given a self-contained constructive derivation. (IV) Integration. B^AGM fails the sheaf composition law BP-comp for sequential revision (explicit countermodel, Coq-verified). We introduce Single-Step Revision Systems (SSRS), prove B^AGM is a valid SSRS (Coq-verified), and show this suffices for trace morphisms, retraction characterisation, and revision witnesses. The BP-comp failure reveals a fundamental tension between path-dependent belief revision and functor consistency, not previously identified.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。