Твердые приложения теории категорий в TCS?

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

У меня есть какое-то смутное понимание того, что теория категорий полезна на стороне языков программирования / логики («Теория B»), и мне интересно, какую пользу могут принести алгоритмы и сложность («Теория A»). Хотя, возможно, это поможет мне оторваться от земли, если я знаю некоторые серьезные применения теории категорий в теории В. (Я уже неявно предполагаю, что в теории А приложений пока не найдено, но если у вас есть некоторые из них, это даже лучше для меня!)

Под «твердым приложением» я имею в виду:

(1) Применение настолько сильно зависит от теории категорий, что его очень трудно достичь без использования механизма.

(2) Приложение использует по крайней мере одну нетривиальную теорему теории категорий (например, лемму Йонеды).

Вполне возможно, что (1) подразумевает (2), но я хочу убедиться, что это «реальные» приложения.

Хотя у меня есть некоторый опыт «Теории Б», это было давно, поэтому любая де-жаргонизация была бы очень цениться.

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

Я могу вспомнить один случай, когда теория категорий была непосредственно «применена» для решения открытой проблемы в языках программирования: Торстен Альтенкирх, Питер Дибьер, Мартин Хофманн и Фил Скотт, «Нормализация с помощью оценки для типизированного лямбда-исчисления с копроизведениями» . Из их аннотации: «Мы решаем проблему решения для просто типизированного лямбда-исчисления с сильными двоичными суммами, эквивалентно словесной проблеме для свободных декартовых замкнутых категорий с двоичными копроизведениями. Наш метод основан на семантической методике, известной как« нормализация по оценке », и включает в себя инвертирование интерпретации синтаксиса в подходящую модель связки и извлечение соответствующих уникальных нормальных форм ".

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

Важным историческим примером является предложение Эудженио Могги о том, что понятие монады (которое является базовым и вездесущим в теории категорий) может использоваться как часть семантического объяснения побочных эффектов в языках программирования (например, состояния, недетерминизма). Это также вдохновило на размышления о синтаксисе языков программирования, например, привело непосредственно к «классу типов Monad» в Haskell (используется для инкапсуляции эффектов).

Совсем недавно (последнее десятилетие) это объяснение эффектов в терминах монад было пересмотрено с точки зрения старой связи (установленной теоретиками категорий в 60-х годах) между монадами и алгебраическими теориями: см. Мартина Хайленда и Джона Пауэра. , "Теоретическое понимание категории универсальной алгебры: теории и монады Лаврера" . Идея состоит в том, что монадическое представление эффектов совместимо с (в некоторых отношениях более привлекательным) алгебраическим представлением эффектов, в котором эффекты (например, хранение) могут быть объяснены с точки зрения операций (например, «поиск» и «обновление») и связанные уравнения (например, идемпотентность обновления). В последнее время Пол-Андре Мельес (Paul-André Melli) пишет об этой связи: «Условие Сигала встречает вычислительные эффекты».которая также в значительной степени опирается на идеи, исходящие из «теории более высоких категорий» (например, понятие «структура Йонеда» как способ организации семантики дошкольных преобразований).

Другой, связанный класс примеров происходит из линейной логики . Вскоре после его введения Жаном-Ивом Жираром в 80-х годах (с целью лучшего понимания конструктивной логики) были установлены прочные связи с теорией категорий. Некоторые объяснения этой связи см. В статье Джона Баеза и Майка Стей "Физика, топология, логика и вычисления: камень Розетты" .

Наконец, этот ответ будет неполным без ссылки на светлый блог Сигфпа «Соседство бесконечности» . В частности, вы можете проверить «Частичное упорядочение некоторой теории категорий, примененной к Haskell» .

Квантовые вычисления

Одна очень интересная область - применение различных моноидальных категорий к квантовым вычислениям. Кто-то может поспорить, что это тоже физика, но работа выполняется людьми из отделов информатики. Ранняя статья в этой области - категориальная семантика квантовых протоколов Самсона Абрамского и Боба Кекке; многие недавние работы по Абрамскому и Coecke и другим продолжать работу в этом направлении.

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

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

Теория систем

Коалгебра использовалась в качестве общего каркаса для моделирования систем (потоков, автоматов, переходных систем, вероятностных систем). Его теория основана на теории категорий, основанной на понятии коалгебры , где - функтор, который описывает структуру переходной системы. Таким образом, вид системы изменяется с основным функтором, но большая часть теории, такая как понятие бисимуляции, применима для всех функторов. Теория категорий также позволяет модульное построение модальных логик для рассуждений о системах, описанных как угольные алгебры.$F$$F$

Преобразования Графа

Преобразования графов можно довольно хорошо выразить на языке теории категорий. Это нашло применение, например, в преобразовании модели (как в моделях UML) и других формализмах визуального моделирования. Подход имеет место в категории графов и гомоморфизмов графов. Во-первых, отталкивание можно рассматривать как конструкцию склеивания: даны два графика . Граф и два морфизма и обозначают части, общие для двух графов. Отжим объединяет эти части, фактически добавляя оставшиеся части и , склеивая и вместе P e 1 : P → G 1 e 2 : P → G 2 G 1 G 2 G 1 G 2$G_1,G_2$$P$$e_1:P\to G_1$$e_2:P\to G_2$$G_1$$G_2$$G_1$$G_2$$P$ .

Двойной Кодекартов Квадрат используется для описания преобразования графа. Правило представлено кортежем , где обозначает предварительное условие правила, обозначает пост-условие правила, а обозначает часть графа, к которой применяется правило. Существуют карты от и от , одна из которых будет использоваться для соответствия части исходного графа, а другая - для создания результирующего графа. описывает часть графа, подлежащую удалению. описывает часть, которая будет создана. Карта из в контекст$(L, K, R)$$L$$R$$K$$l:K\to L$$r:K\to R$$L\setminus K$$R\setminus K$$d$$K$График должен быть обеспечен, и из Кодекартова Квадрат и отображение должен равняться графиком процентного . Выталкивание и затем дает результат выполнения преобразования.$D$$d$$l$$G$$d$$k$

