bamalip: (NGE)
Мне на выходных ставили вопрос о сигма-типах (но тогда происходили слишком бурные события):
http://zeit-raffer.livejournal.com/169637.html?thread=733605#t733605

Отвечаю. Кодировка состоит из нескольких слоев - превращение зависимых типов в расслоения, представление сигм контекстами (категория контекстов), и сворачивание сложных типов "обобщенным черчем" (т.е. пределы), которое в тривиальном случае у меня записано как Pack.

Пусть заданы (B : Type) (F : B -> Type)

Тип сигмы кодируется как (Sigma := Pack record (b : B)(f : F b)), где под record понимается контекст (как и везде в файлах с расширением macro).

С первой проекцией проблем не возникает (pr1 : Sigma B F -> B).

Для кодирования второй проекции нам нужно выписать ее тип. Это (s : Sigma B F) -> F (pr1 s)
Она должна кодироваться сечением расслоения Pack record (b : B) (f1,f2 : F b) -> Pack record (b : B) (f : F b). Его можно задать как Pack.map (\{b,f} -> {b,f,f}).

Выше написано то, что происходит в сетоидно-категорной кодировке. Что там будет с сигмами в "Симплетоне", я еще не знаю.

Еще раз напоминаю, что окончательная форма кодировки пока не выписана / не проверена пруфчекером, соответственно я не говорю, что результат окончательно получен, и нигде этого не говорил. Я провожу исследование и пока не встретил препятствий для его продвижения вперед.
bamalip: (NGE)
Наша "индукция" не живет сама по себе, для типа Bool или другого. Она представлена в виде трансляции формальных систем (язык + правила вывода и аксиомы): `CIC -t-> CoC`. Реализация аксиом CIC, таким образом, представляет собой только половину проблемы, другая половина - это описание трансляции всех языковых выражений. Первая половина, аксиомы, у нас реализована (да, для Bool), вторая, трансляция АСТ, витает в виде идеи (расслоения). Надо реализовать. Причем реализовать можно как (1) в общепринято-математическом виде "семантика, модель, тра-ля-ля", типа монографии Джекобса на 700 страниц, либо (2) записать тайпчеканную тотальную функцию на Агде или Леан. Второй вариант выйдет короче и будет надежнее, и непосредственно может быть портирован в Эрланг и/или ЕХЕ как работающий транслятор. Поэтому мне он видится более экономным по времени.

В упрощенном виде "для статьи" можно функцию трансляции ограничить до `(CoC+Bool) -a-> (CoC+records) -b-> CoC`. Минимальная часть `CoC -a0-> CoC` все равно нетривиальна. Она представляется в виде композиции `CoC --> (CategoryTheory) --> CoC`, где в промежутке у нас язык, состоящих из термов некоторой "синтаксической категории". Я могу оптимизировать этот участок, "посчитав" композицию в голове и не упоминая категорную часть явно, но разобраться полностью, как она устроена, я все равно должен. Отсюда игры с Hask, в котором реализована SystemF, как более простой вариант по сравнению с полными зав-типами. Всё связано!

Можно поставить вопрос о публикации отдельной статьи об аксиоме индукции для Bool (могу и для Nat, так солиднее), но я не уверен, что в ней есть смысл отдельно от всей трансляции `CIC -t-> CoC`. Можно написать, что это первая статья из серии статей, например.

Ситуация осложняется или улучшается тем, что я за лето в несколько шагов упрощал свои идеи по реализации кодировки. Я не знаю, хорошо это или плохо (может показаться, что мы меняем цели, и чего-то не достигаем), но если бы я просто "прыгал под деревом" в попытках сразу "сорвать банан", то я бы еще не сделал даже того, что уже сделано сейчас (да, Bool), потому что изначально реализация индукции виделась гораздо объемнее (включая портирование категорной библиотечки на ОМ). Сейчас я доделываю очередной раунд упрощения, будет неимоверно просто. Это хорошо, но при написании статьи надо выбирать, описывать ли все версии кодировки или какую-то одну (первую? последнюю? или опять серию статей?).

Дальше, для программистской части, нам нужен тайпчекер и транслятор `макросы->CoC`. Отдельный тайпчекер желателен, чтобы не попать в ситуацию, из которой уже который год пытается выбраться С++ со своими темплейтами, которые подставляются до тайпчека. Основное новшество по сравнению с ОМ тайпчекера здесь будет в сборе информации о записях/рекордах, которая потом пойдет в транслятор. Кроме того у нас осталась задача из ОМ: надо договориться, как ОМ режет дерево файловой системы на модули Эрланга и как это описывается в исходных файлах ЕХЕ (простейший вариант: 1 файл ЕХЕ -> 1 файл Эрланга).

