Приложения алгебраической геометрии в теории типов / теории языка программирования

9

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

Я знаю, что алгебраическая топология имеет много применений в теории типов (теория гомотопических типов и многие другие), но как насчет алгебраической геометрии, кроме того, что и теория типов / теория PL, и AG являются хорошими мотиваторами теории категорий?

xrq
источник
1
Это не ответ на ваш вопрос, но алгебраическая топология также применяется в теории параллелизма. Взгляните на направленную гомотопию, и в Fossacs 2019 об этом тоже есть статья.
Хеннинг Базольд
Меня тоже интересует студент по компьютерному программированию и математике. Мой руководитель тополог. Но я хочу провести исследования в области математики, связанные с информатикой, такие как линейная алгебра. Мне нужна помощь для поиска темы моей диссертации, чтобы я мог проводить исследования в области теоретической информатики, но я не знаю, с чего мне начать. Нужна помощь по теме моей диссертации, чтобы я мог провести исследования в своей области.
Сайед Мухаммад Асад
@SyedMuhammadAsad Я также студент, поэтому я не тот человек, чтобы спросить. Вы должны проконсультироваться с некоторыми специалистами в этой области. Топология (особенно алгебраическая) имеет глубокие связи с теорией типов, поэтому вы можете начать с нее.
XRQ

Ответы:

10

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

  • Тьерри Кокванд, Анри Ломбарди. Логический подход к абстрактной алгебре .

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

  • Анри Ломбарди и Клод Куитте имеют (свободно доступный) учебник « Коммутативная алгебра: конструктивные методы» .

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

В этой области также есть ряд очень интересных кандидатских диссертаций:

  • Кандидатская диссертация Андреса Мёртберга « Формализация уточнений и конструктивная алгебра в теории типов»

    Если у вас есть конструктивное доказательство, у вас есть алгоритм. Этот тезис направлен на то, чтобы сделать эти алгоритмы эффективными.

  • Кандидатская диссертация Басселя Манны, семантика пучков в конструктивной алгебре и теории типов

    В этом тезисе он конструктивно доказывает правильность теоремы Ньютона-Пуазе и независимость принципа Маркова. Это хороший пример того, как семантические методы имеют применение как в геометрии, так и в логике.

  • Кандидатская диссертация Инго Блехшмидта « Использование внутреннего языка топосов в алгебраической геометрии»,

    Этот тезис рассматривает переделывание многих обычных доказательств алгебраической геометрии на внутреннем языке маленьких топов Зарисского, связанных со схемой, что дает своего рода «синтетическую алгебраическую геометрию». (Он также делает «теорию синтетических схем», используя большой топ Zariski). Как и следовало ожидать, поскольку topoi обычно не являются булевыми, доказательства должны быть выполнены в интуитивистском стиле.

Стоит также указать следующую ссылку:

Нил Кришнасвами
источник
6

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

Линейный цикл - это очень простая программа вида:

Иксзнак равноs

Пока ИксF

ИксAИкс

куда s,ИксQd а также AQd×dэто матрица НаборF является завершающим условием, которое может быть некоторым просто описанным множеством (например, многогранником или полуалгебраическим множеством).

Анализ этих циклов часто сводится к анализу орбиты матрицыAа именно {ANs:NN}, Это, в свою очередь, включает в себя анализ степеней собственных значенийA, поведение которого имеет тесную связь с понятиями в алгебраической геометрии (например, теорема Массера о базисе).

Вы можете взглянуть на статью «Сложность проблемы орбиты» как хорошую отправную точку.

Shaull
источник