В первой части статьи про язык Arend мы рассматривали простейшие индуктивные типы, рекурсивные функции, классы и множества.

2. Сортировка списков в Arend

2.1 Упорядоченные списки в Arend

Определим тип упорядоченных списков как пару, состоящую из списка и доказательства его упорядоченности. Как мы уже говорили, в Arend зависимые пары определяются при помощи ключевого слова \Sigma. Определение типа Sorted дадим через сопоставление с образцом, вдохновившись определением из уже упомянутой статьи про упорядоченные списки.

\func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l)

\data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs
 | nil => nilSorted
 | :-: x nil => singletonSorted
 | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))

Обратите внимание: Arend сумел автоматически вывести, что тип Sorted содержится во вселенной \Prop. Это произошло потому, что все три образца в определении Sorted являются взаимно исключающими, а конструктор consSorted имеет два параметра, оба из которых принадлежат \Prop.
Докажем какое-нибудь очевидное свойство предиката Sorted, скажем, что хвост упорядоченного списка сам является упорядоченным списком (это свойство пригодится нам в дальнейшем).

\func tail-sorted {O : LinearOrder.Dec} (x : O) (xs : List O) (A : Sorted (x :-: xs)) : Sorted xs \elim xs, A
  | nil, _ => nilSorted
  | :-: _ _, consSorted _ xs-sorted => xs-sorted

В реализации tail-sorted мы использовали сопоставление с образцом одновременно по списку xs и предикату Sorted, кроме того, мы использовали символ пропуска «_», который можно подставлять вместо неиспользуемых переменных.

Можно спросить, возможно ли в Arend доказать свойство упорядоченных списков, упомянутое в разделе 1.3 как пример факта, который нельзя доказать в Agda без аннотаций несущественности. Напомним, что данное свойство утверждает, что для доказательства равенства упорядоченных списков, определенных через зависимые пары, достаточно проверить равенство первых компонент пар.

Утверждается, что в Arend это свойство легко получается как следствие уже упомянутой выше конструкции inProp и свойства экстенсиональности для зависимых пар SigmaExt.

\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 
  => SigmaPropExt Sorted l1 l2 P

Свойство SigmaPropExt доказано в модуле Paths стандартной библиотеки, там же доказываются многие другие факты из второй главы книги HoTT, в том числе свойство функциональной экстенсиональности.

Оператор .n используется в Arend для обращения к проектору сигма-типа с номером n (в нашем случае сигма-типом является SortedList A, а выражение l1.1 означает первую компоненту этого типа — выражение типа List A).

2.2 Реализация свойства «быть перестановкой»

Попробуем теперь реализовать функцию сортировки списка на Arend. Естественно, мы хотим иметь не простую реализацию алгоритма сортировки, а реализацию вместе с доказательством некоторых свойств.

Ясно, что у этого алгоритма должно быть по крайней мере 2 свойства:
 1. Результат работы алгоритма должен быть упорядоченным списком.
 2. Получившийся список должен являться перестановкой исходного списка.

Попробуем для начала реализовать на Arend свойство списков «быть перестановкой». Для этого мы адаптируем для Arend определение, взятое отсюда.

\truncated \data InsertSpec {A : \Set} (xs : List A) (a : A) (ys : List A) : \Prop \elim xs, ys
  | xs, :-: y ys => insertedHere (a = y) (xs = ys)
  | :-: x xs, :-: y ys => insertedThere (x = y) (InsertSpec xs a ys)

\truncated \data Perm {A : \Set} (xs ys : List A) : \Prop
  | permInsert (xs' ys' : List A) (a : A) (Perm xs' ys') (InsertSpec xs' a xs) (InsertSpec ys' a ys)
  | permTrivial (xs = ys)

Введенный нами предикат InsertSpec имеет следующий интуитивный смысл: InsertSpec xs a ys в точности означает, что список ys является результатом вставки элемента a внутрь списка xs (на любую позицию). Таким образом, InsertSpec можно воспринимать как спецификацию функции вставки.

Ясно, что тип данных Perm действительно определяет отношение «быть перестановкой»: конструктор permInsert в точности утверждает, что xs и ys являются перестановкой друг друга, если xs и ys получаются при помощи вставки одного и того же элемента a в некоторые списки xs’ и ys’ меньшей длины, уже являющиеся перестановками друг друга.

