Эффективный топос

В математике эффективный топос ${\mathsf {Eff}}$ предложенный Мартином Хайландом ( 1982 ), отражает математическую идею эффективности в рамках теории категорий .

Определение

Предварительные сведения

Реализуемость по Клини

Топос алгебре , основан на частичной комбинаторной заданной Клини . первой алгеброй ${\mathcal {K}}_{1}$. Клини В понятии рекурсивной реализуемости любому предикату присваивается реализация чисел, то подмножества есть ${\mathbb {N} }$. Экстремальные предложения – это $\top$ и $\bot$, реализованный ${\mathbb {N} }$ и $\{\}$. Однако в целом этот процесс присваивает предложению больше данных, чем просто двоичное значение истинности.

Формула с $k$ свободные переменные приведут к появлению карты в $({\mathcal {P}}{\mathbb {N} })^{{\mathbb {N} }^{k}}$ значениями которых является подмножество соответствующих реализаторов.

Топосы реализуемости

${\mathsf {Eff}}$ является ярким примером топоса реализуемости . Это класс элементарных топосов с интуиционистской внутренней логикой и реализующих форму зависимого выбора . Как правило, это не топосы Гротендика.

В частности, эффективный топос ${\mathsf {RT}}({\mathcal {K}}_{1})$. Можно сказать, что другие конструкции топоса реализуемости абстрагируют некоторые аспекты, которые играют ${\mathbb {N} }$ здесь.

Описание Eff

Объекты представляют собой пары. $\langle X,E_{X}\rangle$ множеств вместе с симметричным и транзитивным отношением в $({\mathcal {P}}{\mathbb {N} })^{X\times X}$, представляющий собой форму предиката равенства, но принимающий значения в подмножествах $\mathbb {N}$. Один пишет $E_{X}(x)$ всего лишь с одним аргументом для обозначения так называемого предиката существования, выражающего, как $x$ относится к самому себе. Оно может быть пустым, и поэтому отношение обычно не является рефлексивным .Стрелки соответствуют классам эквивалентности функциональных отношений, соответствующим образом соблюдающих определенные равенства.

Классификатор ​ составляет ${\mathcal {P}}{\mathbb {N} }$. Пара (или, если злоупотреблять обозначениями, просто базовый набор полномочий) можно обозначить как $\Omega$. Отношение следствия $\vdash _{X}$ на ${\mathcal {P}}{\mathbb {N} }^{X}$ превращает ее в предалгебру Гейтинга . Такой контекст позволяет определить соответствующую решетчатую логическую структуру с логическими операциями, заданными в терминах операций наборов реализателей, с использованием пар и вычислимых функций.

Терминальный объект является синглтоном $\langle \{*\},E_{\{*\}}\rangle$ с тривиальным предикатом существования ( ${\mathbb {N} }$). Конечный продукт соответствующим образом соблюдает равенство.Равенство классификатора $E_{{\mathcal {P}}{\mathbb {N} }}$ задается через эквивалентности в его решетке.

Свойства

Связь с наборами

Некоторые объекты демонстрируют довольно тривиальный предикат существования, зависящий только от действительности отношения равенства» $=$" множеств, так что действительное равенство сопоставляется с верхним набором $\mathbb {N}$ и отверг карты равенства $\{\}$. Это порождает полный и точный функтор $\nabla \colon {\mathsf {Sets}}\to {\mathsf {Eff}}$ вне категории множеств , которая имеет конечные пределы, сохраняющие функтор глобальных сечений $\Gamma$ как его левосопряженный.Это происходит за счет сохранения конечного предела, полного и точного вложения. $\omega$- ${\mathsf {Sets}}\to {\mathsf {Eff}}$.

НЕТ

Топос имеет объект натуральных чисел. $N=\langle {\mathbb {N} },E_{\mathbb {N} }\rangle$ просто $E_{\mathbb {N} }(n)=\{n\}$.Верные предложения о $N$ являются в точности рекурсивно реализованными предложениями арифметики Гейтинга ${\mathsf {HA}}$.

