В математике эффективный топос, введенный Мартином Хайлендом (1982), отражает математическую идею эффективности в рамках теории категорий .
Топос основан на частичной комбинаторной алгебре , заданной первой алгеброй Клини . В понятии рекурсивной реализуемости Клини любому предикату назначаются реализующие числа, т. е. подмножество . Экстремальными предложениями являются и , реализуемые посредством и . Однако в целом этот процесс назначает предложению больше данных, чем просто двоичное значение истинности.
Формула со свободными переменными приведет к отображению, в значениях которого находится подмножество соответствующих реализаторов.
является ярким примером топоса реализуемости . Это класс элементарных топосов с интуиционистской внутренней логикой и выполняющих форму зависимого выбора . Они, как правило, не являются топосами Гротендика.
В частности, эффективный топос — это . Можно сказать, что другая конструкция топоса реализуемости абстрагирует некоторые аспекты, которые здесь играют.
Объекты представляют собой пары множеств вместе с симметричным и транзитивным отношением в , представляющие форму предиката равенства, но принимающие значения, которые являются подмножествами . Пишется только с одним аргументом для обозначения так называемого предиката существования, выражающего, как относится к себе. Он может быть пустым, выражая отношение, которое, как правило, не является рефлексивным . Стрелки равны классам эквивалентности функциональных отношений, соответствующим образом соблюдающим определенные равенства.
Классификатор равен . Пара (или, злоупотребляя обозначением, просто этот базовый набор полномочий) может быть обозначена как . Отношение вывода на превращает его в предалгебру Гейтинга . Такой контекст позволяет определить соответствующую решетчатую логическую структуру с логическими операциями, заданными в терминах операций множеств реализатора, с использованием пар и вычислимых функций.
Конечный объект — это синглтон с тривиальным предикатом существования (т.е. равный ). Конечное произведение соответствующим образом соблюдает равенство. Равенство классификатора дается через эквивалентности в его решетке.
Некоторые объекты демонстрируют довольно тривиальный предикат существования, зависящий только от действительности отношения равенства " " множеств, так что действительное равенство отображается в верхний набор , а отклоненное равенство отображается в . Это приводит к полному и точному функтору из категории множеств , который имеет функтор глобальных сечений, сохраняющий конечные пределы, в качестве своего левого сопряженного. Это факторизуется через сохраняющее конечные пределы, полное и точное вложение - .
Топос имеет объект натуральных чисел с просто . Предложения, истинные относительно которых, являются в точности рекурсивно реализованными предложениями арифметики Гейтинга .
Теперь стрелки можно понимать как общие рекурсивные функции, и это также выполняется внутренне для . Последнее является парой, заданной общими рекурсивными функциями и отношением таким, что является набором кодов для . Последнее является подмножеством натуральных чисел, но не просто синглтоном, поскольку существует несколько индексов, вычисляющих одну и ту же рекурсивную функцию. Таким образом, здесь вторая запись объектов представляет реализующие данные.
С и функциями из и в него, а также с простыми правилами для отношений равенства при формировании конечных произведений , теперь можно более широко определить наследственно эффективные операции. Опять же можно думать о функциях в как заданных индексами, и их равенство определяется объектами, которые вычисляют ту же функцию. Это равенство явно накладывает ограничение на , поскольку эти функции оказываются только теми вычислимыми функциями, которые также должным образом соблюдают упомянутое равенство в своей области определения. И так далее. Ситуация для общего , равенство (в смысле 's) в области определения и образе должно соблюдаться.
При этом можно подтвердить принцип Маркова и расширенный принцип Чёрча (и его вариант второго порядка), которые сводятся к простому утверждению об объекте, таком как или . Они подразумевают и независимость посылок .
Принцип выбора, связанный со слабой непрерывностью Брауэра, не работает. Из любого объекта есть только счетное число стрелок к . удовлетворяет принципу однородности. не является счетным копроизведением копий . Этот топос не является категорией пучков.
Объект эффективен в формальном смысле и из него можно определить вычислимые последовательности Коши . Через фактор топос имеет объект вещественных чисел, который не имеет нетривиального разрешимого подобъекта. При выборе понятие дедекиндовых вещественных чисел совпадает с понятием Коши.
Анализ здесь соответствует рекурсивной школе конструктивизма. Он отвергает утверждение, которое было бы справедливо для всех вещественных чисел . Формулировки теоремы о промежуточном значении неверны, и все функции от вещественных чисел до вещественных чисел доказано непрерывны . Последовательность Шпеккера существует, и тогда Больцано-Вейерштрасс неверна.
