Всё для Учёбы — студенческий файлообменник
1 монета
pdf

Студенческий документ № 010372 из РГПУ

Временн?aя сложность оптимальной сортировки

Борис Золотов

Научный руководитель - Д.Г. Штукенберг

Герценовские чтения

21 апреля 2017

Отцы-основатели

Morten Heine Sorensen, Pawel Urzyczyn,

Lectures on Curry-Howard Isomorphism, 2006

?-исчисление

Формальная система, по выразительности эквивалентна машинам Тьюринга и рекурсивным функциям. Полна - тезис Чёрча-Тьюринга.

?-термы и ?-эквивалентность 1 ?? ::= V | (?? ??) | (?V . ??)

2 ?x.x z =? ?y.y z ?x.x a 6=? ?x.x b

3 ?=??/ =? ?-редукция

?f . (?x.f (f x)) (?n.n?2) 5 ?> (5 ? 2) ? 2 = 20,, ?x.x x ?x.x x ?> ?x.x x ?x.x x -

Этот терм не редуцируется к нормальной форме. Да и вообще непонятно, что значит применить x к себе. Если такое разрешить - парадокс Карри,, любое утверждение верно.

Что же делать?

Типизированное ?-исчисление: ?>

По Карри: пишем тип терма

?x.?y.x : ? > ? > ?

По Чёрчу: пишем типы всего сразу

?x : ?. ?y : ?. x :? > ? > ?

Типы сохраняются при редукции,, любой типизируемый терм редуцируется к нормальной форме.

Чем же плохо? Теорема Швихтенберга

Расширенные полиномы:

Содержат проекции: Uim(n1,...,nm) = ni,,

Содержат константы, функцию знака,,

Замкнуты относительно сложения и умножения.

Теорема Швихтенберга При обыкновенных целых числах все функции, определённые в ?> - в точности расширенные полиномы. Разные системы типизации. Примеры

?P - типы зависят от термов - string [n],, ?? - типы зависят от типов - List (A),, ?2 - термы зависят от типов - compose :

(p q r : Set) ?> (f : p > q) ?> (g : q > r) ?> (p > r)

Интуиционистская логика. BHK-интерпретация

Доказательства утверждений - из аксиом с помощью правил вывода.

Отсутствует закон исключённого третьего.

BHK-интерпретация P ? Q - пара доказательств (p,q),,

P ? Q - пара (0,p) или (1,q),,

P > Q - конструкция по док-ву p док-ва q,,

?x : P(x) - пара (x,p),,?x : P(x) - функция x > p(x),, P - то же, что P > ?. У ? нет доказательств. Изоморфизм Карри-Ховарда

Типы соответствуют утверждениям,,

Переменные - логическим переменным,,

Обитаемый тип - доказуемое утверждение,,

Типизируемый терм - построенное доказательство.

Примеры ?x.x - доказательство того, что a =? a,,

?f .?g. g ? f - того, что ,,

Элемент z ? n населяет тип "0 ? 2",, s ? s (z ? n) - тип "1 ? 3". Алгоритм сортировки

Задавая вопросы рода "ai (a ? b) ?> (b ? c) ?> (a ? c) trans_? z?n _ = z?n trans_? (s?s p) (s?s q) = s?s (trans_? p q) Формализация понятия алгоритма

Algorithm data Alg : {n : N} ?> List (BorderedNlist n) ?> Set where leaf : {n : N} ?> (b : BorderedNlist n) ?> Alg (b :: [])

node : {n : N} ?> {l : List (BorderedNlist n)} ?> (i j : Fin n) ?> (i 6? j)

?> Alg (cmpFilter i j l) ?> Alg (cmpFilter j i l) ?> Alg l Идея доказательства

Длина списка равна сумме длин двух фильтрованных,,

Длина списка перестановок равна количеству листьев,,

Количество листьев не больше чем 2глубина,,

Утверждение noexist: если глубина - 0, а перестановок много - очевидно,, иначе проверяет все возможные сравнения и для каждого ищет противоречие. Позволяет доказать, что не существует алгоритмов данной глубины для данного множества перестановок.

Плюсы 1 Синтаксис повторяет математические формулы,,

2 Невозможно ошибиться в доказательстве и в программе,,

3 В не очень сложных случаях доказательства генерируются автоматически.

Минусы

1 Абсолютная строгость затрудняет доказательство сколько-то неформальных утверждений,,

2 Размер доказательства очень быстро растёт (нелинейно от размера переменной).

Спасибо за внимание!

Начало?-calcTyped ?-calcЛогикаСортировкиФормальное док-воPros & consКонец

Начало?-calcTyped ?-calcЛогикаСортировкиФормальное док-воPros & consКонец

Борис ЗолотовГерценовские чтения - 2017 Sorting algorithms and Agda

Борис ЗолотовГерценовские чтения - 2017 Sorting algorithms and Agda

Начало?-calcTyped ?-calcЛогикаСортировкиФормальное док-воPros & consКонец

Борис ЗолотовГерценовские чтения - 2017 Sorting algorithms and Agda

Показать полностью… https://vk.com/doc24958510_444329264
339 Кб, 21 апреля 2017 в 12:19 - Россия, Ростов-на-Дону, РГПУ, 2017 г., pdf
Рекомендуемые документы в приложении