Для выбранного нами определения свойства «быть перестановкой» несложно проверить свойство симметричности.

\func Perm-symmetric {A : \Set} {xs ys : List A} (P : Perm xs ys) : Perm ys xs \elim P
  | permTrivial xs=ys => permTrivial (inv xs=ys)
  | permInsert perm-xs'-ys' xs-spec ys-spec => permInsert (Perm-symmetric perm-xs'-ys') ys-spec xs-spec

Свойство транзитивности также выполнено для Perm, однако его проверка существенно сложнее. Так как данное свойство не играет никакой роли в реализации нашего алгоритма сортировки, мы оставляем его проверку читателю в качестве упражнения.

\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}

2.3 Изменение гомотопических уровней при сопоставлении с образцом

Попробуем теперь реализовать функцию, вставляющую элемент в упорядоченный список так, чтобы получившийся список остался упорядоченным. Начнем со следующей наивной реализации.

\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs
  | nil => y :-: nil
  | :-: x xs' => \case LinearOrder.trichotomy x y \with {
     | byLeft x=y => x :-: insert xs' y
     | byRight (byLeft x<y) => x :-: insert xs' y
     | byRight (byRight y<x) => y :-: x :-: xs'
 }

Конструкция \case позволяет производить сопоставление с образцом произвольного выражения (\elim может быть использована только на самом верхнем уровне определения функции и только для ее параметров). Если попросить Arend проверить тип insert, то будет выведено следующее сообщение об ошибке.

[ERROR] Data type '||' is truncated to the universe \Prop
      which does not fit in the universe of the eliminator type: List O.E
   In: | byLeft x-leq-y => x :-: insert xs' y
   While processing: insert

Проблема заключается в том, что в классе LinearOrder.Dec определение trichotomy даётся при помощи оператора ||, который, в свою очередь, определен при помощи пропозиционального усечения. Как уже было сказано, для типов, принадлежащих вселенной \Prop, сопоставление с образцом в Arend разрешается только в том случае, если тип результирующего выражения сам является утверждением (у функции выше результат имеет тип List O.E, а данный тип является множеством).

Можно ли как-то обойти эту проблему? Самый простой способ решения заключается в том, чтобы изменить определение свойства трихотомии. Рассмотрим следующее определение трихотомии, использующее неусеченный тип Or вместо усеченного ||:

\func set-trichotomy {A : StrictPoset} (x y : A) => ((x = y) `Or` (x < y)) `Or` (y < x)

Отличается ли это определение чем-то от исходного определения trichotomy через ||? Почему вообще мы использовали пропозиционально усеченный тип, если это только усложняет нам жизнь и мешает использовать сопоставление с образцом?

Попробуем ответить для начала на первый вопрос: для строгих порядков StrictPoset разницы между trichotomy и set-trichotomy на самом деле нет совсем. Заметим, что тип set-trichotomy является утверждением. Данный факт вытекает из того, что все три альтернативы в определении трихотомии взаимно исключают друг друга благодаря аксиомам порядка, а каждый из трех типов x = y, x < y, y < x сам по себе является утверждением (x = y является утверждением, так как при определении класса BaseSet мы потребовали, чтобы носитель E являлся множеством!).

\func set-trichotomy-isProp {A : StrictPoset} (x y : A) (l1 l2 : set-trichotomy x y): l1 = l2 \elim l1, l2
  | inl (inl l1), inl (inl l2) => pmap (\lam z => inl (inl z)) (Path.inProp l1 l2)
  | inl (inr l1), inl (inr l2) => pmap (\lam z => inl (inr z)) (Path.inProp l1 l2)
  | inr l1,       inr l2       => pmap inr (Path.inProp l1 l2)
  | inl (inl l1), inl (inr l2) => absurd (lt-eq-false l1 l2)
  | inl (inr l1), inl (inl l2) => absurd (lt-eq-false l2 l1)
  | inl (inl l1), inr l2       => absurd (lt-eq-false (inv l1) l2)
  | inr l1,       inl (inl l2) => absurd (lt-eq-false (inv l2) l1)
  | inl (inr l1), inr l2       => absurd (lt-lt-false l1 l2)
  | inr l1,       inl (inr l2) => absurd (lt-lt-false l2 l1)
  \where {
     \func lt-eq-false {A : StrictPoset} {x y : A} (l1 : x = y) (l2 : x < y) : Empty =>
        A.<-irreflexive x (transport (x <) (inv l1) l2)

     \func lt-lt-false {A : StrictPoset} {x y : A} (l1 : x < y) (l2 : y < x) : Empty =>
        A.<-irreflexive x (A.<-transitive _ _ _ l1 l2)
 }