Дальше необходимо выбрать систему описания типобезопасных макросов, тем более, что образцов для подражания у нас достаточно (это подразумевает расширение парсера и транслятора). Дальше портировать на язык макросов те функции трансляции верхнего языка, которые у нас будут уже к этому моменту реализованы на Леан или Агде. Так постепенно начнет проявляться ЕХЕ, если мы к тому времени будем еще живы и трудоспособны.
bamalip: (NGE)
Мысли по поводу нового варианта получения инициальной алгебры, то что сейчас в процессе.

Можно определить функтор, выделяющий в каждом объекте A минимальный подобъект, т.е. инициальный объект в C/A. Этот функтор оказывается комонадой. И вместо того, чтобы строить инициальную алгебру сразу, можно взять минимальную подалгебру простой черчевской.

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

Следите на новостями!
bamalip: (NGE)
Я пишу здесь постоянно, над чем работаю, но обычно это выглядит черезчур фрагментарно, поэтому сейчас я попытаюсь описать текущее положение вещей в нашем проекте в рамках одного поста.

____________________________________________________________________

Что уже есть?

Стек языков состоит из OM (низкоуровневый) и ЕХЕ (высокоуровневый).

OM - это реализация CoC, Calculus of Construction, с иерархией универсумов, с опциональной предикативностью. Фактически ОМ - это лямбда-исчисление с зависимыми типами. Сейчас мы транслируем его в Эрланг, но запланированы и другие бекэнды.

В репозитории на данный момент можно ознакомиться с таким исходным кодом:

OM, транслятор, на Эрланге
- парсер https://github.com/groupoid/om/blob/master/src/om_parse.erl
- тайпчекер https://github.com/groupoid/om/blob/master/src/om_type.erl
- стиратель https://github.com/groupoid/om/blob/master/src/om_erase.erl
- кодогенератор https://github.com/groupoid/om/blob/master/src/om_extract.erl
+ стиратель я сейчас дорабатываю (и в будущем мы планируем его улучшать и улучшать)

OM, работающие примеры библиотек, на ОМ
- "normal" https://github.com/groupoid/om/tree/master/priv/normal - это минимальная практическая библиотека, созданная по образцу библиотеки для языка Морте от Габриэля Гонзалеза, для индуктивных типов используется простейшая кодировка Черча (или Бёма-Берардуччи, если угодно), есть минимальная реализация монады IO.
- "new-setoids" https://github.com/groupoid/om/tree/master/priv/new-setoids - это реализация структуры "сетоид", на которой мы планировали делать кодировку, но потом переключились на следующий, немного урезанный вариант; в перспективе мы доделаем все варианты кодировок да рабочего состояния и проведем бенчмарки.
- "posets" https://github.com/groupoid/om/tree/master/priv/posets - реализация структуры "нерефлексивных частично-упорядоченных множеств", которые являются урезанным вариантом сетоидов и записываются в теории типов короче, чем сетоиды; здесь реализовано вручную несколько простейших типов данных, в частности тип Bool, вместе с зависимым элиминатором https://github.com/groupoid/om/tree/master/priv/posets/Data/Bool/
+ планируется написать все библиотеки на верхнем языке ЕХЕ (сейчас на ОМ писать вручную очень трудоемко) и держать в репозитории ОМ оттранслированный вариант для самостоятельного использования.
+ планируется дописать (уже начатые) библиотеки girard, hurkens, russell, в которых будут реализованы известные логические парадоксы, показывающие неконсистентность теории типов с импредикативной иерархией универсумов.

ЕХЕ - это реализация CIC, Calculus of Inductive Constructions, с минималистичным, но юзабельным синтаксисом (синтаксис на данный момент еще не совсем зафиксирован, subject to change). ЕХЕ транслируется в ОМ.

