Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Мечта о финитизме I: Гедонизм

Я начну с цитаты из замечательной статьи Лесли Лампорта «How to write a proof»:
«The proofs have been carried out to an excruciating level of detail … The reader may feel that we have given long, tedious proofs of obvious assertions. However, what he has not seen are the many equally obvious assertions that we discovered to be wrong only by trying to write similarly long, tedious proofs.»

Много веков что математические доказательства, что математические построения (как в геометрии: помните, там часто достраивают всякие штуки, чтобы доказательство провести) записывали обычными человеческими словами. В 19ом веке случился кризис, стало понятно, что если доказательства записывать недостаточно строго, возможны очень тонкие ошибки, которые очень тяжело заметить.

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

Идеи на эту тему были уже у Декарта и Лейбница, но первая попытка сделать такой язык и такую систему принадлежит Фреге с его Begriffschrift. Позже Гильберт и Аккерман усовершенствовали этот метод, и его стало можно применять на практике в математике, но записывать доказательства было всё ещё страшно неудобно, и на практике никто этим не занимался.

Огромным шагом вперёд была разработка Яськовским и Гентценом около 1930 года системы под названием «естественная дедукция» (natural deduction), её адаптированный для записи текстом вариант приводится в отличной статье Лампорта, с которой я начинаю текст. Записывать и читать доказательства в такой форме уже удобно.

Интересно, что примерно в то же время более или менее для нужд информатики придумали т.н. лямбда-исчисление, при помощи которого удобно записывать как раз не доказательства, а построения. Чуть позже обнаружилось, что лямбда-исчисление и естественная дедукция, это одно и то же. Этот факт называется изоморфизмом Карри-Говарда.

Итак, что естественная дедукция, что лямбда-исчисление используют два примитива: применение (application) и абстракцию (abstraction).
Что такое применение?
В случае построений: если у нас есть объект a типа A (записывается a: A) и функция f: A => B, мы можем применить f к а и получить f(a): B
В случае доказательств:
1) Если у нас есть доказательство p, что верно утверждение P (записывается p: [P]) и доказательство f, что из P следует Q (записывается [P] => [Q]), то мы можем применить f к p и получить f(p): [Q], т.е. доказательство что верно Q.
2) Если у нас есть доказательство p, что для всех объектов типа T верно P (записывается p: (x: T) => [P(x)]), и объект a: T, то мы можем применить общее доказательство к объекту, и получить частное доказательство p(a): [P(a)].

Что такое абстракция?
В случае построений: когда мы хотим описать свою функцию A => B, мы пишем [a: A | definition ], где definition это вычисление, использующее а как константу типа A и дающее на выходе B. Синтаксически definition представляет из себя дерево применений и абстракций, т.к. больше никаких примитивов в нашем языке и нет.
В случае доказательств:
1) Чтобы доказать, что из A следует B, необходимо и достаточно сконструировать доказательство B из доказательства A, что записывается как [p: [A] | proof ], где proof это построение [B], использующее p как имеющееся в наличии доказательство [A].
2) Чтобы доказать, что для любого объекта типа T верно P, нужно изготовить функцию, конструирующую доказательство P для любого переданного ей x: T, то есть нам нужно [x: T | proof].

Если в системе изначально определены типы/атомные высказывания с присущими им конструкторами/аксиомами, то любое построение/любое доказательство можно записать на вот таком вот простом языке, использующем всего два примитива. Проверка корректности построения/доказательства сводится к проверке соответствия типов во всех случаях применения. Т.е. что функции f: A => B применяются только к объектам типа A.