В листинге выше absurd — обозначение для принципа ex falso quodlibet, который определяется в модуле Logic. Так как тип Empty не имеет конструкторов в определении (см. раздел 1.2), не приходится перебирать случаи и в определении absurd:

\func absurd {A : \Type} (x : Empty) : A

Так как теперь мы знаем, что set-trichotomy является утверждением, мы можем вывести свойство set-trichotomy из обычного свойства trichotomy разрешимых порядков. Для этого мы можем воспользоваться конструкцией \return \level, сообщающей тайпчекеру Arend, что в данном месте сопоставление с образцом является разрешенной операцией (при этом нам приходится предъявить доказательство того факта, что результат функции set-trichotomy-property является утверждением).

\func set-trichotomy-property {A : LinearOrder.Dec} (x y : A) : set-trichotomy x y =>
  \case A.trichotomy x y \return \level (set-trichotomy x y) (set-trichotomy-isProp x y) \with {
     | byLeft x=y => inl (inl x=y)
     | byRight (byLeft x<y) => inl (inr x<y)
     | byRight (byRight y<x) => inr (y<x)
 }

Попробуем теперь ответить на второй вопрос, а именно почему при формулировке свойств математических объектов предпочтительнее использовать не обычные, а пропозиционально усеченные конструкции. Рассмотрим для этого фрагмент определения нестрогих линейных порядков (полные определения Lattice и TotalOrder можно найти в модуле LinearOrder):

\class TotalOrder \extends Lattice {
  | totality (x y : E) : x <= y || y <= x
}

Попробуем пофантазировать теперь, как изменился бы смысл класса TotalOrder в том случае, если бы мы написали определение поля totality через неусеченную конструкцию Or.

\class BadTotalOrder \extends Lattice {
  | badTotality (x y : E) : (x <= y) `Or` (y <= x)
}

В данном случае тип (x <= y) `Or` (y <= x) уже не является утверждением, т.к. в случае равных значений x и y обе альтернативы в определении badTotality могут реализовываться, а выбор левой или правой ветви при доказательстве badTotality абсолютно произволен и остаётся на усмотрение пользователя — нет никакой причины предпочесть один конструктор Or другому.

Теперь понятно, в чём заключается отличие TotalOrder от BadTotalOrder. Два упорядоченных множества O1 O2: TotalOrder равны всегда, когда можно доказать равенство множеств O1.E, O2.E и заданных на них порядков O1.<, O2.< (это является желаемым свойством). С другой стороны, для O1 O2: BadTotalOrder доказать равенство O1 и O2 можно только в тех случаях, когда вдобавок для всех элементов x из E имеет место равенство O1.badTotality x x и O2.badTotality x x.

Таким образом, получается, что класс BadTotalOrder интуитивно уже нужно рассматривать не как «линейно упорядоченное множество», а как «линейно упорядоченное множество вместе с выбором для каждого элемента x поля E левой или правой ветви Or в реализации badTotality x x».

2.4 Алгоритм сортировки

Приступим теперь к реализации алгоритма сортировки. Попробуем исправить наивную реализацию функции insert из прошлого раздела при помощи доказанного свойства set-trichotomy-property (при этом благодаря более удачной расстановке скобок в определении set-trichotomy у нас сократилось количество рассматриваемых случаев).

\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs
  | nil => y :-: nil
  | :-: x xs' => \case set-trichotomy-property x y \with {
     | inr y<x => y :-: x :-: xs'
     | inl x<=y => x :-: insert xs' y
 }

Попробуем теперь реализовать аналог данного определения для упорядоченных списков. Мы воспользуемся специальной конструкцией \let … \in, позволяющей добавить в контекст новые локальные переменные.

