HoTT

morfizm меня навёл на потрясающую совершенно базовую математическую теорию – HoTT. Собсно, у него-то шла речь о том, что несколько математиков разработали теорию и написали по ней научный 600-страничный труд используя… github. Морфизм это скорее как забавный курьёз привёл – а я пришёл в полный, неописуемый восторг.

В восторг от теории.

Я тут недавно писал про неподвижную точку, валидацию, вычислимость, то-сё… Так вот, цитатка одна:

Secondly, every type-forming rule conforms to a well-understood pattern: there is a part for formation (making a new type), a part for introduction (how to construct elements of that type), a part for elimination (how to extract information from an arbitrary element of that type), and a part for computation (how introduction and elimination interact). This uniformity makes the meta-theoretic analysis of type theory particularly simple, allowing proofs of “consistency by evaluation”.

Болд – от меня. Это вот отсюда, длинный довольно пост, который умеренно подготовленному читателю объясняет, чем же этот HoTT отличается от теории множеств.

Эта цитата соотносится с задачей из поста про неподвижную точку, да и вообще с конструкцией и идеологией jQuery.my так, как будто я про эту теорию знал, когда $.my придумывал. Я был просто потрясён.

Type-forming rule из цитаты – это манифест формы (или рекурсивно её фрагмента), прямо до мелких соответствий. То, что в цитате про inroduction, elimination и computation – это просто таки с точностью до замены терминов вот это http://jquerymy.com/tutorial/what-is-bind/. Все три этих действия у меня просто совмещены в одну функцию для краткости записи. Она просто в обе стороны работает, и для introduction, и для elimination, и для computation посредине.

Та же логика, один-в-один. Даже то, что эта форма может служить дочерним типом для другой формы прямо соотносится с системой построения типов в HoTT.

Элемент определённого типа в моём случае – это группа отображений множества состояний html-формы на множество состояний подлежащего js-объекта. Предполагается, что есть отображения в обе стороны всегда. Такая структура называется в теоркате группоид – и как раз на основе таких структур и выстроена HoTT-теория.

Которая ни много ни мало претендует практически на роль теории множеств в современной математике. И которая… это оттуда же, следующее предложение:

It makes type theory into essentially a programming language, at the same time as a foundational system, allowing the easy verification and construction of proofs by computers.

Так вот, есть уже такой language. В крошечном масштабике и под определённый круг задач, но есть. Жду, когда же наступит этот proof by computers – это ровно та задача, что я озвучивал в посте про неподвижную точку.

Напишу письмо чувакам, как осилю 600 страниц с гитхаба. Это очень интересно.

И неожиданно. Кстати, уважаемому morfizm: в группоиде, который в этой теории базовая конструкция, каждый морфизм – изоморфизм )

Что бы это ни значило.