Строить иерархию классов в Coq? - PullRequest
Новая
       46

Строить иерархию классов в Coq?

9 голосов
/ 03 ноября 2011

Я могу наивно построить иерархию алгебраических структур в Coq, используя классы типов. У меня возникли проблемы с поиском ресурсов по синтаксису и семантике Coq для классов типов. Тем не менее, я считаю, что правильная реализация полугрупп, моноидов и коммутативных моноидов является следующей: 

Class Semigroup {A : Type} (op : A -> A -> A) : Type := {
  op_associative : forall x y z : A, op x (op y z) = op (op x y) z
}.

Class Monoid `(M : Semigroup) (id : A) : Type := {
  id_ident_left  : forall x : A, op id x = x;
  id_ident_right : forall x : A, op x id = x
}.  

Class AbelianMonoid `(M : Monoid) : Type := {
  op_commutative : forall x y : A, op x y = op y x
}.

Если я правильно понимаю, дополнительные параметры (например, элемент идентичности моноида) можно добавить, сначала объявив Monoid экземпляр Semigroup, а затем параметризовав id : A. Однако в записи, построенной для AbelianMonoid.

, происходит нечто странное. 
< Print Monoid.
    Record Monoid (A : Type) (op : A -> A -> A) (M : Semigroup op) 
    (id : A) : Type := Build_Monoid
    { id_ident_left : forall x : A, op id x = x;
      id_ident_right : forall x : A, op x id = x }

< Print AbelianMonoid.
    Record AbelianMonoid (A : Type) (op : A -> A -> A) 
    (M0 : Semigroup op) (id0 : A) (M : Monoid M0 id0) : 
    Type := Build_AbelianMonoid
      { op_commutative : forall x y : A, op x y = op y x }

Это произошло, когда я пытался создать класс для полугрупп. Я думал, что следующий синтаксис был правильным: 

Class Semiring `(P : AbelianMonoid) `(M : Monoid) := {
    ...
}.

Однако я не смог однозначно определить правильные операторы и элементы идентичности. Печать записей выявила проблемы, изложенные выше. Поэтому у меня два вопроса: во-первых, как правильно объявить класс Monoid; во-вторых, как устранить неоднозначность функций в суперклассах?

Что мне действительно нравится, так это хорошие ресурсы, которые четко объясняют классы типов Coq без устаревшего синтаксиса. Например, я думал, что книга Хаттона объясняет классы типов в Хаскеле.

1 Ответ

5 голосов
/ 03 ноября 2011

Ссылка:

Канонические ссылки для классов типов в Coq - за пределами руководства - этой статьи и тезиса (на французском языке) Матье Sozeau . Менее канонических ссылок (с разных точек зрения) на уровне исследований в недавней работе , и в моей диссертации . Вам также следует потратить некоторое время на канал #coq на Freenode и подписаться на список рассылки .

Ваша проблема:

Синтаксическая проблема не в Classes как таковом, а в том, что максимально вставлено неявных аргументов . Типы Monoid и AbelianMonoid имеют в своем определении (неявные) параметрические аргументы, которые в этом порядке представляют собой тип домена, операцию и идентификацию - как проиндексировано зависимым продуктом, который вы увидеть полностью развернутым при печати этих типов записей. Они заполняются автоматически, когда вы упоминаете зависимый продукт без его аргументов в том положении, в котором они могут понадобиться.

Действительно, неявное разрешение аргументов автоматически вставит требуемые параметрические аргументы, которые будут идентичны (для обоих продуктов, которые зависят от них: P и M), если они будут оставлены на его собственные устройства. Вам просто нужно указать ограничения между этими идентификаторами, указав переменные для различных идентификаторов, различающихся при необходимости: 

Class Semiring A mul add `(P : AbelianMonoid A mul) `(M : Monoid A add) := {
}.

Результат: 

> Print Semiring.
Record Semiring (A : Type) (mul add : A -> A -> A) 
(M0 : Semigroup mul) (id0 : A) (M : Monoid M0 id0) 
(P : AbelianMonoid M) (M1 : Semigroup add) (id1 : A) 
(M : Monoid M1 id1) : Type := Build_Semiring {  }

For Semiring: Arguments M0, id0, M, M1, id1 are implicit and maximally
              inserted
For Semiring: Argument scopes are [type_scope _ _ _ _ _ _ _ _ _]
For Build_Semiring: Argument scopes are [type_scope _ _ _ _ _ _ _ _ _]

Обратите внимание, что тождества абелевого моноида и моноида на этот раз различны. Это хорошее упражнение (даже если оно не имеет большого математического смысла) - научиться писать тип записи (он же Класс), который вы хотели бы иметь, если бы у вас был один и тот же элемент идентичности для аддитивной и мультипликативной структур.

...