Языки программирования (через MathOverflow)

Было много применений теории категорий в проектировании языков программирования и теории языков программирования. Обширные ответы можно найти на MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory ) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory .

Биграфы - исчисление процесса

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

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

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

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

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

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

РЕДАКТИРОВАТЬ: я буду продолжать спекулировать, по просьбе Райана. Насколько я понимаю, естественным доказательством является примерно одно из тех, которые пытаются определить индуктивный инвариант структуры цепи, подверженной различным разумным условиям. Подобные идеи (что неудивительно) довольно распространены и в языках программирования, когда вы пытаетесь определить инвариант, поддерживаемый индуктивно с помощью термина лямбда-исчисления (например, чтобы доказать безопасность типов). 1

Однако эта техника часто ломается при более высоких (то есть функциональных) типах. Например, лямбда-исчисление простого типа является полным - каждая программа, написанная в нем, завершается. Однако прямые попытки доказать это имеют тенденцию основывать на проблеме функций первого класса: недостаточно доказать, что каждый член типа заканчивается. Поскольку мы можем дополнительно применять аргументы к функциям, нам нужно не только гарантировать, что каждый член типа останавливается, мы также должны убедиться, что это свойство обладает «наследственно» - нам также нужно знать, что с учетом любого члена тип , приложение также будет остановлено.A → B $A \to B$$A \to B$$A$

Это то, что делают логические отношения. Вместо определения одного индуктивного инварианта, мы определяем целое семейство предикатов путем рекурсии по структуре (обычно) типа. Затем мы докажем, что каждый определяемый термин лежит в соответствующем предикате, что позволяет нам установить то, что мы искали. Поэтому для завершения мы бы сказали, что хорошие значения базового типа являются значениями базового типа, а хорошие значения типа являются значениями этого типа, которые, учитывая хорошее значение , оценивают в хорошее значение изA $A \to B$$A$$B$, Обратите внимание, что не существует единственного индуктивного инварианта - мы определяем целое семейство инвариантов путем рекурсии по структуре входных данных и используем другие средства, чтобы показать, что все члены лежат в этих инвариантах. Теоретически, это намного более сильный метод, и поэтому он позволяет вам доказать результаты согласованности.

Связь с пучками возникает из-за того, что нам часто нужно рассуждать об открытых терминах (то есть, терминах со свободными переменными), и поэтому необходимо различать застревание из-за ошибок и застревание из-за необходимости уменьшения переменной. Пучки возникают из рассмотрения редукций лямбда-исчисления как определения морфизмов категории, члены которой являются объектами (т. Е. Частичного порядка, индуцированного редукцией), а затем из рассмотрения функторов из этой категории в наборы (т. Е. Предикаты). Жан Галлье написал несколько хороших статей об этом в начале 2000-х, но я сомневаюсь, что они читабельны, если вы уже не усвоили достаточное количество лямбда-исчисления.

Есть много примеров, первый из которых приходит на ум - использование теории категорий Алексом Симпсоном для доказательства свойств языков программирования, см., Например, « Вычислительная адекватность для рекурсивных типов в моделях теории интуиционистских множеств », «Анналы чистой и прикладной логики». , 130: 207-275, 2004. Хотя в названии упоминается теория множеств, метод является теоретико-категоричным. Смотрите домашнюю страницу Алекса для большего количества примеров.

Я думаю, что вы задаете два вопроса о применимости, тип A и тип B отдельно.

Как вы заметили, существует множество существенных приложений теории категорий к темам типа B: семантика языков программирования (монады, декартовы замкнутые категории), логика и доказуемость (topoi, разновидности линейной логики).

Тем не менее, кажется, что в теории А мало существенных приложений (алгоритмы или сложность).

В элементарных объектах есть несколько применений, таких как описание категорий автоматов или комбинаторных объектов (графы, последовательности, перестановки и т. Д.). Но, похоже, это не объясняет более глубокого понимания теории или алгоритмов языка.

Спекулятивно, это может быть несоответствие между текущими стратегиями теории категорий и предметов теории А:

• Центральная стратегия теории категорий имеет дело с равенством (когда вещи одинаковы, когда они различны и как они соотносятся друг с другом).

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

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

Приложения «TCS-A», которые приходят мне в голову, - это комбинаторный вид Джояла (обобщение степенных рядов на функторы для описания комбинаторных объектов, таких как деревья, множества, мультимножества и т. Д.) И формализация криптографического «скачкообразного изменения игры» с использованием реляционных вероятностная логика Хоара (работа Easycrypt, Certicrypt, Andreas Lochbihler). Хотя категории непосредственно не появляются в последних, они сыграли важную роль в разработке базовой логики (например, монады).

PS: Поскольку мое имя было упомянуто в первом ответе: использование расслоений группоидов, чтобы продемонстрировать недопустимость определенной аксиомы в теории типов Мартина-Лёфа Томасом Штрейхером и мной, также может считаться «солидным» использованием теории категорий (хотя и в логике или "TCS-B").

В более поздней книге « Семь набросков по композиционности» перечислено несколько приложений теории категорий в информатике и технике. Следует отметить главу о базах данных, где авторы описывают запросы, объединение, миграцию и развитие баз данных на основе категориальной модели. Авторы пошли дальше и разработали язык категориальных запросов (CQL) и интегрированную среду разработки (IDE) на основе своей категориальной модели баз данных.