![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
HoTT as a tool
May. 21st, 2015 04:17 pmДавно хотел написать, да всё руки не доходили. Неделю-полторы назад я наткнулся на первую научную работу, где унивалентная теория типов фигурирует как инструмент, а не как объект исследлвания:
www.cis.upenn.edu/~sweirich/papers/yorgey-thesis.pdf
Это диссертация о комбинаторных видах и помеченных структурах. Напомню, что комбинаторные виды (combinatorial species) это обобщающий подход в перечислительной комбинаторике, в рамках которого удобно рассуждать (и проихводить вычисления) обо всяких перестановках, разбиениях, выборках из n по k, помеченных деревьях, отсортированных комбинациях, раскрасках графов и т.д., короче упорядочивание зоопарка из биномиальных коэффициентов, чисел Стирлинга разных родов и т.д. Недавно их ещё обобщили до т.н. "видов штуковин" (stuff types), чтобы они подходили для описания комбинаторных аспектов в физике элементарных частиц (диаграмы Фейнмана/струнные диаграмы и комбинаторика перенормировок), очень мощная получилась штука, элегантно обобщающая результатф Конна-Крамера. Вот для этого дела унивалентная теория типов* подходит просто отлично.
___
* Специально пишу теперь "унивалентная" вместо "гомотопическая", чтобы не исключать свежепоявившиеся кубические теории типов, где унивалентность вселенных не постулат, а свойство.
www.cis.upenn.edu/~sweirich/papers/yorgey-thesis.pdf
Это диссертация о комбинаторных видах и помеченных структурах. Напомню, что комбинаторные виды (combinatorial species) это обобщающий подход в перечислительной комбинаторике, в рамках которого удобно рассуждать (и проихводить вычисления) обо всяких перестановках, разбиениях, выборках из n по k, помеченных деревьях, отсортированных комбинациях, раскрасках графов и т.д., короче упорядочивание зоопарка из биномиальных коэффициентов, чисел Стирлинга разных родов и т.д. Недавно их ещё обобщили до т.н. "видов штуковин" (stuff types), чтобы они подходили для описания комбинаторных аспектов в физике элементарных частиц (диаграмы Фейнмана/струнные диаграмы и комбинаторика перенормировок), очень мощная получилась штука, элегантно обобщающая результатф Конна-Крамера. Вот для этого дела унивалентная теория типов* подходит просто отлично.
___
* Специально пишу теперь "унивалентная" вместо "гомотопическая", чтобы не исключать свежепоявившиеся кубические теории типов, где унивалентность вселенных не постулат, а свойство.
