В математике , А setoid ( Х , \) представляет собой набор (или типа ) Х оборудован отношение эквивалентности \. Сетоид также может называться E-набором , набором Бишопа или экстенсиональным набором . [1]
Сетоиды особенно изучаются в теории доказательств и теоретико-типовых основаниях математики . Часто в математике, когда кто-то определяет отношение эквивалентности на множестве, он немедленно формирует фактор-множество (превращая эквивалентность в равенство ). Напротив, сетоиды могут использоваться, когда необходимо поддерживать различие между идентичностью и эквивалентностью, часто с интерпретацией интенсионального равенства (равенство на исходном множестве) и экстенсионального равенства (отношение эквивалентности или равенство на факторном множестве).
Теория доказательств [ править ]
В теории доказательств, особенно в теории доказательств конструктивной математики, основанной на соответствии Карри – Ховарда , часто отождествляют математическое предложение с его набором доказательств (если таковые имеются). У данного предложения, конечно, может быть много доказательств; согласно принципу неуместности доказательства , обычно имеет значение только истинность предложения, а не то, какое доказательство было использовано. Однако соответствие Карри – Ховарда может превращать доказательства в алгоритмы , и различия между алгоритмами часто важны. Таким образом, теоретики доказательства могут предпочесть отождествлять предложение с сетоидом.доказательств, считая доказательства эквивалентными, если они могут быть преобразованы друг в друга посредством бета-преобразования или подобного.
Теория типов [ править ]
В теоретико-типовых основах математики сетоиды могут использоваться в теории типов, в которой отсутствуют факторные типы для моделирования общих математических множеств. Например, в Per Martin-LOF «s интуиционистской теории типов , не существует типа действительных чисел , только типа регулярных последовательностей Кошей из рациональных чисел . Следовательно, чтобы провести реальный анализ в рамках Мартина-Лёфа, нужно работать с сетоидом.действительных чисел, тип регулярных последовательностей Коши, снабженных обычным понятием эквивалентности. Для регулярных последовательностей Коши необходимо определить предикаты и функции действительных чисел и доказать их совместимость с отношением эквивалентности. Обычно (хотя это зависит от используемой теории типов) выбранная аксиома будет выполняться для функций между типами (интенсиональные функции), но не для функций между сетоидами (экстенсиональные функции). [ требуется пояснение ] Термин «набор» по-разному используется либо как синоним «типа», либо как синоним «сетоида». [2]
Конструктивная математика [ править ]
В конструктивной математике часто используется сетоид с отношением обособленности вместо отношения эквивалентности, называемый конструктивным сетоидом. Иногда также рассматривают частичный сетоид, используя отношение частичной эквивалентности или частичной обособленности. (см., например, Barthe et al. , раздел 1)
См. Также [ править ]
Заметки [ править ]
- ^ Александр Буисс, Питер Дайбьер, «Интерпретация интуиционистской теории типов в локально декартовых закрытых категориях - интуиционистская перспектива» , Электронные заметки в теоретической информатике 218 (2008) 21–32.
- ^ "Теория множеств Бишопа" (PDF) : 9. Cite journal requires
|journal=(help)
Ссылки [ править ]
- Хофманн, Мартин (1995), «Простая модель для факторных типов», Типизированные лямбда-исчисления и приложения (Эдинбург, 1995) , Конспекты лекций в Comput. Sci . , 902 , Берлин:. Springer, С. 216-234, CiteSeerX 10.1.1.55.4629 , DOI : 10.1007 / BFb0014055 , ISBN 978-3-540-59048-4, MR 1477985.
- Барт, Жиль; Капретта, Венанцио; Pons, Оливье (2003), "Setoids в теории типа" (PDF) , журнал функционального программирования , 13 (2): 261-293, DOI : 10,1017 / S0956796802004501 , MR 1985376.
Внешние ссылки [ править ]
- Реализация сетоидов в Coq
- Setoid в nLab
- Епископ установлен в nLab
