DEKL 2.0: Trace-Indexed Knowledge Evolution in Dependent Type Theory

DEKL 2.0 是一种面向依赖类型理论的迹索引知识演化框架，旨在形式化建模随执行历史动态变化的知识状态。该框架将有限与无限迹作为计算宇宙中的一等公民，将知识解释为有限迹范畴上的预层（presheaf），并在命题层采用带不动点支持的范畴语义进行推理。核心思想在于：证明演算本身在结构规则下保持单调性，而非单调行为源于迹扩展所引发的语义变化——具体体现为预层限制映射的非满射性。论文建立了迹与可达性证明之间的双向对应关系，严格证明了迹完备性，并给出了非单调性的语义刻画定理：知识系统的非单调性当且仅当存在某个迹扩展对应的限制映射不满足满射性。进一步，提出基于迁移系统生成自由范畴的语义模型，统一整合可执行迹、类型化证据与知识修正机制。框架在运行时监控、安全协议中的凭证撤销及基于迹条件的可废止默认推理等场景中展现出良好建模能力，其元理论包括可靠性、一致性、规范化及主项约简等关键性质。DEKL 2.0 为动态系统中的知识演化提供了兼具逻辑严谨性与计算可实现性的依赖类型基础。