Блог

Главная - Вопросы по программированию - Переписка Карри Ховарда в Coq

Переписка Карри Ховарда в Coq

#coq #curry-howard

#coq #карри-Говард

Вопрос:

Согласно соответствию Карри Говарда, все теоремы и леммы являются типами, а объекты доказательства — значениями. В качестве примера:

 Theorem test:  0 <= 0.
Proof.
  omega. Qed.

Когда я это сделаю, проверьте test. Результат Coq является:

 test
     : 0 <= 0

Но когда я проверяю тип «<=», это nat -> nat -> Prop. Это означает, что (0 <= 0) имеет тип Prop. Означает ли это, что тип ‘test’ является подтипом Prop? В общем, являются ли идентификаторы теоремы и леммы подтипами Prop?

Ответ №1:

test : 0 <= 0 и 0 <= 0 : Prop , как вы сказали. В терминологии соответствия Карри-Говарда, 0 <= 0 является утверждением типа / теоремы, и test является значением этого типа / доказательством этой теоремы.

В этом примере нет никакого подтипа, задействованного. Подтипирование — это взаимосвязь между двумя типами; когда Cat <: Animal (cat является подтипом animal), это означает, что все объекты типа cat также относятся к типу animal: x : Cat подразумевает x : Animal .

Coq имеет одну относительно простую форму подтипирования, между универсалиями типов. Простейшим примером является то, что Prop является подтипом Type . Вы можете увидеть это, используя Check для подтверждения этого 0 <= 0 : Prop а также 0 <= 0 : Type .

Комментарии:

1. ‘0 <= 0 : Prop’ : здесь и LHS, и RHS являются типами, не так ли? Итак, подтипирование?

2. Они оба являются типами, но связь между ними «имеет тип», а не подтипирование. Они кажутся действительно похожими (и мы используем похожие обозначения), но ведут себя по-разному.

3. Если я прав, для отношения типа has требуется значение типа в LHS и типа в RHS, как в (n: nat). В приведенном выше (0 <= 0) есть ‘значение’, которое имеет тип ‘Prop’; также это тип? Итак, тип имеет тип ‘Prop’? Я прав?

4. Вы правы в том, что некоторые типы, такие как 0 <= 0 , True , False p / q или x = y , имеют тип Prop , но не все типы имеют тип Prop , для начала Prop сам который имеет тип Prop : Type , но также nat : Set ( Set является псевдонимом для конкретного случая Type ).