Сетоид
В математике сетоид , ( X , ~) — это множество (или тип ) X снабженное отношением эквивалентности ~. Сетоид также можно назвать E-множеством , Бишопа множеством или экстенсиональным множеством . [1]
Сетоиды изучаются особенно в теории доказательств и в теоретико-типовых основах математики . Часто в математике, когда кто-то определяет отношение эквивалентности на множестве, он сразу же формирует фактормножество ( превращая эквивалентность в равенство ). Напротив, сетоиды могут использоваться, когда необходимо сохранить разницу между идентичностью и эквивалентностью, часто с интерпретацией интенсионального равенства (равенство в исходном наборе) и экстенсионального равенства (отношение эквивалентности или равенство в фактормножестве).
Теория доказательств [ править ]
В теории доказательств, особенно в теории доказательств конструктивной математики, основанной на соответствии Карри-Ховарда , часто отождествляют математическое утверждение с его набором доказательств (если таковые имеются). Разумеется, данное предложение может иметь множество доказательств; Согласно принципу нерелевантности доказательства , обычно имеет значение только истинность утверждения, а не то, какое доказательство было использовано. Однако соответствие Карри-Ховарда может превратить доказательства в алгоритмы , и различия между алгоритмами часто имеют важное значение. Таким образом, теоретики доказательства могут предпочесть отождествить предложение с сетоидом доказательств, считая доказательства эквивалентными, если они могут быть преобразованы друг в друга посредством бета-конверсии или тому подобного.
Теория типов [ править ]
В теоретико-типовых основах математики сетоиды могут использоваться в теории типов, в которой отсутствуют фактортипы для моделирования общих математических множеств. Например, в Пера Мартина-Лёфа не интуиционистской теории типов существует типа действительных чисел , а есть только тип регулярных последовательностей Коши рациональных чисел . Поэтому, чтобы провести реальный анализ в рамках Мартина-Лёфа, нужно работать с сетоидом действительных чисел, типом регулярных последовательностей Коши, снабженных обычным понятием эквивалентности. Предикаты и функции действительных чисел необходимо определить для регулярных последовательностей Коши и доказать их совместимость с отношением эквивалентности. Обычно (хотя это зависит от используемой теории типов) аксиома выбора справедлива для функций между типами (интенсиональные функции), но не для функций между сетоидами (экстенсиональные функции). [ нужны разъяснения ] Термин «множество» по-разному используется либо как синоним «типа», либо как синоним «сетоида». [2]
Конструктивная математика [ править ]
В конструктивной математике часто берут сетоид с отношением обособленности вместо отношения эквивалентности , называемый конструктивным сетоидом. Иногда также рассматривают частичный сетоид, используя отношение частичной эквивалентности или частичной обособленности (см., например, Барт и др. , раздел 1).
См. также [ править ]
Примечания [ править ]
- ^ Александр Буиссе, Питер Дюбьер, «Интерпретация интуиционистской теории типов в локально декартовых замкнутых категориях — интуиционистская перспектива» , Electronic Notes in Theoretical Computer Science 218 (2008) 21–32.
- ^ «Теория множеств Бишопа» (PDF) . п. 9.
Ссылки [ править ]
- Хофманн, Мартин (1995), «Простая модель для фактор-типов», Типизированные лямбда-исчисления и приложения (Эдинбург, 1995) , Конспекты лекций по вычислениям. наук, том. 902, Берлин: Springer, стр. 216–234, CiteSeerX 10.1.1.55.4629 , doi : 10.1007/BFb0014055 , ISBN. 978-3-540-59048-4 , МР 1477985 .
- Барт, Жиль; Капретта, Венанцио; Понс, Оливье (2003), «Сетоиды в теории типов» (PDF) , Журнал функционального программирования , 13 (2): 261–293, doi : 10.1017/S0956796802004501 , MR 1985376 , S2CID 10069160 .
