Настроение:	geeky
Музыка:	Ladytron -- Jet Age

Ричард Карп писал о совсем другом
Великие CS мастера древности такие как Кнут или де Бройн были еще и матерыми комбинаторщиками. Связь между алгоритмической сложностью и комбинаторикой, думаю, ясна (вообще-то нет, тут надо бы большую врезку сделать). К сожалению, успехи микроэлектроники заметно снизили необходимость в тщательном анализе алгоритмов, в результате чего теория сложности была захвачена тварями из черной лагуны и по большей части оказалась в аду неконструктивности. Мне всегда казалось это странным, потому что речь в обоих идет о совокупности конструктивных объектов. Если сказать точнее, я был очень удивлен, что перечислительная комбинаторика в действительности не перечисляет, а только считает объекты.

Обычный вопрос звучит так: сколько есть объектов типа X, обладающих свойством P. Обычный ответ дает какую-нибудь формулу подсчета и нудное доказательство в котором смешаны объяснения на естественном языке, формулы, рисунки всякие идиотские. Т.е. в доказательстве есть алгоритм построения объектов, но нет подходящего языка, чтобы формально его описать, вместе с доказательством корректности.

И здесь в игру вступает теория типов.



Когда я познакомился с языками с зависимыми типами (кстати, знакомству с ними обязан вот этому комменту, прочитал я его примерно в 2010) то дико взбодрился, потому что такие языки гораздо лучше подходят для описания и рассуждения о конструктивных объектах. Под лучше, здесь подразумевается прежде всего точность в передачи смыслов. Пример: возьмем перестановки. Перестановку n-элементов можно записать как n-натуральных чисел, где ни одно не повторяется. Обычно в языке программирования нет никакого способа статически передать это свойство ``ни одно не повторяется''. Лучшее что вы можете сделать это выделить кусок памяти, защитить его, и контролировать все операции, которые с ним совершаются, так чтобы это свойство не нарушалось. Но все это происходит уже в run-time, а нас интересуют структурные различия на уровне синтаксиса.

Как это выглядит? Начнем с конечных множеств. Натуральные числа это вот:

data Nat : Set where
   nz : Nat
   ns : Nat -> Nat
Тут вроде бы все ясно: натуральные числа это либо ноль, либо натуральное число плюс один. Надеюсь все понимают, что это чисто синтаксическое представление, в run-time их разумеется можно представить в обычном двоичном виде, но это совсем другая история.

Конечные множества это такое семейство Fin : Nat -> Set такое, что для каждого натурального числа n : Nat тип Fin n имеет ровно n элементов. Можно задать индуктивно:

data Fin : Nat -> Set where
   fz : {n : Nat} -> Fin (ns n)
   fs : {n : Nat} -> Fin n -> Fin (ns n)
Т.е. конечные множеста это либо новый элемент (fz), либо вложение (fs) из предыдущего уровня. Соответственен выражений типа Fin nz не бывает, потому что nz нельзя унифицировать с ns n.

Оказывается, что и другие комбинаторные объекты можно задавать как индуктивные семейства. Это будут точные описания в том смысле, что синтаксически различные описания будут соответствовать семантически различным объектам.

Еще примеры.

Конечные инъективные функции:
data Inj : Nat * Nat -> Set where
   [] : {m : Nat} -> Inj (0 , m)
   _::_ : {n m : Nat}(x : Fin (ns m))(p : Inj (n , m)) -> Inj ((ns n) , (ns m))

Перестановки: Inj (n , n)

Сочетания:
data Bin : Nat * Nat -> Set where
   bz : {n : Nat} -> Bin (n , 0)
   bs : {n m : Nat}(t : Bin (n , ns m)) -> Bin (ns n , ns m)
   bc : {n m : Nat}(t : Bin (n , m)) -> Bin (ns n , ns m)

Разбиения:
data Partition : Nat * Nat -> Set where
   pz : Partition (0 , 0)
   ps : {n m : Nat}(p : Partition (n , ns m)) -> Partition (ns m + n , ns m)
   pc : {n m : Nat}(p : Partition (n , m)) -> Partition (ns n , ns m)

Числа Каталана:
data Cat : Nat * Nat -> Set where
   cz : (m : Nat) -> Cat (0 , m)
   cn : {n m : Nat} -> (Cat (n , 0) * Cat (m , 0)) -> Cat (n , ns m) -> Cat (ns n , m)

Инволюции:
data Involution : Nat -> Set where
   iz : Involution nz
   is : {n : Nat}(i : Involution n) -> Involution (ns n)
   ic : {n : Nat}(x : Fin (ns n))(i : Involution n) -> Involution (ns (ns n))

Собственно все определения получены автоматически из соответствующих рекуррентных соотношений (кроме чисел Каталана, там не совсем автоматически). Не со всеми рекуррентными формулами такое проходит (в смысле получаются точные описания).

Для каждого из них можно построить считающую и перечисляющую процедуру, доказать что они корректны. У каждого из этих семейств есть много интерпретаций и их также можно построить. Например, построить отображение <_> : {n m : Nat} -> Inj (n , m) -> Fin n -> Fin m и доказать, что для любой f : Inj (n , m) функция < f > является инъективной.

Почему это важно? No idea.

0) Они индуктивны, значит можно строить структурно рекурсивные функции (что важно, когда находишься внутри тотального языка) и индукцию в доказательства.
1) Views для других типов. Скажем вот, можно записать тип перестановок как определен выше, а можно как дизъюнктивное объединение циклов. Когда речь о композиции удобнее первый вариант, а когда о действии -- второй. По идее само определение должно быть, как говорят, абстрактным, а эти два описания -- равноправными способами задавать индукцию.
2) Combinatorial Design.
3) Вдохновившись комбинаторными видами, можно значительно расширить класс распознаваемых рекурсивных схем (через Memo-структуры).
4) Собственно хотелось бы построить нормальную теорию сложности.



Такие дела, на фото я.