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