将Axioms添加到COQ通常会使证明更容易,但也会引入一些副作用.例如,通过使用经典公理,人们离开了直觉主义领域,并且证明不再是可计算的.我的问题是,使用功能扩展性公理的缺点是什么？
对我来说,使用功能扩展性的缺点与使用Coq中的任何其他公理或多或少相同:它增加了系统的复杂性以及我们需要信任的程度.虽然理论上我们很好地理解了使用这些众所周知的公理的逻辑结果(例如,必须避免哪些公理组合以确保一致性),但实际上我们有时会措手不及.例如,它是最近发现的命题外延性公理与勒柯克在8.4版本不一致的理论,即使它被广泛认为是一致的.这个看似自然的公理简单地说等价命题是平等的,并且在许多Coq开发中被采用:
Axiom propositional_extensionality :
forall P Q : Prop, (P <-> Q) -> P = Q.
在上面的答案中,Andrej Bauer认为这种脆弱性可能与这些没有与之相关的计算规则的公理有关,这与Coq的其他理论相反.
除了这个一般性评论之外,我听过有人说默认具有功能扩展性可能是不可取的,因为它将函数等同于非常不同的计算行为(例如,冒泡排序和快速排序),并且我们可能想要推断这些差异.我个人并没有购买这个论点,因为Coq已经将很多不同的值等同于,例如0和47^1729 - 47 mod 1729.我不知道不想承担功能扩展性的其他原因.