Наконец-таки наткнулся на книгу, качественно и полно раскрывающую тему задания и исследования систем типов с помощью теории категорий, — "Introduction to Higher-Order Categorical Logic" Ламбека. Она описывает три разных способа задать типовые системы с помощью категориальных структур, — начиная от наивного CCC, заканчивая доказательством того, что любую типовую систему можно описать как топос, и наоборот. Также рассматриваются немаловажные практические вопросы, — категориальное описание нетипизированного лямбда-исчисления, а также эмуляция рекурсии. В общем я с удовольствием сел за её чтение, чего и всем заинтересованным рекоммендую. Для чтения будет достаточно элементарных знаний в логике и знакомства с аксиоматикой Гёделя-Бернайса, Ламбек вводит всё остальное необходимое прямо в книге.
6 comments
recommend
bookmark
subscribe
ничего не понял по описанию, честно говоря. топос — он тоже CCC (плюс классификатор подобъектов). эта теорема есть где-нибудь в сети?
категориальное описание нетипизированного лямбда-счисления — опять же, естественным образом индуцируется на CCC
мат+ня? иногда я думаю что неплохо бы прочесть чего-то по математике, но когда я читаю что-то похожее на эту аннотацию то "лучше и не надо нахуй!")
Топос это очень особый класс CCC/ Структуры CCC, мягко говоря, не хватает, чтобы описать произвольную сложную типовую систему, не теряя о ней информации (например зависимые типы).
то, что структуры CCC для этого не хватает, я прекрасно понимаю. я не понимаю, чем топос "очень особый" в данном контексте
так что, нету теоремы в сети?
Тем, что в нём есть характеристическая функция, очевидно. А "теорема", которую ты так хочешь занимает 40 страниц книги, сомнительно, что ты её найдёшь
жаль