Comments 15
Очень интересно, спасибо!
Мы не будем рассматривать множества
и
как одинаковые
Тут нюанс - а как же их рассматривать если принадлежность любому из них сводится к рассмотрению предложения 
? И получится, что этим двум множествам принадлежат одни и те же объекты. Т.е., то же самое, вроде термы 
и 
различны, но равенство троек дает одно и то же логическое предложение. Если же рассматривать декартово произведение как множество отображений из 
в 
, с свойством покоординатной принадлежности, то это вообще одно и то же, так, как 
. Так, что может не зря их считают за одно и то же - это и есть одно и то же.
Эээ, смотрите, вот у вас есть универсальное правило, как для кортежей строить предикаты принадлежности. Вы в своём примере два раза применили это правило к разным кортежам, и да, полученные предикаты логически равны. Но правила принадлежности типу недостаточно, оно вообще нужно только на этапе проверки корректности типизации программы. Для составных типов смысл существования - в деструктуризации: получить i-ый элемент кортежа, например. И в вашем примере у этих элементов будут разные типы.
Думаю я понял вас, но дело в том, что тогда вы не рассматриваете просто множества. Для простого математического множества есть только отношение принадлежности: для любого терма он или принадлежит данному множеству или нет. И в этом рассмотрении декатровы тройки равны. Но, разумеется, можно создать более сложную структуру - допустим какое-то "множество с типами" и с ним уже делать различия. Вот интересно как вы это формально определите. В принципе, я уверен, это должно быть уже сделанно в каком-нибудь раннем источнике.
И в этом рассмотрении декатровы тройки равны.
Только их не существует (особенно если рассматривать «просто множества»).
По крайней мере, не существует в ZF. В ZF нет ни пар, ни троек, ни других n-туплов как примитивов, там есть только множества. Пары там определяются как, упрощая, синтаксический шорткат: например, можно определить 
(и дальше в ZF можно доказать, что это определение ведёт себя как ожидается, вроде 
), или как 
(это эквивалентное определение, но ему ЕМНИП не нужна аксиома регулярности из ZF).
Соответственно, пара 
и пара 
— это сильно разные множества. И 
вместе с 
— это тоже сильно разные множества (которые в ZF строятся такими-то костылями, и данные вами в прошлом комментарии логические формулы не имеют прямого отношения к определению этих множеств, хотя их и можно получить после упрощения, но β-эквивалентность — это не синтаксическое равенство). Но, конечно, в школьной (и прикладной вузовской) математике никто не вспоминает про ZF или другие основания математики, поэтому там это всё неважно, и можно интуитивно считать эти множества одинаковыми.
В теоркате, кстати, декартовых произведений может быть (бесконечно) много (например, в Set A×B — это и множество пар
вместе с двумя очевидными проекциями, и множество 
с теми же проекциями, но наоборот, и множество 
с чуть менее очевидными проекциями), поэтому их там тоже обычно рассматривают с точностью до изоморфизма.
Но, разумеется, можно создать более сложную структуру - допустим какое-то "множество с типами" и с ним уже делать различия. Вот интересно как вы это формально определите. В принципе, я уверен, это должно быть уже сделанно в каком-нибудь раннем источнике.
Теория типов, собсна, уже тоже придумана. Что-нибудь в духе Мартина-Лёфа будет выглядеть примерно как:
Постулируем существование конструктора типов ×: A : Type, B : Type ⊢ A × B : Type
Постулируем конструктор термов ⟨⟩: a : A, b : B ⊢ ⟨a, b⟩ : A × B
Постулируем элиминатор. Если не вскрывать тему с зависимыми типами и зависимыми элиминаторами, то проще всего через проекции:
A × B : Type ⊢ π₁ : A × B → A
A × B : Type ⊢ π₂ : A × B → BПостулируем операционную семантику:
π₁ (⟨ a, b ⟩) ⇝ a
π₂ (⟨ a, b ⟩) ⇝ bВ зависимости от конкретной теории типов (экстенсиональная/интенсиональная, есть ли UIP, всякое такое вот) может быть полезно постулировать η-равенство: ∀ p : A × B. ⟨ π₁ p, π₂ p ⟩ ≡ p.
Кстати, даже тут уже, если присмотреться, видны намёки на некоторые проблемы с единственностью, пусть и слегка другого рода.
Дальше ещё изоморфизм ∀ X. (X → A × B) ≅ (X → A) × (X → B), который по факту выражает привычное универсальное свойство произведений.
У автора этой статьи есть прекрасное свойство - он приводит источники. Я пишу следуя известной монографии Nicolas Bourbaki "Theory of Sets" Springer-Verlag Berlin Heidelberg 2004. Есть и русский перевод, например, Бурбаки Н. - Основные структуры анализа. Теория множеств., Мир, 1965. Там, кстати, невероятные опечатки, так, что давайте сопоставлять с английской версией. Среди определенного круга математиков эта книга сегодня не пользуется популярностью, позвольте не погружаться в причины. Мне важен, в этой книге, точный подход, что подразумевает построение математики с нулю - с понятия алфавита и знакосочетаний из этого алфавита. Не подразумевается знание предварительных математических понятий, например даже кванторов, которые не определяются в других монографиях или называются первичными элементами или примитивами. Для нашего разговора важно, что построенная Бурбаками система является эквивалентной ZF. Кстати а какую монографию/источник вы имеете ввиду, говоря о фактах из ZF?
Так вот, на странице 72 [2004], стр. 82 [1965], вводится понятие пары с помошью специального субстантивного (substantific) знака. Так, что если U и T термы, то (U, T) также терм для которого вводится аксиома пары. Определение аксиомы на стр. 24 [2004], стр. 40 [1965]. И декартово произведение прекрасно существует стр. 74 [2004], стр. 83 [1965]. Кстати, определение существования стр. 36 [2004], стр. 53 [1965].
Таким образом все приведенные мной формулы и утверждения верны по этой монографии. Никаких костылей и равенство это реляциооный знак веса 2 в эгалитарной теории.
Далее, если, по вашему, можно ввести понятие пары используя множество, т.е. пары Куратовского (Н. К. Верещагин, А.Шень НАЧАЛА ТЕОРИИ МНОЖЕСТВ Москва Издательство МЦНМО, 2012, стр. 36), то разве это означает, что пара не существует? В каком источнике по ZF вы это видели? и что означает по вашему не "существует"? Опять-таки интересен источник.
Кстати, в вики https://ru.wikipedia.org/wiki/Упорядоченная_пара полный бедлам: всего два предложения и одно по Куратовскому, другое по Бурбакам.
У автора этой статьи есть прекрасное свойство - он приводит источники.
Для исторического обзора это естественно. Для обзора по самой математике это не очень естественно, потому что мало кто говорит «ах, сложение коммутативно? приведите ваши источники!»
Так вот, на странице 72 [2004], стр. 82 [1965], вводится понятие пары с помошью специального субстантивного (substantific) знака. Так, что если U и T термы, то (U, T) также терм для которого вводится аксиома пары.
Тогда это не ZF, только и всего. Можете работать в этой формальной системе, никто не против, но тогда, по идее, вы должны понимать, что в некоторых других формальных системах (которые, похоже, принимаются по умолчанию) этой аксиомы нет, поэтому ваше рассуждение там не работает.
Кстати, мне лень читать Бурбаки — вводится ли там аналогично фундаментальное понятие тройки? Вводится ли там аналогично фундаментальное понятие произвольного кортежа, индексированного произвольным множеством (чтобы можно было определить декартово произведение произвольного семейства множеств)? Как упорядоченность (и декартовы произведения) работает, когда индексирующее множество несчётно и вообще произвольное? Не вылезает там вдобавок к ZF ещё и C?
то разве это означает, что пара не существует? и что означает по вашему не "существует"?
Это означает, что пара не существует как примитив — для этого достаточно прочитать следующее же предложение (поясняющее предыдущее).
После этого момента типы-суммы исчезают из императивного программирования. В императивных языках конца XX века доминировало влияние Pascal и C. В Pascal не было типов-сумм, потому что Вирт считал их менее гибкими, чем не размеченные (untagged) объединения.
Не специалист по этому всему, но в Pascal же чуть ли не с рождения были variant records? Википедия считает что это и есть tagged unions https://en.wikipedia.org/wiki/Tagged_union#1970s_&_1980s
В C, возможно, нет типов-сумм, потому что его создатели заимствовали систему типов из языка PL/I от IBM
В C тоже можно сделать tagged unions "на коленке", но нужно следить вручную за тегами. В телекомах это вообще такая классика, используется в куче протоколов и есть даже специальный термин TLV (type-length-value / tag-length-value) https://en.wikipedia.org/wiki/Type–length–value
Насколько мне известно, ни в одной реализации Паскаля теги фактически не проверялись. Возможно, дело в этом.
Да, Вирт их добавил, но видимо не до конца поверил в их безопасность. В итоге получился компромисс: тег есть, но его проверка на совести программиста, а мы знаем, к чему это приводит) Именно поэтому в функциональных языках, где проверка исчерпываемости это киллер-фича, типы-суммы и взлетели
Неплохой перевод интересного материала.
Я глянул страничку автора книги. Он, конечно, молодец, но 30 долларов за 162 страницы мне было бы жмотно заплатить.
Для большинства вся эта история просто забавный факт, мы используем struct и enum не особо задумываясь почему они так называются
Но вот эта детективная работа по поиску первоисточников, когда показывается как за каждой строчкой кода, за каждым ключевым словом, стоит чья-то мысль, чья-то научная работа, написанная 60 лет назад - это круто
Алгебра предполагает кроме операций и нейтральные элементы для этих операций, 0 для сложения и 1 для произведения.
Статья не полна без затрагивания единичного типа unit type, нейтрального для типа-произведения и нулевого типа never type нейтрального для типа-суммы в Rust именно они позволяют полностью замкнуть алгебраическую систему типов с целью, с которой она задумывалась - доказать корректность программ, о чем мечтал Дейкстра, соответственно на примере Rust:
Unit type - () и struct Foo;
Never type - ! и enum Foo {};
Требую рассмотреть!
чисто технически, есть ведь ещё и типы-степени (функции)… сосредотачиваться лишь на суммах и произведениях — не так хорошо, я полагаю, но как бы с другой стороны, функции должны быть даже в тех япах, где нету структур… немного спускаясь в полуфилософскую шутливость, операции открылись словно наоборот от классической алгебры. если конечно не вспоминать о first class – функциях и замыканиях…
Ранняя история алгебраических типов данных