По техническим причинам нам удобно разделить ЕХЕ на
- ядро имеет типы `record`, которые используются как модули или как структуры, они прозрачно транслируются в ОМ как "контексты" (т.е. просто последовательности типов и термов);
- над ним слой метапрограммирования, который позволяет записывать и исполнять макросы, транслирующие верхний язык в ядро;
- на макросах мы пишем библиотечку для собственно кодировки (будут разные варианты, которые можно будет переключать при компиляции);
- верхний "прикладной" язык, собственно само ЕХЕ, в котором при помощи макросов из предыдущего слоя можно использовать индуктивные и коиндуктивные типы, data, codata, (в перспективе и индуктивно-индуктивные, mutual).

Скорее всего синтаксис ядра будет просто подъязыком верхнего языка.

В репозитории на данный момент можно ознакомиться с таким исходным кодом:

EXE, транслятор, на Эрланге
- парсер ядра https://github.com/groupoid/exe/blob/master/src/macro_parser.yrl
+ в разработке - синтаксический механизм нотаций, они же миксфиксные операторы, они же просто сахар

ЕХЕ, примеры кода, на ЕХЕ
- пример кодировки для типа Bool, https://github.com/groupoid/exe/blob/master/prelude/macro.new/Data.Bool.macro (этот исходный код должен транслироваться в ту библиотечку, которая сейчас лежит в ОМ -> https://github.com/groupoid/om/tree/master/priv/posets/Data/Bool/
- см. в том же каталоге кодировки некоторых других типов, например свободной монады https://github.com/groupoid/exe/blob/master/prelude/macro.new/Data.FreeMonad.macro
+ макросы, которые будут генерировать все это для любых типов

____________________________________________________________________

Как оно работает?

Полностью идею кодировки мы начали последовательно излагать вот здесь: https://github.com/groupoid/om/blob/master/doc/tale.tex однако переключились на непосредственно написание компилятора. Документация это хорошо и важно, но приоритетнее - рабочий код. Надеемся в скором времени дописать все подробно. А коротко я сейчас изложу, у нас уже появилось несколько вариантов.

Прежде всего - то, что реализовано, работает в CoC с добавлением непредикативной иерархии. Это немного печально (ввиду проблем с консистентностью), но мы надеемся сделать ограниченный вариант, который будет умещаться в исходный CoC с одной *, консистентность которого доказана.

На чем основана исходная идея.

Есть на свете такая теория категорий. Если читатель о ней знает, это хорошо, а если нет, то я отсылаю его к учебникам, в одном посте это описать трудно. В мире теории категорий имеются некоторые способы характеризации объектов, называемые универсальным свойством, и некоторые теоремы о них. В частности, есть способы вычисления сопряженных функторов, основанный на теореме Фрейда о сопряженных функторах (их есть несколько). Эта информация общеизвестна в среде алгебраистов, например, в популярный учебник Ленга входит описание процедуры конструирования подобным приемом алгебраического замыкания поля. Нам сейчас будет достаточно такого факта, что инициальный объект совпадает (с точностью до изоморфизма) с пределом тождественного функтора.

То была алгебра, а вот computer science. В мире теории типов известно, что аксиомы, описывающие индуктивные типы данных (их конструкторы и элиминаторы), выглядят не очень просто (как бы ad hoc), если смотреть на них невооруженным взглядом, но на самом деле они просто означают инициальность объекта, заданного типом и конструкторами (F-algebra), в категории подобных объектов (теория категорий, как всегда, все упрощает). Это значит, что мы можем применить для построения индуктивных типов теорему из предыдущего абзаца.

Тут возникает интересный момент. В теории типов есть как бы общеизвестная вера в то, что рекурсор (non-dependent eliminator) представляет собой более слабое свойство, чем индукция (dependent eliminator). В то же время из теории категорий мы знаем, что универсальное свойство определяет объект однозначно, а в случае инициального объекта в категории алгебр инициальность задается, фактически, рекурсором. Это значит, что все свойства нашей алгебры вытекают из ее инициальности, в частности, из рекурсора можно получить индукцию. Тут есть тонкий момент - все категорные конструкции формулируются в присутствии предзаданного хорошо ведущего себя равенства на морфизмах, в то время как в теории типов равенство является внутренней конструкцией, у которой может быть много сложных свойств, зависящих от дополнительных аксиом. Упрощая, мы можем сказать так: без равенства мы можем получить только рекурсор из индукции; в присутствии хорошего равенства мы можем, наоборот, получить индукцию из рекурсора.