Понимание по части изоморфизма Карри-Говарда приходило очень постепенно. Его версия для логики высказываний и для гильбертовой дедукции была понята очень рано: Конструктивистской логике высказываний соответствует просто-типизированное лямбда-исчисление. Также быстро стало понятно, что дедуктивному исчислению Фреге-Гильберта-Аккермана соответствует исчисление комбинаторов SKI. Это открыли в 30ые и 50ые годы соответственно.
Понимание того, что соответствует логике предикатов, пришло значительно позже, с разработкой в 1970ые зависимо-типизированного лямбда-исчисления. Точнее говоря, тогда пришло понимание лишь того, что соответствует конструктивистской логике предикатов. Понимание, как отразить в лямбда-исчислении классическую логику предикатов пришло уже в 1990ые с разработкой зависимого лямбда-мю исчисления.

Математические теории, такие как теория групп или даже теория множеств (внутри которой можно сформулировать все остальные распространённые теории), практически всегда формулируются как набор дополнительных типов, констант и аксиом в дополнение к классической илк конструктивистской логике предикатов. Таким образом, для записи в естественной форме и проверки доказательств в этих теориях требуются возможность гибко расширять типизированные лямбда-исчисления новыми типами с присущими им аксиомами и конструкторами.

Конструктивная теория типов, допускающая расширение т.н. конструктивно-рекурсивными типами (такими, как списки, деревья и всё прочее, что можно конструировать в памяти компьютера программно) обрела законченную формулировку лишь в 2009 году, она называется Observable Type Theory. Это в определённом смысле максимальная теория, оперирующая только конструктивными типами и тотальными вычислимыми функциями. Любые представители любого типа могут быть конкретно представлены в памяти компьютера, любые функции — конечными программами. В начале 1920ых годов Гильберт высказал мечту о финитизме — теории/системе, оперирующей только конечными, конечнопостроимыми объектами, и конечно-доказуемыми высказываниями про них. OTT — это гедонистический вариант финитизма: система вполне удовлетворят требованию, что оперировать нужно только конечными объектами и вычислимыми функциями, однако это богатая, удобная в использовании система, далёкая от минимализма.

Нужно отметить, что исследования в области теории типов ещё далеки от завершения. Во-первых, в отличие от равенства между объектами, которое в OTT наблюдаемое (т.е. равны объекты с одинаковым поведением, а не только объекты с идентичным определением) и вычислимо, равенство между типами чисто синтаксическое, наблюдаемое поведение сторону не затрагивающее. Несколько лет назад Awodey и Воеводский обнаружили связь теории типов с очень далёкой от оснований математики гомотопической теорией. Воеводский (кажется в соавторстве с Thierry Coquand'ом, автором знаменитого верификатора доказательств Coq) на основании этого придумали совершенно неожиданную теорию типов, где равенство между типами тоже является наблюдаемым. Подход оказался столь интересен, что Воеводский, Awodey и Coquand (все трое — весьма крупные математики) сконцентрировали на ней усилия и недавно создали специальную рабочую группу чисто по вопросам этой теории, куда набирали на превосходных условиях докторантов и постдоков. Для этой теории пока не найдено теоретико-множественной модели, так что работать есть над чем. Это направление называется «унивалентной теорией типов».

Во-вторых, активно исследуются расширимые системы, поддерживающие не только дискретно-конкретные типы данных, но и такие штуки как действительные числа. Paul Taylor и коллеги развивают конструктивные теории типов в сторону включения наряду с дискретно-конкретными типами и вычислимыми функциями, топологические пространства с измеримыми функциями между ними (топология и измеримость математически кодифицируют физические пространства величин вместе с процессом их измерения). Это направление называют конструктивным физикализмом.

Наконец третье направление — реализация используемой в математике повсеместно NBG-теории множеств как теории типов. В определённом смысле NBG является максимальной рефлексивной теорией: в NBG все почти все типы можно рассматривать как объекты, объекты типа Set. Ограничение рефлексии нужно чтобы избежать парадокса лжеца, и в NBG оно минимально: каждый тип S представим множеством s, кроме как в случае существования биекции между S и Set. Тут ничего выдающегося не ожидается, однако необходимо преодалеть ряд технических сложностей. Это направление можно назвать максимализмом, и им мало кто занимается в виду невыгодного соотношения объёма технических сложностей и ожидаемой оригинальности результата.
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments