什么是Axiom K？

Question

什么是Axiom K？

Ste*_*haw 31 programming-languages pattern-matching agda dependent-type

我注意到自从HoTT以来,"Axiom K"的讨论经常出现.我相信它与模式匹配有关.我很惊讶我在TAPL,ATTAPL或PFPL中找不到参考.

什么是Axiom K？
它是否用于ML样式的模式匹配,如SML(或只是依赖模式匹配)？
什么是Axiom K的适当参考？

Answer 1

Axiom K也被称为身份证明的唯一性原则,它是关于Martin-Löf依赖型理论中身份类型本质的公理.在System F这样的简单类型理论中,这种类型不存在(事实上也无法定义),所以这可能就是你没有在你提到的书中遇到它的原因.

身份类型被写为Id(A,x,y)或同时x = y编码x并且y相等的属性(在Curry-Howard对应下).有一种基本方法可以证明身份类型refl : Id(A,x,x),即证明x与自身相等.

在调查他的论文中的身份类型时,Thomas Streicher为身份类型引入了一个新的消除器,他称之为K(作为J之后的字母表中的下一个字母,身份类型的标准消除器).它指出,任何p形式x = x相等的证据本身都等同于琐碎的证据refl.由此,可以得出任何两个证明p和q的任何方程x = y是相等的,因此替代名称"同一性样张唯一性".什么是显着的是,他证明了这并没有从类型理论的标准规则可循.我建议阅读Dan Licata 关于同伦类型理论博客的文章,如果你想理解为什么不这样做,他会比我更好地解释它.

回答你问题的第二部分:ML样式模式匹配与K无关,因为ML没有身份类型,因此甚至不能形成K公理.另一方面,由Thierry Coquand在"与依赖类型的模式匹配(1992)"中引入的依赖模式匹配需要K. 这样做的原因是通过refl身份类型的构造函数上的模式匹配来证明K非常容易:

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

Run Code Online (Sandbox Code Playgroud)

事实上,Conor McBride在他的论文("依赖类型化的功能程序及其证明(2000)")中表明,K是唯一依赖模式匹配真正增加依赖类型理论的东西.

我自己对这个主题感兴趣的是要明确为什么依赖模式匹配需要K以及如何限制它以便它不再存在.结果是一篇论文和--without-KAgda 中的选项的新实现.基本思想是在依赖模式匹配期间用于案例分析的统一算法不应该删除表单的方程式x = x,因为这样做需要K.如果你想了解更多,我建议你阅读(介绍)论文.

原因是Id不是一个归纳定义的数据类型系列,而是一个归纳定义的数据类型系列.这意味着如果`x`和`y`是不同的变量,原则上你只能匹配`Id xy`的值.这会非常烦人,所以Agda使用统一来允许在更多情况下匹配`refl`:它统一了索引`x; 带有索引`x',x'的构造函数的数据类型的x`.在一步之后,这导致'x = x`,但这正是我们需要K再次摆脱这个等式的地方(阅读我的论文了解更长的版本). (4认同)
如果`Id {A:Set a}:a - > a - > Set _`是根据唯一的构造函数`refl:forall {x:A}定义的.Id xx`,然后将`Id xx`类型的值与`refl`匹配会出现什么问题？ (2认同)
值得指出的是，Coq 有一些它称之为（在我看来是正确的）依赖模式匹配的东西，但它是一种较弱的形式，不需要公理 K。实际上，我很惊讶听到 Coquand 的原始论文需要 Axiom K。我会看看为我自己，但我在我的手机上，我只能找到一个 #!*%@$! .ps 文件... (2认同)

归档时间：	9 年，4 月前
查看次数：	1617 次
最近记录：	7 年，9 月前