HoTT, первые впечатления

[ermouth]

Больше для себя, зафиксировать, предыстория здесь и здесь.

Прочитал первые четыре главы http://hottheory.files.wordpress.com/2013/03/hott-a4.pdf.  Первые две главы прочитал уже на два раза. Страниц там 475, а не 600.

Дальше много про математику, довольно нудно. В конце вывод о классах программ, для которых можно строго доказать вычислимость.

HoTT – это просто новый способ представления и манипуляции математическими абстракциями. В этом случае абстракции – это типы, а способ представления и манипуляций – гомотопии. Связаны типы с гомотопиями следующим образом.

Для начала табличка вот, как соотносится терминология type theory, теории множеств, логики и теории гомотопий.

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

HoTT предлагает представлять вычисления, необходимые для установления эквивалентности, как непрерывный путь с началом в пространстве одного типа и концом – в пространстве другого. Начало и конец – точки (type inhabitants), эквивалентность которых мы проверяем.

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

Весь набор таких путей образует гомотопию, как бы “перетекание” пространства одного типа в другой. Каждый такой путь теория предлагает воспринимать как доказательство частного случая эквивалентности типов, а все такие частные случаи – морфизмом из одного типа в другой и обратно.

С точки зрения type theory это множество изоморфизмов тоже является типом и называется identity type. Если такое “перетекание” из типа в тип возможно в обоих направлениях и оно непрерывно, типы эквивалентны вне зависимости от природы этой эквивалентности. Соответственно, нахождение доказательства существования и непрерывности такой гомотопии является доказательством запрошенной эквивалентности между типами в целом.

А типами очень удобно представлять не только какие-то данные в компьютерах, но и определённые предпосылки в математических доказательствах, они куда больше говорят о сущности объекта.

Интересно, что эта конструкция – identity type – всегда может быть построена как последовательный вычислитель, причём всегда двумя способами. Первый способ – построение с помощью трёх правил: formation, introduction и elimination. С компьютерной точки зрения это примерно конструктор, функция-конвертер из типа 1 в тип 2 и функция-конвертер обратно.

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

Между этими identity types также можно установить преобразования эквивалентности и тд.

Из всех этих посылок следует по определению, что любой вложенности корректный identity type всегда является вычислимым (в силу того, что он рекурсивно-определяемый). Собственно, для меня это главное знание, полученное в результате чтения первой половины теории и разбора сопутствующих понятий. Этот вывод там явно вообще не звучит (потому что он не вывод никакой, а определение, да вообще тавтология по-хорошему то), но он для меня очень важен.

Из него прямо следует, что вычислимость программы доказана, как только доказано, что сама программа – суть воплощение identity type, объект этого типа.

Самое интересное в этой конструкции, что jQuery.my-форма это прямо и есть воплощение в  реальном мире этих самых identity types. Конечно, если formation rule (init и отчасти check функции в jQuery.my), а также introduction и elimination rules (объединены в bind-функцию в jQuery.my) соответствуют определению.

jQuery.my форма – штука рекурсивная, она может включать подчинённые формы, а те, в свою очередь ещё подчинённные и тд.

Таким образом, если получится показать, что все внутренние identity types либо (1) рекурсивно определимы, либо (2) их пара introduction-elimination образует harmоny (то-есть рефлексивна, в обе стороны одинаково работает), мы сразу докажем вычислимость jQuery.my-формы.

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

Из (2) следует, что

• мы должны определять check-функцию для каждого поля, её роль по сути – образовывать из набора множеств всех значений конечный набор допустимых значений как типа 1, так и  типа 2 (через последующий вызов bind(bind())
• мы не можем нигде в вычислениях использовать Date() без аргумента, потому что для неё нет обратной функции, которая вернёт undefined
• мы не можем интегрировать, теряя базу (это вот надо трактовать очень широко, например взятие длины строки без сохранения самой строки – это как раз интегрирование с потерей базы, reduce как правило тоже)
• bind-функция при связывании в конкретном направлении не может сдвигать или разрушать точку, из которой она вышла (не может менять аргумент, который преобразовывается)
• вероятно, ещё какие-то ограничения, думаю

Это, в общем, не выглядит невыполнимым – но потребует множества изменений в jQuery.my, в самой механике её работы.

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

Интересно всё обернулось. Скоро в отпуск, намерен круто прокачать type theory и разметить планчик приведения jQuery.my в соответствие этим всем кондишенам.