如何解决库克的咖喱霍华德对应
通过Curry Howard对应关系,所有定理和引理都是类型,证明对象是值。例如:
Theorem test: 0 <= 0.
Proof.
omega. Qed.
当我这样做时,请检查测试。 Coq的输出是:
test
: 0 <= 0
但是当我检查“ nat-> Prop。这意味着(0
解决方法
test : 0 <= 0
和0 <= 0 : Prop
,如您所说。在Curry-Howard对应关系的术语中,0 <= 0
是类型/定理陈述,test
是该类型/定理的证明。
此示例中不涉及任何子类型。子类型化是两种类型之间的关系。如果Cat <: Animal
(猫是动物的子类型),则意味着猫类型的所有对象也都是动物类型的:x : Cat
表示x : Animal
。 >
Coq在类型Universe之间具有一种相对简单的子类型形式。最简单的示例是Prop
是Type
的子类型。您可以使用Check
来确认0 <= 0 : Prop
以及0 <= 0 : Type
来查看此内容。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。