В математике сетоид ( X , ~) — это множество ( или тип ) X , снабженное отношением эквивалентности ~. Setoid также может называться E-set , Bishop set или extensional set . [1]
Сетоиды изучаются особенно в теории доказательств и в теоретико-типовых основах математики . Часто в математике, когда кто-то определяет отношение эквивалентности на наборе, он сразу же формирует фактор-множество (превращая эквивалентность в равенство ). Напротив, setoids можно использовать, когда необходимо сохранить различие между тождеством и эквивалентностью, часто с интерпретацией интенсионального равенства (равенство на исходном множестве) и экстенсионального равенства (отношение эквивалентности или равенство на частном множестве).
В теории доказательств, особенно в теории доказательств конструктивной математики , основанной на соответствии Карри-Ховарда , математическое утверждение часто отождествляется с его набором доказательств (если таковые имеются). У данного предложения, конечно, может быть много доказательств; в соответствии с принципом нерелевантности доказательства обычно имеет значение только истинность предложения, а не то, какое доказательство было использовано. Однако соответствие Карри-Ховарда может превратить доказательства в алгоритмы , и различия между алгоритмами часто важны. Таким образом, сторонники теории доказательств могут предпочесть отождествлять пропозицию с setoid.доказательств, считая доказательства эквивалентными, если они могут быть преобразованы друг в друга посредством бета-преобразования или т.п.
В теоретико-типовых основаниях математики множества могут использоваться в теории типов, в которой отсутствуют частные типы для моделирования общих математических множеств. Например, в интуиционистской теории типов Пера Мартина-Лёфа нет типа действительных чисел , есть только тип регулярных последовательностей Коши рациональных чисел . Таким образом, чтобы провести настоящий анализ в рамках Мартина-Лёфа, нужно работать с setoid.действительных чисел, типа регулярных последовательностей Коши, снабженных обычным понятием эквивалентности. Предикаты и функции действительных чисел необходимо определить для регулярных последовательностей Коши и доказать их совместимость с отношением эквивалентности. Обычно (хотя это зависит от используемой теории типов) аксиома выбора будет выполняться для функций между типами (интенсиональные функции), но не для функций между сетоидами (экстенсиональные функции). [ требуется разъяснение ] Термин «набор» по-разному используется либо как синоним «типа», либо как синоним «сетоид». [2]
В конструктивной математике часто берут сетоид с отношением обособленности вместо отношения эквивалентности, который называется конструктивным сетоидом. Иногда также рассматривают частичный сетоид, используя отношение частичной эквивалентности или частичное разделение. (см., например, Barthe et al. , раздел 1)