什么是公理 K? [英] What is Axiom K?

问题描述

我注意到自 HoTT 以来，关于Axiom K"的讨论越来越频繁.我相信这与模式匹配有关.我很惊讶在 TAPL、ATTAPL 或 PFPL 中找不到参考.

I've noticed the discussion of "Axiom K" comes up more often since HoTT. I believe it's related to pattern matching. I'm surprised that I cannot find a reference in TAPL, ATTAPL or PFPL.

• 什么是 Axiom K?
• 它是否像 SML 一样用于 ML 样式的模式匹配(或仅用于依赖模式匹配)?
• Axiom K 的合适参考是什么?

推荐答案

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

Axiom K is also called the principle of uniqueness of identity proofs, and it is an axiom about the nature of the identity type in Martin-Löf's dependent type theory. This type doesn't exist (and in fact cannot be defined) in simpler type theories such as System F, so that is probably the reason why you haven't encountered it in the books you mention.

身份类型写为 Id(A,x,y) 或 x = y 并编码 x 和y 相等(根据 Curry-Howard 通信).有一种基本的方式来证明身份类型，那就是 refl : Id(A,x,x)，即 x 等于的证明自己.

The identity type is written as Id(A,x,y) or also x = y and encodes the property that x and y are equal (under the Curry-Howard correspondence). There is one basic way to give a proof of the identity type, and that is refl : Id(A,x,x), i.e. the proof that x is equal to itself.

在他的论文中调查身份类型时，Thomas Streicher 为他称之为 K 的身份类型(作为字母表中 J 之后的下一个字母，身份类型的标准消元).它指出任何形式 x = x 等式的证明 p 本身等于平凡证明 refl.由此推导出，any等式x = y的任意两个证明p和q是相等的，因此替代名称身份证明的唯一性".值得注意的是，他证明了这不遵循类型论的标准规则.我推荐阅读 Dan Licata 的 关于同伦类型理论的文章博客如果你想了解为什么不，他解释得比我好得多.

When investigating the identity type in his thesis, Thomas Streicher introduced a new eliminator for the identity type which he called K (as the next letter in the alphabet after J, the standard eliminator for the identity type). It states that any proof p of an equality of the form x = x is itself equal to the trivial proof refl. From this, it follows that any two proofs p and q of any equation x = y are equal, hence the alternative name "uniqueness of identity proofs". What's remarkable is that he proved that this does not follow from the standard rules of type theory. I recommend reading Dan Licata's article on the homotopy type theory blog if you want to understand why not, he explains it much better than I could.

回答您问题的第二部分:ML 样式的模式匹配与 K 无关，因为 ML 没有身份类型，因此甚至无法制定 K 公理.另一方面，正如 Thierry Coquand 在Pattern matching withdependent types (1992)"中介绍的那样，依赖模式匹配需要 K.这样做的原因是通过对标识类型的构造函数refl进行模式匹配很容易证明K:

To answer the second part of your question: ML-style pattern matching is unrelated to K, since ML doesn't have an identity type and hence cannot even formulate the K axiom. On the other hand, K is required for dependent pattern matching as introduced by Thierry Coquand in "Pattern matching with dependent types (1992)". The reason for this is that it is very easy to prove K by pattern matching on the constructor refl of the identity type:

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

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

In fact, Conor McBride showed in his thesis ("Dependently typed functional programs and their proofs (2000)") that K is the only thing that dependent pattern matching really adds to dependent type theory.

我自己对这个主题的兴趣是确切地了解为什么依赖模式匹配需要 K 以及如何限制它以便不再使用.结果是论文和的新实现--Agda 中没有 -K 选项.基本思想是，在依赖模式匹配期间用于案例分析的统一算法不应该删除 x = x 形式的方程，因为这样做需要 K.我建议你阅读 (introduction of)如果您想了解更多，请参阅论文.

My own interest in this subject is to understand exactly why dependent pattern matching requires K and how it can be restricted so it doesn't anymore. The result was a paper and a new implementation of the --without-K option in Agda. The basic idea is that the unification algorithm used for case analysis during dependent pattern matching shouldn't delete equations of the form x = x, because doing so requires K. I recommend you read the (introduction of) the paper if you want to know more.

这篇关于什么是公理 K?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！