On the strength of dependent products in the type theory of Martin-Löf
On the strength of dependent products in the type theory of Martin-Löf
复制标题
论Martin-Löf类型论中依赖积的强度
DOI：
10.1016/j.apal.2008.12.003
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Richard Garner
中科院分区：
文献类型：
--
作者：
Richard Garner
人们可以根据像 lambda 演算那样的抽象和应用运算符；或者像类型论的其他构造函数那样根据引入和消除规则来制定类型论的 Martin-L 的依赖积类型。众所周知，后者的规则至少与前者一样强：我们证明它们实际上严格更强。我们还表明，在存在恒等类型的情况下，依赖积的消除规则 - 这是最后，我们考虑类型论中的函数外延性原理，该原理断言从属乘积类型的两个元素在命题上相等，它们本身在命题上相等。
One may formulate the dependent product types of Martin-L\"of type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the other constructors of type theory. It is known that the latter rules are at least as strong as the former: we show that they are in fact strictly stronger. We also show, in the presence of the identity types, that the elimination rule for dependent products--which is a "higher-order" inference rule in the sense of Schroeder-Heister--can be reformulated in a first-order manner. Finally, we consider the principle of function extensionality in type theory, which asserts that two elements of a dependent product type which are pointwise propositionally equal, are themselves propositionally equal. We demonstrate that the usual formulation of this principle fails to verify a number of very natural propositional equalities; and suggest an alternative formulation which rectifies this deficiency.