Верифицированный QuickSort на Agda

[VoidEx]

Ух ты, статья по Agda, спасибо большое!

Интересно бы попробовать доказать аналогичное на обычной сортировке. Т.е. для функций

sort : ∀ {l} {a : Set l} → (a → a → bool) → list a → list a
sorted : ∀ {l} {a : Set l} → (a → a → bool) → list a → bool

доказать утверждение

sort-sorts : ∀ {l} {a : Set l} {cmp : a → a → bool} {xs : list a} → sorted (sort xs) ≡ true

[dima_mendeleev]

В данной ситуации обязательно нужно иметь определения функций sort и sorted, потому как с описанного типа много информации получить нельзя. И после уже можно проступать к доказательству — это весьма реально.

[winger]

Как минимум, в sort-sorts необходимо передавать еще доказательство того, что cmp образует полный порядок

[dima_mendeleev]

Вообще то не обязательно. На эти функции нужно смотреть абстрагируясь от названий: задача доказать — а это значить построить терм. Обязательное тут, как я писал — это определения функций sort и sorted, пока этого не будет, ничего точно сказать нельзя. Вот например если так:

-- sort - любой
sorted _ _ = true
sort-sorts = refl

То есть без определений никак.

[winger]

Без доказательства что cmp образует линейный порядок тоже ничего не получится — иначе отсортированная последовательность может не существовать (например если cmp всегда возвращает false)

А то что без определений никак это очевидно)

[dima_mendeleev]

Вы не абстрагируетесь… Забудьте о том, что это функции сортировки.
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
Это нельзя утверждать — и доказательство этому мой пример с предыдущего комментария.

[VoidEx]

Ну мы всё-таки о вполне понятном и очевидном sorted, написать который можно разными путями, но это никак не просто true. И, на всякий случай, такой вариант тоже исключается

sorted cmp xs = xs == sort cmp xs

по понятным причинам.

[dima_mendeleev]

Все правильно, но все же мой пример не единственный при котором не нужно доказательство линейного порядка.
То есть, я только хочу сказать, что следующее утверждать нельзя:
> Без доказательства что cmp образует линейный порядок тоже ничего не получится

[winger]

Я рассматриваю случай когда реализации sort и sorted действительно соответствуют своим названиям — и утверждаю что в этом случае для доказательства их корректности обязательно потребуется еще один аргумент.

[dima_mendeleev]

В этом случае согласен. Наверное зависимые типы и суровая жизнь заставили меня больше верить типу функции чем ее названию.
Действительно без определенных ограничений на функцию сравнения ничего не получится.

[dima_mendeleev]

А как такой вариант?

sort _ [] = []
sort _<_ (h :: t) = filter (\x -> x < h) t ++ h ++ filter (\x -> not (x < h)) t

sorted _ []  = true
sorted _ (_ :: [])  = true
sorted _<_ (x :: y :: t)  = ((x < y) || not (y < x)) && sorted _<_ (y :: t)

[kingu]

Как вы набираете тест программы? Особенно эти кванторы, нижние индексы?

[winger]

Для agda есть замечательный emacs agda-mode, в нем есть сочетания для набора математических символов и goals, существенно облегчающие разработку/доказательства.
Goal, грубо говоря, «дырка» в программе, для которой agda показывает необходимый тип выражения и все выражения которые есть в контексте с их типами.

[dima_mendeleev]

… пишешь \_1 получается ₁, пишешь \<=, получается ≤, пишешь \all или \forall, получается ∀.
Еще классно, что в agda-mode есть подсказки, типа intellisense.

[ramntry]

Почти TeX :)

[dima_mendeleev]

Это и есть ТеХ ;)
А еще Unicode можно:

\название_символа

[roman_kashitsyn]

Кстати, вставку символов по именам в TeX можно получить в любом моде Emacs через
M-x set-input-method TeX

[winger]

github.com/winger/agda-stuff/blob/master/Splay.agda — реализация splay-дерева с доказательствами, правда пока есть пара пробелов, не хватает времени дописать

[terrain]

«Прочитав несколько книг по типизированном лямбда исчисление»

«И я шепчу дрожащие губами
Велик могучим русский языка» (с) А. Иванов

Возможно:
«Прочитав несколько книг по типизированному лямбда исчислению»?

[dima_mendeleev]

Кэп в ударе?

[dima_mendeleev]

Простите, я имел ввиду, спасибо:)

[dima_mendeleev]

Простите, это сюда… пиво=)

[AztEK]

Можно ещё взглянуть на статью Why Dependent Types Matter МакБрайда et al, там приводится верифицированный merge sort на Epigram.

[dima_mendeleev]

Спасибо! Интересный материал, у меня кстати был выбор, что писать: merge или quck sort.
Но если честно мне синтаксис Agda больше нравиться чем Epigram. На самом деле я не сразу на Agda подсел. Была попытка с ATS, и длительное время сидел на Coq. Но Agda все же привлекает больше всего. Плюс заманчивая возможность через Haskell подключить C/C++ — боюсь даже представить, что может выйти.