Механизм получения индукции за счет равенства основывается на представлении зависимых типов в рамках теории категорий через расслоения. Зависимый тип (D: B -> Type) при этом задается как морфизм (p: Sigma B P -> B), который просто проектирует зависимую пару на первое поле. В топологии (см. HoTT) такой подход называют "расслоениями". В обратную сторону, если задан произвольный морфизм (p: E -> B), который мы понимаем как расслоение с проекцией p, мы можем получить из него зависимый тип (D: B -> Type), вычисляя в каждой точке (b: B) ее прообраз при проекции p (для чего нам потребуется использовать некоторое равенство на элементах B). В теории типов помимо упомянутой здесь зависимой суммы Sigma используют еще Pi, зависимое произведение. При нашем кодировании зависимых типов расслоениями элементам зависимого поизведения соотвествуют морфизмы-сечения для проекции p, т.е. такие (s: B -> E), которые после умножения их на p дают единицу. Пример реализации этой конструкции можно увидеть тут:
ЕХЕ - https://github.com/groupoid/exe/blob/master/prelude/macro.new/Mini.macro#L71
ОМ - https://github.com/groupoid/om/blob/master/priv/posets/sec2all

На вход индукции мы передаем предикат - зависимый тип, закодированный в виде проекции (p: E -> B). Индукция требует дополнительную информацию о предикате, тип которой определяется типами конструкторов исследуемого индуктивного типа; она в точности соответствует утверждению о том, что на E задана структура F-алгебры. Теперь достаточно применить рекурсор к E, получив отображение (I -> E) из инициального объекта, которое оказывается сечением расслоения, а значит, задает ту самую зависимую функцию, которая окажется значением "доказанной" таким способом аксиомы индукции. Реализация:
ЕХЕ - https://github.com/groupoid/exe/blob/master/prelude/macro.new/Data.Bool.macro#L128
ОМ - https://github.com/groupoid/om/blob/master/priv/posets/Data/Bool/induc

Итак, мы кодируем типы исходного лямбда-исчисления - объектами выбранной категории, зависимые типы - расслоениями, зависимые функции - сечениями, индуктивные типы - пределами тождественного функтора на категории алгебр, зависимый элиминатор - конструкцией, описанной в предыдущем абзаце.

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

Собственно, сейчас в коде реализована последняя конструкция. Необходимое для трансляции отображение исходных типов на объекты выбранной категории еще не воплощено в коде, и будет реализовано на языке макросов. Конечно, все это немного громоздко.

____________________________________________________________________

Что еще запланировано?

Буквально вчера я закоммитил вариант упрощенной кодировки, который не опирается на слой категорных абстраций, но в некотором смысле делает то же самое. Пока не ясно, удастся ли довести его до полной трансляции CIC->CoC, но если удастся, то это будет неплохая оптимизация. https://github.com/groupoid/exe/tree/master/prelude/smart-simpleton

Кроме того, есть мысли по поводу кодировки в предикативной иерархии универсумов, но потребуется время, чтобы довести их до рабочего варианта (или опровергнуть идею). Ожидается, что она будет более сложной и будет использовать категорные доктрины (идемпотентные 2-монады).

____________________________________________________________________


Вопросы и комменты приветствуются.
bamalip: (NGE)
По итогам недели у нас анонс. Грядет еще один вариант кодировки, более приспособленный для ТТ, чем для ТК. Я обратил внимание, что у нас типы выглядят как зависимая пара (el : El) (ok : Ok el) для некоторых типов (El : *) (Ok : El -> *). Второе поле здесь (как предикат) вырезает из первой некоторую часть, на которой у нас выполняются необходимые для структуры аксиомы. Проблема была в том, что предикат записывался так, как нам диктовала ТК, и чтобы вытащить из него то, что нужно для ТТ, нужно было попотеть и выписать километры категорной библиотечки. Сейчас мне пришло в голову (и кое-что получилось сделать на бумаге), что в (Ok) мы можем сразу всунуть то, что нам нужно для ТТ (элиминатор), а получится объект, который изоморфен тому, что был раньше, и он будет удовлетворять всем требуемым свойствам индуктивного типа - хоть теоркатегорным, хоть теортиповым. Пока что в работе два варианта: в одном элиминатор принимает предикат (P : El -> *), во втором, более сложном, (P : ∀ (el : El) -> ∀ (ok : Ok : el) -> *). Сейчас нужно проверить, что такие типы образуют модель CoC. Кроме того, я еще не умею получать конструкторы общего вида.

