вівторок, 31 липня 2012 р.

[Ссылки] Верифицированный QuickSort на Agda

(Копипастить не буду, но держать в одном месте все же лучше.)

Прочитав несколько книг по типизированному лямбда исчислению, а именно по зависимым типам, увидел интересную закономерность: везде первым примером приводится определение типа «отсортированный список». Все бы хорошо, но дальше этого определения ничего не было. Вот я и придумал восполнить этот пробел и реализовать функцию, принимающую список, и возвращающую другой список и два доказательства. Одно доказывает, что результат — это перестановка входа, а другое доказывает, что результат — отсортированный список.
Читать далее [Habrahabr]