Комментарии 24
Ух ты, статья по 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
+2
В данной ситуации обязательно нужно иметь определения функций sort и sorted, потому как с описанного типа много информации получить нельзя. И после уже можно проступать к доказательству — это весьма реально.
+1
Как минимум, в sort-sorts необходимо передавать еще доказательство того, что cmp образует полный порядок
+2
Вообще то не обязательно. На эти функции нужно смотреть абстрагируясь от названий: задача доказать — а это значить построить терм. Обязательное тут, как я писал — это определения функций sort и sorted, пока этого не будет, ничего точно сказать нельзя. Вот например если так:
То есть без определений никак.
-- sort - любой
sorted _ _ = true
sort-sorts = refl
То есть без определений никак.
0
Без доказательства что cmp образует линейный порядок тоже ничего не получится — иначе отсортированная последовательность может не существовать (например если cmp всегда возвращает false)
А то что без определений никак это очевидно)
А то что без определений никак это очевидно)
+1
Вы не абстрагируетесь… Забудьте о том, что это функции сортировки.
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
Это нельзя утверждать — и доказательство этому мой пример с предыдущего комментария.
> Без доказательства что cmp образует линейный порядок тоже ничего не получится
Это нельзя утверждать — и доказательство этому мой пример с предыдущего комментария.
0
Ну мы всё-таки о вполне понятном и очевидном sorted, написать который можно разными путями, но это никак не просто true. И, на всякий случай, такой вариант тоже исключается
по понятным причинам.
sorted cmp xs = xs == sort cmp xs
по понятным причинам.
0
Я рассматриваю случай когда реализации sort и sorted действительно соответствуют своим названиям — и утверждаю что в этом случае для доказательства их корректности обязательно потребуется еще один аргумент.
+1
В этом случае согласен. Наверное зависимые типы и суровая жизнь заставили меня больше верить типу функции чем ее названию.
Действительно без определенных ограничений на функцию сравнения ничего не получится.
Действительно без определенных ограничений на функцию сравнения ничего не получится.
0
А как такой вариант?
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)
0
Как вы набираете тест программы? Особенно эти кванторы, нижние индексы?
+8
Для agda есть замечательный emacs agda-mode, в нем есть сочетания для набора математических символов и goals, существенно облегчающие разработку/доказательства.
Goal, грубо говоря, «дырка» в программе, для которой agda показывает необходимый тип выражения и все выражения которые есть в контексте с их типами.
Goal, грубо говоря, «дырка» в программе, для которой agda показывает необходимый тип выражения и все выражения которые есть в контексте с их типами.
+2
… пишешь \_1 получается ₁, пишешь \<=, получается ≤, пишешь \all или \forall, получается ∀.
Еще классно, что в agda-mode есть подсказки, типа intellisense.
Еще классно, что в agda-mode есть подсказки, типа intellisense.
+2
Почти TeX :)
0
Кстати, вставку символов по именам в TeX можно получить в любом моде Emacs через
M-x set-input-method TeX
0
github.com/winger/agda-stuff/blob/master/Splay.agda — реализация splay-дерева с доказательствами, правда пока есть пара пробелов, не хватает времени дописать
+2
«Прочитав несколько книг по типизированном лямбда исчисление»
«И я шепчу дрожащие губами
Велик могучим русский языка» (с) А. Иванов
Возможно:
«Прочитав несколько книг по типизированному лямбда исчислению»?
«И я шепчу дрожащие губами
Велик могучим русский языка» (с) А. Иванов
Возможно:
«Прочитав несколько книг по типизированному лямбда исчислению»?
0
Кэп в ударе?
0
Простите, это сюда… пиво=)
0
Можно ещё взглянуть на статью Why Dependent Types Matter МакБрайда et al, там приводится верифицированный merge sort на Epigram.
+1
Спасибо! Интересный материал, у меня кстати был выбор, что писать: merge или quck sort.
Но если честно мне синтаксис Agda больше нравиться чем Epigram. На самом деле я не сразу на Agda подсел. Была попытка с ATS, и длительное время сидел на Coq. Но Agda все же привлекает больше всего. Плюс заманчивая возможность через Haskell подключить C/C++ — боюсь даже представить, что может выйти.
Но если честно мне синтаксис Agda больше нравиться чем Epigram. На самом деле я не сразу на Agda подсел. Была попытка с ATS, и длительное время сидел на Coq. Но Agda все же привлекает больше всего. Плюс заманчивая возможность через Haskell подключить C/C++ — боюсь даже представить, что может выйти.
0
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Верифицированный QuickSort на Agda