Безусловно, нужно выписать получающиеся модели в том виде, как это делает, например, Джекобс (на 700 страниц!) и сверить с теми результатами о кодировках, на которые ссылается, например, Пенг-Фу. Хотя на самом дела лучшим сертификатом корректности окажется работающий компилятор.
bamalip: (NGE)
LaTeX в атоме прекрасно работает почти "из коробки" (достаточно установить пару пакетов из репозитория)

Вот я нарисовал оглавление длинного пути, где мы, следуя строгой математической традиции, старательно вводим все определения перед использованием:

latex-in-atom.png

Но будет еще короткий путь (и с него начнем): центром текста является пример термов кодировки для списков, перед этим же приведем по одному-двум мотивационным предложениям на каждое определение, т.е. на каждый пункт оглавления до и после списков, и их упрощенный лямбда-код.

PS: текст планируется не слишком математический, примерно для уровня программистов (см. предыдущий пост). Просто я начал писать сразу про тип List и наткнулся на то, что кучу терминов надо так или иначе вводить и определять, а если делать это настолько минималистично, как это сделано сейчас на нашем сайте (там для тех, кто в курсе!:)), то такое объяснение вызовет еще больше вопросов. А статью впоследствии напишем компутер-сайенсовую отдельно, с явным указанием правил вывода и всего такого, согласно жанру.

* * *

May. 3rd, 2016 06:18 pm
bamalip: (NGE)
сущность котегорий и кодеровок немедля будет описана детективным языком для вящего понимания рачительных читателей!

ждите в следующем номере: умопомрачительная история о пределе и конструкторах.

bamalip: (NGE)
Создаем пределы.

Есть такая типичная ситуация -- мы строим категорию на основе другой, базовой категории. Классический случай -- объекты с дополнительной структурой. Если у нас категория алгебр, то стирающий функтор создает пределы [1]. С коалгебрами дуально - стирающий создает копределы. Это означает, что носитель (ко)предела совпадает с (ко)пределом носителей, а структуру (ко)алгебры можно вытащить из универсальных свойств (ко)предела.

Нас сейчас будет интересовать частный случай - алгебры, структура которых имеет тот же тип, что и конструкторы заданного индуктивного типа. Как мы уже знаем, инициальная алгебра в такой категории - это сам индуктивный тип, причем его можно вычислить как предел тождественного функтора в этой категории. Ее носитель - это предел стирающего функтора. Как нам из общих соображений (понятия created limit) построить конкретные конструкторы, т.е. вычислить предел в категории (ко)алгебр?

Поскольку мы ориентируемся на создание макроса, который будет разбирать конструкцию индуктивного типа на некоторые базовые шаги, мы опишем, как эти шаги влияют на формулу для предела.

Рассмотрим самый общий случай. Категорию диалгебр Dialg P над категорией сетоидов Set будем задавать профунктором P : Set° x Set -> Set. Стирающий функтор обозначим U : Dialg P -> Set. Эта категория обладает универсальным свойством: задание функтора G : D -> Dialg P эквивалентно заданию функтора G'=UG : D -> Set одновременно с концом End P(G'(-), G'(-)). Пределы в Set мы строить умеем, поэтому можно сразу записать U(Lim G) = Lim G'. Нам не хватает структуры диалгебры, т.е. значения P(Lim G', Lim G'). Фактически, пределы в Dialg P задает функция qP,D,G : End P(G'(-), G'(-)) -> P(Lim G', Lim G'). Для получения нужных нам конструкторов достаточно вызвать эту функцию на стирающем функторе U.

Как строить q для P, описывающих алгебры над полиномиальными функторами?

Пусть P0 (A, B) = B, что соответствует простейшему конструктору без аргументов, например Zero : Nat.
Тогда q0(e) : Lim G'; q0(e) = e. Эта запись правомочна, поскольку конец (End), зависящий только от одного аргумента, совпадает с пределом.

Пусть известна q для профунктора P. Проведем вычисления для более сложного профунктора P1 (A, B) = X -> P (A, B). Это означает добавление к конструктору одного аргумента фиксированного типа.
Положим q1(e) : X -> P(Lim G', Lim G'); q1(e)(x)(A) = e(A)(x).

Пусть известна q для профунктора P. Проведем вычисления для более сложного профунктора P2 (A, B) = A -> P (A, B). Это означает добавление к конструктору одного рекурсивного аргумента.
Положим q2(e) : Lim G' -> P(Lim G', Lim G'); q2(e)(l)(A) = e(A)(l(A)).

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

