什么是Axiom K？

Question

什么是Axiom K？

pattern-matchingprogramming-languagesagdadependent-type

43

我注意到自从HoTT之后，“Axiom K”的讨论变得更加频繁。我相信它与模式匹配有关。但我很惊讶在TAPL, ATTAPL或PFPL中都找不到相关的引用。

Axiom K是什么？
它是否被用于像SML中的ML风格模式匹配（还是只用于依赖模式匹配）？
Axiom K的适当参考资料是什么？

答案：

Axiom K是一个简单类型理论中的公理，它允许在证明等同性时使用类型的反射。它通常出现在依赖类型理论和归纳类型上，与模式匹配无关。

Axiom K用于依赖模式匹配，而不是ML风格模式匹配，ML风格模式匹配通常基于带标签的联合类型。

《Homotopy Type Theory》是Axiom K的主要参考资料。

- Steven Shaw

通常依赖模式匹配需要K，但Agda也允许您在没有K的情况下进行匹配，因此依赖模式匹配和公理K都不意味着另一个。公理K基本上是说相同术语的2个证明是相等的，消除了类型的更高群体结构。 - 盛安安

@盛安安，我一开始在第二个要点中问的是“是否必需”，后来为什么改成了“是否使用”。看起来它通常被使用，但至少在Agda中可以避免使用它。 - Steven Shaw

2

@盛安安，“消除类型的更高群体结构”——这只适用于通过HoTT的视角来看待类型吗？（或者其他TT是否具有更高的群体结构，或者我说的没有意义）？ - Steven Shaw

6

在MLTT中，更高的群体结构有些无聊，因为所有东西都只能是“refl”（虽然在没有K公理的系统中你不能正式地这样说）。 - 盛安安

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Jesper · Accepted Answer

Axiom K也被称为“证明唯一性原则”，它是关于Martin-Löf依赖类型理论中“恒等类型”的本质的公理。这种类型在简单的类型理论（如System F）中不存在（实际上也无法定义），所以这可能是您没有在提到的书籍中遇到它的原因。

恒等类型写作Id(A,x,y)或x = y，编码了x和y相等的属性（根据Curry-Howard correspondence）。有一种基本的方法来证明恒等类型，即refl : Id(A,x,x)，即证明x等于它自己的证明。

在研究他的论文中的恒等类型时，托马斯·斯特赖彻引入了一个新的恒等类型消解器，称为K（作为标准恒等类型消解器J之后字母）。它声明任何形如x = x的等式的证明p本身等于平凡证明refl。由此可知，任何两个任意方程x = y的证明p和q都是相等的，因此有另一种名称“恒等证明的唯一性”。值得注意的是，他证明这不是来自类型理论的标准规则。如果您想了解原因，我建议阅读丹·利卡塔在同伦类型理论博客上的文章，他比我解释得更好。

回答您问题的第二部分：ML风格的模式匹配与K无关，因为ML没有身份类型，因此甚至无法制定K公理。另一方面，依赖模式匹配需要K，正如Thierry Coquand在“Pattern matching with dependent types（1992）”中介绍的那样。原因是很容易通过对身份类型的构造函数refl进行模式匹配来证明K：

K : (p : x = x) -> p = refl
K refl = refl

事实上，Conor McBride在他的论文《Dependently typed functional programs and their proofs (2000)》中表明，K是依赖模式匹配真正添加到依赖类型理论中的唯一东西。

我对这个主题的兴趣在于确切地了解为什么依赖模式匹配需要K以及如何限制它，使其不再需要。结果是一篇论文和Agda中--without-K选项的新实现。基本思想是，在依赖模式匹配期间用于案例分析的统一算法不应删除形如x = x的方程，因为这样做需要K。如果您想了解更多信息，建议阅读论文（引言部分）。