\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : SortedList O \elim xs
  | (nil, _) => (y :-: nil, singletonSorted)
  | (:-: x xs', xs-sorted) => \case set-trichotomy-property x y \with {
     | inr y<x => (y :-: x :-: xs', consSorted (byRight y<x) xs-sorted)
     | inl x<=y => \let (result, result-sorted) => insert (xs', tail-sorted x xs' xs-sorted) y
                   \in (x :-: result, {?})

Мы оставили в доказательстве незаконченный фрагмент (обозначенный выражением {?}) в том месте, где нужно показать, что список x :-: result упорядочен. Хотя в контексте и имеется доказательство упорядоченности списка result, нам остаётся проверить, что x не превосходит значения первого элемента списка result, что не так уж и легко следует из имеющихся в контексте посылок (чтобы увидеть все посылки в текущей цели — так мы называем реализуемую в настоящий момент ветвь вычислений — нужно запросить проверку типов у функции insert).

Оказывается, что insert куда проще реализовать, если мы будем доказывать упорядоченность результирующего списка параллельно с доказательством спецификации insert. Изменим сигнатуру insert и впишем доказательства этой спецификации в простейших случаях:

\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : 
  \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs
  | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp)
  | (:-: x xs', xs-sorted) => \case set-trichotomy-property x y \with {
     | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp)
     | inl x<=y =>
        \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y
        \in ((x :-: result, {?}), insertedThere idp result-spec)

Для единственного оставленного без доказательства фрагмента Arend выведет следующее значение контекста:

Expected type: Sorted (x :-: (insert (\this, tail-sorted x \this \this) \this).1.1)
   Context:
      result-sorted : Sorted (insert (\this, tail-sorted \this \this \this) \this).1.1
      xs-sorted : Sorted (x :-: xs')
      x : O
      x<=y : Or (x = y) (O.< x y)
      O : Dec
      result : List O
      y : O
      xs' : List O
      result-spec : InsertSpec xs' y (insert (xs', tail-sorted \this xs' \this) y).1.1

Для завершения доказательства нам придётся использовать в полную силу возможности оператора \case: мы применим сопоставление с образцом по 5 различным переменным, а так как типы одних переменных могут зависеть от значений других переменных, мы воспользуемся зависимым сопоставлением с образцом (dependent pattern matching).

Конструкция с двоеточием явно указывает, как тип одних переменных, по которым ведется сопоставление, зависит от значения других переменных (таким образом, в тип переменных xs-sorted, result-spec и result-sorted в каждом из пунктов \case вместо переменных xs' и result будут подставлены соответствующие образцы).

Конструкция \return связывает переменные, по которым ведется сопоставление с образцом, с типом ожидаемого результата. Иными словами, в текущей цели в каждом из пунктов \case вместо переменной result будет подставлен соответствующий образец. Без этой конструкции такая замена не осуществлялась бы, и цель у всех пунктов \case совпадала бы с целью на месте самого \case-выражения.

\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) :
  \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs
   | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp)
   | (:-: x xs', xs-sorted) => \case set-trichotomy-property x y \with {
      | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp)
      | inl x<=y =>
          \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y
          \in ((x :-: result,
            \case result \as result, xs' \as xs', xs-sorted : Sorted (x :-: xs'),
                 result-spec : InsertSpec xs' y result, result-sorted : Sorted result
            \return Sorted (x :-: result) \with {
             | nil, _, _, _, _ => singletonSorted
             | :-: r rs, _, _, insertedHere y=r _, result-sorted =>
               consSorted (transport (\lam z => (x = z) || (x < z)) y=r (Or-to-|| x<=y)) result-sorted
             | :-: r rs, :-: x' _, consSorted x<=x' _, insertedThere x2=r _, result-sorted =>
               consSorted (transport (\lam z => (x = z) || (x < z)) x2=r x<=x') result-sorted
           }), insertedThere idp result-spec)

В приведенном выше блоке кода дополнительного комментария заслуживают сложные первые аргументы конструктора consSorted в двух последних пунктах сопоставления с образцом. Чтобы разобраться, что означают оба этих выражения, заменим их на выражение {?} и попросим тайпчекер Arend определить цели на обеих позициях.

Можно видеть, что и там, и там текущей целью является тип (x = r) || O.< x r. При этом в контексте первой цели присутствуют посылки

x<=y : Or (x = y) (O.< x y) 
y=r : y = r

а в контексте второй — посылки

x<=x' : (x = x') || O.< x x'
x2=r : x' = r.

Интуитивно ясно: чтобы доказать первую цель, достаточно подставить в верное утверждение Or (x = y) (O.< x y) вместо переменной y переменную r, а затем перейти к пропозиционально усеченному типу || при помощи определенной в разделе 1.3 функции Or-to-||. Чтобы доказать вторую цель, достаточно подставить в (x = x') || O.< x x' вместо переменной x' переменную r.

Для формализации описанной операции подстановки выражений в стандартной библиотеке Arend существует специальная функция transport. Рассмотрим ее сигнатуру:

\func transport {A : \Type} (B : A -> \Type) {a a' : A} (p : a = a') (b : B a) : B a'

В нашем случае вместо переменной A нужно подставить тип O.E (его можно явно не указывать, если указаны остальные аргументы transport), а вместо B— выражение \lam (z : O) => (x = z) || (x < z).

Реализация алгоритма сортировки вставками вместе со спецификацией уже не вызывает особых трудностей: для того чтобы отсортировать список x :-: xs', мы сначала сортируем хвост списка xs' при помощи рекурсивного вызова insertSort, а затем вставляем внутрь этого списка элемент x с сохранением порядка при помощи обращения к уже реализованной функции insert.

\func insertSort {O : LinearOrder.Dec} (xs : List O) : 
  \Sigma (result : SortedList O) (Perm xs result.1) \elim xs
  | nil => ((nil, nilSorted), permTrivial idp)
  | :-: x xs' => \let | (ys, perm-xs'-ys) => insertSort xs'    
                      | (zs, zs-spec) => insert ys x
                  \in (zs, permInsert perm-xs'-ys (insertedHere idp idp) zs-spec)

Мы выполнили поставленную изначально цель и реализовали сортировку списков на Arend. Весь Arend-код, приведенный в настоящем параграфе, можно скачать одним файлом отсюда.

Можно было бы спросить, как пришлось бы изменить реализацию функции insert, если бы вместо строгих порядков LinearOrder.Dec мы использовали нестрогие порядки TotalOrder? Как мы помним, в определении функции totality использование усеченной операции || было весьма существенно, то есть это определение не эквивалентно определению, в котором вместо || используется Or.

Ответ на этот вопрос выглядит так: построить аналог insert для TotalOrder по-прежнему возможно, однако для этого нам пришлось бы доказать, что тип функции insert является утверждением (это позволило бы нам в определении insert произвести сопоставление с образцом по утверждению totality x y).

Иными словами, нам пришлось бы доказать, что существует только один с точностью до равенства упорядоченный список, являющийся результатом вставки элемента y в упорядоченный список xs. Несложно увидеть, что это верный факт, однако его формальное доказательство уже не столь тривиально. Мы оставляем проверку этого факта в качестве упражнения для заинтересованного читателя.

3. Заключительные замечания

В настоящем введении мы познакомились с основными конструкциями языка Arend, а также научились пользоваться механизмом классов. Мы сумели реализовать простейший алгоритм вместе с доказательством его спецификации. Таким образом, мы показали, что Arend вполне пригоден для решения «житейских» задач, таких как, например, верификация программ.

Мы упомянули далеко не все возможности и особенности Arend. Например, мы почти ничего не сказали про типы с условиями, позволяющие «склеить» различные конструкторы типа при некоторых специальных значениях параметров этих конструкторов. Например, реализация типа целых чисел в Arend даётся при помощи типов с условиями следующим образом:

\data Int
  | pos Nat
  | neg Nat \with { zero => pos zero }

В данном определении говорится, что целые числа состоят из двух копий типа натуральных чисел, в которых отождествлены «положительный» и «отрицательный» нули. Такое определение гораздо более удобно, чем определение из стандартной библиотеки Coq, где «отрицательную копию» натуральных чисел приходится «сдвигать на единицу», чтобы эти копии не пересекались (намного удобнее, когда нотация neg 1 обозначает число -1, а не -2).

Мы ничего не сказали про алгоритм вывода предикативных и гомотопических уровней у классов и их экземпляров. Мы также почти не упоминали тип интервала I, хотя он играет ключевую роль в теории типов с интервалом, являющейся логическим основанием Arend. Чтобы понять, насколько важен этот тип, достаточно упомянуть, что в Arend равенство типов определяется через понятие интервала. Сопоставление с образцом по переменной, имеющей тип интервала, ведется согласно достаточно специфическим правилам, о которых мы также ничего не сказали в настоящей статье (т.н. гомотопическое сопоставление с образцом).

Автор статьи: Сергей Синчук, старший исследователь группы HoTT и зависимых типов в JetBrains Research.