[1] https://ncatlab.org/nlab/show/created+limit
bamalip: (NGE)
А в предикативном случае, если не использовать пополнения (сложно!), то та же Черчевская техника дает такую диаграмму вместо индукции:

I_{n} : *{n}, I_{n+1} : *{n+1} - экземпляры нашей инициальной алгебры в соответствующих универсумах

P : I_{n} -> *{n} - зависимый тип (плюс исходные данные индукции)
π : ΣP -> I_{n} - представление того же зав.типа в виде расслоения над инициальной алгеброй (удобно для категорных конструкций)
i_{ΣP} : I_{n+1} -> ΣP - катаморфизм, который строится рекурсором
i_{I_{n}} : I_{n+1} -> I_{n} - катаморфизм, тоже строится рекурсором, определяет отличие (и связь) инкарнаций нашего индуктивного типа в разных универсумах

Вся хитрость в том, что последний морфизм не обязательно равен единице.
Если он будет равен единице, то у нас будет работать та же схема, что и в непредикативном случае, и коммутативность треугольника из последних трех морфизмов даст желанную аксиому индукции.
Если он не равен единице, а определяет некий подобъект, то его можно интерпретировать так, что ослабленная индукция для зав.типа P над I_{n} строит функцию не на всем I_{n}, а на его подтипе I_{n+1}.
А если нужна функция на I_{n}, то надо брать изначально P над I_{n-1}.
Как-то так.
"Индукция со сдвигом".

Подчеркиваю, в этом посте имеются в виду объекты в нашей почти-черчевкой кодировке. Для избавления от сдвига я и пытался сделать что-то с пополнениями.
bamalip: (NGE)
а задумывались ли вы, дорогие читатели, что привычные вещи, как пустой тип (инициальный объект) и натурально-числовой объект - имеют свою копию в каждом универсуме, причем эти копии могут не совпадать? и ничего приятного в такой фантастике нет - мы вычисляем пустой объект, а он не совсем пустой, потому что есть другой, еще более пустой (?!). и набор натуральных чисел может оказаться разным, что может вызвать проблемы с попыткой проитерировать функцию.

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

итого, при проверке у нас оказалось, что подход к кодировке в предикативной иерархии работоспособен только для пустого типа. для остальных индуктивных типов есть претенденты, но не похоже, что они правильно работают. в следующих выпусках нашего журнала мы опишем эту космонавтику подробнее.
bamalip: (NGE)
все эти потуги, чтобы изобразить в чистой системе типов одно сложное выражение, удовлетворяющее типу аксиомы аксиомы индукции. ничего, мы взлетим!

как сказано:

Есть одно слово,
Которое сложно сказать.
Но скажи его раз, и железная клетка пуста
http://www.ytime.com.ua/ru/55/1739/31/

БГ - Ещё один раз (15) Рига live



Для этого нам понадобятся:

- понятие категории
- категории функторов
- опционально - эквивалентность и сопряжения функторов
- опционально - предел функтора
- категория сетоидов, включая сетоиды отображений сетоидов
- категория зависимых сетоидов DepSetoid
- слайс-категория сетоидов над сетоидом OverSetoid
- функтор между этими категориями, вычисляющий Сигма-тип (строится как инициальная алгебра, которая строится как предел)
- это функтор задает эквивалентность двух предыдущих категорий
- два сопряжения, описывающих Пи-типы (кванторы), для DepSetoid и OverSetoid
- утверждение о коммутативности треугольника, образованного эквивалентностью (Сигма-тип) и сопряжениями для Пи-типов (это основной факт семантики зависимых типов в LCCC, и он нам нужен)

Для индукции потребуются еще:
- универсальные свойства пределов
- теорема о сопряженных функторах для случая инициального объекта
- мета-факт, что типы в зависимом элиминаторе "сами собой" складываются в F-алгебру над инициальной F-алгеброй (с учетом того, что в элиминаторе упонимается объект DepSetoid, а мы используем объект OverSetoid)
- наконец, из небольшой манипуляции со стрелочками, - аксиома индукции

(и меньше, вроде, не получается).

сейчас делаю несколько строчек из этого на языке макросов (который нам нужен ввиду трудности написания непосредственно на голой лямбде)

Profile

bamalip: (Default)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 22nd, 2017 06:44 pm
Powered by Dreamwidth Studios