arXiv 论文提出 Eigenius：在构造性制度上存储带类型知识
论文AI 评分 55/100arXiv cs.AI待复核
AI 聚合
本条为 AI 依据下方公开信源自动整理生成的摘要，不构成转载，可能存在偏差，请以原文为准。整理者：贝果科技 AI 资讯助手。
一篇提交至 arXiv 的论文给出 Eigenius 的理论，用于在构造性制度之上存储带类型的知识。其内核采用依赖类型理论，包含累积宇宙、命题的非直谓宇宙、归纳族与外延同一类型。证明无关性被设为带显式见证的公理，而非转换规则，因此同一命题的不同证明可证相等却仍是不同项。定义等价被刻画为正交重写系统下的可连接性，该系统合流、在类型构造子上单射，并可由无类型测试判定；另有独立的包含判断处理宇宙累积、余域协变函数类型与声明的类包含。作者用集合论模型证明一致性，在内核命题上建立辩护逻辑以追踪证据与支持，把环境组织为制度使存储扩展成为签名态射、外部判定经余态射进入，并给出含记录、类与细化的带类型知识图理论，还证明了转换、按值求值归一化与双向类型检查相对于终止性的正确性。论文附有 Lean 4 形式化。
全文梳理
AI 摘要依据下方信源原文自动整理，非原文转载内核类型理论与证明记录
论文的核心出发点是：面向数学或程序验证的类型理论只要求命题成立，转换中的证明无关性会在内核层面抹去一个断言是如何被确立的；而持久知识存储必须保留谁确立了断言、经由哪条推导或哪个外部工具、在哪些假设之下。Eigenius 的内核因此采用依赖类型理论，包含累积宇宙、命题的非直谓宇宙、归纳族与内涵同一类型。关键设计是把证明无关性设为带显式见证的公理，而不是转换规则，于是同一命题的证明可证相等，却仍作为不同项存在，来源信息得以留在项中。
等价判定与包含判断
在定义等价上，论文采用正交重写系统下的可连接性来刻画，该系统具备合流性、在类型构造子上单射，并可由一个无类型测试来判定。宇宙累积、余域协变函数类型以及声明的类包含，则由一个独立的包含判断处理，与定义等价分开。作者通过集合论模型证明了一致性，并在内核命题之上发展辩护逻辑，用来追踪证据与支持关系。
制度组织与知识图
环境被组织为一个制度，存储的扩展对应签名态射，外部判定则通过余态射进入系统。在此基础上，论文给出带类型的知识图理论，包含记录、类与细化。论文还证明了转换、按值求值归一化与双向类型检查相对于终止性的正确性，并附有 Lean 4 形式化伴随该卷。
为什么值得看
关注知识表示与形式化验证交叉方向的研究者，可从中看到把证明来源与假设纳入类型化存储的一种内核设计。
论文
信源1 家
关键事实
相关 · 论文
本页内容由 AI 自动聚合公开信源生成，仅供了解行业动态参考，不构成任何投资或决策建议。如需引用请以原文出处为准。