Войти
В математике, a setoid (X, ~) - это set (или тип ) X, снабженный отношением эквивалентности ~. Сетоид также может называться E-набор, Бишоп набор или экстенсиональный набор .
Сетоиды изучаются особенно в теории доказательств и в теоретико-типовые основы математики. Часто в математике, когда кто-то определяет отношение эквивалентности на множестве, он немедленно формирует фактормножество (превращая эквивалентность в равенство ). Напротив, сетоиды могут использоваться, когда необходимо поддерживать различие между идентичностью и эквивалентностью, часто с интерпретацией интенсионального равенства (равенства на исходном наборе) и экстенсионального равенства ( отношение эквивалентности, или равенство на фактормножестве).
В теории доказательств, особенно в теории доказательств конструктивной математики, основанной на соответствии Карри – Ховарда, часто отождествляют математическое суждение с его набор доказательств (при наличии). Конечно, у данного предложения может быть много доказательств; согласно принципу, обычно имеет значение только истинность предложения, а не то, какое доказательство было использовано. Однако соответствие Карри – Ховарда может превратить доказательства в алгоритмы, и различия между алгоритмами часто важны. Таким образом, теоретики доказательства могут предпочесть отождествлять предложение с множеством доказательств, считая доказательства эквивалентными, если они могут быть преобразованы друг в друга посредством бета-преобразования или подобного.
В теоретико-типовых основах математики сетоиды могут использоваться в теории типов, в которой отсутствуют факторные типы для моделирования общих математических множеств. Например, в интуиционистской теории типов Пер Мартина-Лёфа нет типа действительных чисел, есть только тип регулярных последовательностей Коши. из рациональных чисел. Следовательно, чтобы выполнить реальный анализ в рамках Мартина-Лёфа, нужно работать с множеством действительных чисел, типом регулярных последовательностей Коши, снабженных обычным понятием эквивалентности. Для регулярных последовательностей Коши необходимо определить предикаты и функции действительных чисел и доказать их совместимость с отношением эквивалентности. Обычно (хотя это зависит от используемой теории типов) аксиома выбора будет выполняться для функций между типами (интенсиональные функции), но не для функций между сетоидами (экстенсиональные функции). Термин «множество» по-разному используется либо как синоним «типа», либо как синоним «сетоида».
В конструктивной математике один часто используется сетоид с отношением отделенности вместо отношения эквивалентности, называемый конструктивным сетоидом. Иногда также рассматривают частичный сетоид с использованием отношения частичной эквивалентности или частичного обособления. (см., например, Barthe et al., раздел 1)
| journal =()