Теперь стрелки $N\to N$ можно понимать как полностью рекурсивные функции, и это также справедливо для внутренних функций. $N^{N}$. Последняя представляет собой пару, заданную тотально рекурсивными функциями $\mathrm {TR}$ и такое отношение, что $E_{\mathrm {TR} }(f)$ это набор кодов $e\in {\mathbb {N} }$ для $f$. Последний представляет собой подмножество натуральных чисел, а не просто одиночный элемент, поскольку существует несколько индексов, вычисляющих одну и ту же рекурсивную функцию. Итак, здесь вторая запись объектов представляет собой реализующие данные.

С $N$ и функций из него и в него, а также с простыми правилами отношений равенства при формировании конечных произведений $\times$, теперь можно более широко определить наследственно эффективные операции.Опять же, можно подумать о функциях в $N^{N}$ как задано индексами, и их равенство определяется объектами, которые вычисляют одну и ту же функцию. Это равенство явно накладывает ограничение на $N^{(N^{N})}$, поскольку эти функции оказываются только теми вычислимыми функциями, которые также должным образом соблюдают упомянутое равенство в своей области определения. И так далее.Ситуация в целом $\langle X,E_{X}\rangle \to \langle Y,E_{Y}\rangle$, равенство (в смысле $E$х) домен и изображение должны соблюдаться.

Свойства и принципы

Таким образом, можно подтвердить принцип Маркова. ${\mathrm {MP} }$ и принцип расширенной Церкви ${\mathrm {ECT} }_{0}$ (и его вариант второго порядка), которые сводятся к простому утверждению об объекте, например $N^{N}$ или $(1+1)^{N}$. Это подразумевает ${\mathrm {CT} }_{0}$ и независимость помещения ${\mathrm {IP} }_{0}$.

Принцип выбора $N^{N}$ связанная с Брауэровской слабой непрерывностью, терпит неудачу.От любого объекта имеется только счетное число стрелок, $N$. $\Omega ^{N}$ соответствует принципу единообразия. $N$ не является счетным копроизведением копий $1$. Этот топос не является категорией пучков.

Анализ

Объект $\langle {\mathbb {Q} }^{\mathbb {N} },E_{{\mathbb {Q} }^{\mathbb {N} }}\rangle$ является эффективным в формальном смысле и на его основе можно определить вычислимые последовательности Коши . Через частное топос имеет объект действительных чисел, у которого нет нетривиального разрешимого подобъекта. При выборе понятие реалов Дедекинда совпадает с понятием Коши.

Свойства и принципы

Анализ здесь соответствует рекурсивной школе конструктивизма. Он отвергает утверждение, что $x\leq 0\lor 0\leq x$ будет справедливым для всех реалий $x$. Формулировки теоремы о промежуточном значении не работают, и все функции от вещественных чисел до вещественных чисел являются доказанно непрерывными . Последовательность Спекера существует, и тогда последовательность Больцано-Вейерштрасса терпит неудачу.

См. также

• Категорическая логика

Ссылки

• Хайланд, JME (1982), «Эффективный топос» (PDF) , в Троелстре, AS; Дален, Д. ван (ред.), Симпозиум столетия Л. Дж. Брауэра (Нордвейкерхаут, 1981) , Исследования по логике и основам математики, том. 110, Амстердам: Северная Голландия, стр. 165–216, doi : 10.1016/S0049-237X(09)70129-6 , ISBN.  978-0-444-86494-9 , МР   0717245
• Клини, Южная Каролина (1945). «Об интерпретации интуиционистской теории чисел». Журнал символической логики . 10 (4): 109–124. дои : 10.2307/2269016 . JSTOR   2269016 . S2CID   40471120 .
• Фоа, Уэсли (1992). Введение в расслоения, теорию топоса, эффективный топос и скромные множества (Технический отчет). Лаборатория основ компьютерных наук Эдинбургского университета. CiteSeerX   10.1.1.112.4533 . ECS-LFCS-92-208.
• Бернадетт, Алексис; Грэм-Ленгранд, Стефан (2013). «Простое представление эффективного топоса». arXiv : 1307.3832 [ cs.LO ].
• Корфилд, Дэвид; Рамеш, Шридхар; Шрайбер, Урс; Бартельс, Тоби; Шкода, Зоран; Шульман, Майк; Тримбл, Тодд; Робертс, Дэвид; Холдер, Томас (22 января 2023 г.) [10 июля 2009 г.], эффективный топос (19-е изд.), nLab