oort: http://arxiv.org/abs/1307.8418"Under thi

(Анонимно)
2013-12-23 21:11 (ссылка)

Митя, бросай ты эту алгебраическую геометрию, займись лучше теорией типов. Тут как раз конструктивную интерпретацию аксиомы унивалентности Воеводского (https://groups.google.com/forum/#!topic/homotopytypetheory/GmXKEArD3HY) открыли. Это реальный шаг к коммунизму! Или почитай работы Конорушки нашего МакБрайда (http://strictlypositive.org/). То о чем мечтали фантасты натурально.

(Ответить) (Ветвь дискуссии)

(Анонимно)
2013-12-24 23:44 (ссылка)

Анон, а ты не хочешь написать пост с кратким планом того как это всё лучше учить? Я читал Мартин-Лёфа немного и пробовал чуть-чуть в Coq'е доказывать, но потом забросил. Так много всего интересного, но я не студент. Мне еще на работу надо ходить. Но для других интересующихся мини-обзор бы не помешал.

(Ответить) (Уровень выше) (Ветвь дискуссии)

ljranonymous
2013-12-25 18:20 (ссылка)

В качестве пререквиза надо знать мат. логику (что такое предикат хотя бы) и какой-нибудь ``чистый'' функциональный язык. В моем случаем это был Haskell. Самые важные концепции, которые из него надо знать, это параметрический полиморфизм, рекурсивные типы и определение функций над ними путем pattern matching. Если ты понимаешь, почему из data List a = Nil | Cons a (List a) не бывает тотальных полиморфных функций в data BTree a = Leaf a | Node (BTree a) (BTree a), то ты дошел до кондиции. Полезно также почитать Уодлера. Если ты категорно-ориентированный чувак, то на этом этапе ты должен познакомиться с функторами, естественными преобразованиями и монадами. Заметь, что в computer science полезны некоторые типы функторов, которые по-видиму не используются среди математиков: applicative, foldable, traversable. Из книжек мне была полезна Graham Hutton, Programming in Haskell.

Основные концепции интуиционистской теории типов: индуктивные типы, зависимые типы (в частности, индуктивные семейства), соответствие Карри-Говарда. Индуктивные типы -- это подмножество рекурсивных типов, которые удовлетворяют условию строгой положительности (см. Thierry Coquand, Christine Paulin: Inductively defined types). Для таких типов понятно как строить принцип индукции и как с ними вычислять. С категорной точки зрения, индуктивные типы связаны с функторами у которых есть наименьшая неподвижная точка.

Обычно языки с зависимыми типами (Agda, язык системы Coq и т.п.) позволяют определять только тотальные функции, чтобы не загубить логическую сторону соответствия Карри-Говарда. Допускается только структурная рекурсия плюс есть проверка покрытия случаев. По началу может показаться, что это неудобно, но на самом деле это очень полезно при доказательствах. Плюс общерекурсивные функции допускают интересную декомпозицию через структурно рекурсивные, которая называется гилеморфизмом (см. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire или Sorting Morphisms by Lex Augusteijn). Эта же конструкция возникает при исследовании жадных алгоритмов и динамического программирования (см. Bird, de Moor Algebra of Programming; есть формализация в Agda).

Зависимые типы нужны, чтобы выражать свойства (предикаты). Сократить, так сказать, semantic gap. Объяснить компилятору какие свойства должна иметь программа и доказать, что она их имеет. Например, можно заявить, что результатом вычисления является не просто список, а отсортированный список. И тогда при определении функции придется это доказать, иначе компилятор программу не примет. С категорной точки зрения зависимые типы связаны с fibered cateogries. Кстати, аноны, если вам в сраче надо будет доказать, что у теории категорий есть содержательные применения в computer science, ссылайтесь на эту работу.

Есть две основных области, в которых используется интуиционистская теория типов: формальная верификация и доказательство теорем vs политипическое/метапрограммирование. Если больше интересует первая то лучше использовать Coq, если вторая, то Agda. У Coq значительно больше пользователей, больше библиотек, больше работ и литературы. Там есть шикарный язык для создания тактик доказательств Ltac и библиотечка ssreflect. Это помогает в значительной степени автоматизировать процесс доказательства. У Coq есть импредикативный универсум Prop, куда можно поместить вычислительно нерелевантные доказательства. Тогда при экспорте, скажем в Haskell, они будут стерты и получившаяся программа будет не хуже того, что можно было бы написать вручную. При этом она будет верифицирована. Если же сильно использовать индуктивные семейства в вычислениях, то результирующий код будет ужасен. Это, очевидно, временная ситуация, зависимые типы дают гораздо больше возможностей для оптимизации (см. работы Edwin Brady, начать с этой). У Coq достаточно уродский синтаксис для работы с индуктивными семействами. Он правда со временем улучшается, три года назад поддержка была совсем никакая. Еще у Coq нет индуктивно-рекурсивных семейств. У Agda они напротив есть, что делает возможным элегантные вложения теории типов в теорию типов (это важно для политипического программирования). В Agda хорошая поддержка индуктивных семейств и, в частности, механизма view, придуманного МакБрайдом и МакКиной.

Если кратко, то Coq -- это явно станет мейнстриом (или уже стал, в этом году разработчикам присудили какую престижную ACMовскую премию). В нем респектабельные кексы делают серьезные дела. Например, работы К. Лероя по верификации компилятора Си. Язык настолько выразительный, что в нем можно описать синтаксис и семантику языка Си, ассемблера и доказать, что процесс компиляции сохраняет семантику (это очень упрощенно, там конечно как в настоящих компиляторах куча промежуточных языков плюс немного оптимизирующих преобразований). Так-то, а чего добился ты? Agda больше для маргиналов и аутсайдеров, которые делают там супер интересные штуки (орнаменты, например).

Но вообще это непаханное поле, куча проблем. Русские же как обычно сосут. И это очень забавно, учитывая то, что Мартин-Леф является учеником Колмогорова, а сам Колмогоров еще в 30 каком-то году писал, что интуиционистское исчисление высказывание нужно интерпретировать как исчисление задач (Brouwer–Heyting–Kolmogorov interpretation).

Введение для Coq: Sofware Foundations, книга Сertified programming with dependent types (в ней особый упор делается на использования тактик доказательств) и книжка Interactive Theorem Proving and Program Development, которая на мой взгляд уступает первым двум, подойдет совсем теплым гражданам.

Введение для Agda: две вводных статьи (раз и два) и супер курс от Конора МакБрайда: от начального до очень продвинутого материала. Есть видео на ютубе.

(Ответить) (Уровень выше)