![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
(no subject)
May. 29th, 2015 02:47 amТут пару часов назад появилась вот такая публикация: http://www.cse.chalmers.se/~coquand/vv.pdf. Я не совсем понял, это часом не конструкция фибрантной вселенной в CubTT?
May. 29th, 2015
Терминология в HoTT
May. 29th, 2015 05:42 pmМне очень нравится, когда в HoTT типы, удовлетворяющие UIP, называют просто утверждениями (mere proposition), и не нравится, когда просто propositions. Потому что утверждение, пригодное для экстракции из него, реалайзера, это всё ещё утверждение. Но конркетно сказать, что это уже "не просто утверждение".
И мне не нравится, что типы с тривиальной гомотопической структурой называют просто Sets, а не Mere(ly) Sets. Потому что тип неупорядоченных пар или там циклических списков тогда не входит в Set. А вот нефиг так делать, на нормальном человеческом языке это тоже Set, просто не Merely set, потому что у него есть дополнительная структура.
И ещё, чтобы два раза не вставать: когда в рамках HoTT формализуешь обыкновенную математику, очень хочется использовать обычный значок ∈ , вместо одинарных или двойных двоеточий, пришедших из мира естественной дедукции.
P.S. А ещё интересно, как бы сформировалась терминология, если бы малые категории, обобщающие структуру Х называли гетерогенными Х.
Просто категория, это стало быть, гетеромоноид.
Группоид — гетерогруппа.
Braided monoidal category — гетероалгебра.
Ну например множество всех матриц над тем или иным кольцом K это K-гетероалгебра.
С другой стороны, для больших категорий такие интуиции скорее вредны, чем полезны.
И мне не нравится, что типы с тривиальной гомотопической структурой называют просто Sets, а не Mere(ly) Sets. Потому что тип неупорядоченных пар или там циклических списков тогда не входит в Set. А вот нефиг так делать, на нормальном человеческом языке это тоже Set, просто не Merely set, потому что у него есть дополнительная структура.
И ещё, чтобы два раза не вставать: когда в рамках HoTT формализуешь обыкновенную математику, очень хочется использовать обычный значок ∈ , вместо одинарных или двойных двоеточий, пришедших из мира естественной дедукции.
P.S. А ещё интересно, как бы сформировалась терминология, если бы малые категории, обобщающие структуру Х называли гетерогенными Х.
Просто категория, это стало быть, гетеромоноид.
Группоид — гетерогруппа.
Braided monoidal category — гетероалгебра.
Ну например множество всех матриц над тем или иным кольцом K это K-гетероалгебра.
С другой стороны, для больших категорий такие интуиции скорее вредны, чем полезны.
Математические теории (хоть теорию групп, хоть теорию множеств) обычно рассматривают поверх логики предикатов, то есть, кроме значков теории считается что уже даны логические операторы ¬∨∧∀∃ и все аксиомы для них. Равенство и его аксиомы иногда тоже относят к ambient logic, а иногда вносят в теорию. Последнее, разумеется, более модулярный подход. Для удобства требование наличия структуры равенства вводят при помощи наследования, когда говорят "группа это множество, с такой-то дополнительной структурой", а в где-то в начале книжки написано, что "множество это структура, снабженная отношением равенства со всякими нужными свойствами.
Иногда ambient logic ослабляют до интуиционистской (фактически просто убирают одну аксиому), это ещё более модулярный подход, вместо одной структуры «колько» можно определить «разрешимое кольцо», которое ведёт себя точно как обычное (т.е. "аксиому" про исключённое третье превратили в часть определения кольца) и ещё две разновидности колец, с богатыми теориями. Это подход тоже повышает модулярность и оттого уже хорош. Ещё раз отмечу, что общности он не снижает: в классической логике для всех утверждений верен принцип исключённого третьего, а в интуиционистской мы рассматриваем как утверждения с этим свойством (т.н. разрешимые утверждения), так и иные, для которых это не обязательно так.
Чтобы ещё больше повысить модулярность, нужно ослабить ambient logic до линейной, тогда группы естественно обобщаются до "квантовых групп", решётки до кванталей и тому подобное. Но это значительно сложнее, чем просто убрать аксиомку, основная фича линейной логики в том, что нельзя так просто делать дубликаты сущностей, её можно делать только для специальных сущностей (т.н. значений), а вообще "бывают" материальные сущности типа электрона, фотона, ячейки памяти (в т.ч. квантового регистра) или файлхендла, с которыми так обращаться нельзя. Очень сложно переходить к такой ambient logic, т.к. математика очень привыкла работать только со значениями, и буквально везде значения клонируют и отбрасывают почём зря.
Давайте попытаемся разобрать, что это означает на практике, на примере групп. Группа это, значить, во-первых множество G с ассоциативной операцией композиции _·_, и нейтральным относительно неё элементом. На языке струнных диаграмм, это формулируется вот так:
(q) https://dkwise.wordpress.com/tag/weak-hopf-algebras/
Во вторых есть на нём операция $ нахождения обратного относительно композиции, то есть если взять x, построить $x, то x·$x = $x·x = e. Так, товарищи, что-то здесь, не то... Мы взяли один икс, потом изготовили из него $икс, значит исходного икса у нас вообще говоря не осталось, соответственно записать x·$x уже не получится! Каков же выход?
Выход заключается в том, чтобы сказать, что мы вообще умеем определять группы только если в их элементы умеют клонироваться, то есть наряду с операцией композиции типа G × G -> G, у нас должна быть операция дупликации: G -> G × G. Эта операция коассоциативна, т.е. если мы решим вместо пары попродить тройку, то сперва можно наклонировать пару, а потом склонировать любой из оставшихся элементов, всё равно какой. Кроме этого, надо как-то сформулировать, что каждый из новополучившихся элементов равен исходному, а для этого понадобится операция поглощения, чтобы можно было лишнюю копию снова отбросить: тогда подтверждение, что операция дупликации действительно копирует исходный элемент -- это просто аксиома о том, что если сначала склонировать, а потом один из элементов отбросить, то мы как бы ничего и не сделали:
Правда симпатично, что это в точности перевёрнутые диаграмы сверху? :-)
( Read more... )
Иногда ambient logic ослабляют до интуиционистской (фактически просто убирают одну аксиому), это ещё более модулярный подход, вместо одной структуры «колько» можно определить «разрешимое кольцо», которое ведёт себя точно как обычное (т.е. "аксиому" про исключённое третье превратили в часть определения кольца) и ещё две разновидности колец, с богатыми теориями. Это подход тоже повышает модулярность и оттого уже хорош. Ещё раз отмечу, что общности он не снижает: в классической логике для всех утверждений верен принцип исключённого третьего, а в интуиционистской мы рассматриваем как утверждения с этим свойством (т.н. разрешимые утверждения), так и иные, для которых это не обязательно так.
Чтобы ещё больше повысить модулярность, нужно ослабить ambient logic до линейной, тогда группы естественно обобщаются до "квантовых групп", решётки до кванталей и тому подобное. Но это значительно сложнее, чем просто убрать аксиомку, основная фича линейной логики в том, что нельзя так просто делать дубликаты сущностей, её можно делать только для специальных сущностей (т.н. значений), а вообще "бывают" материальные сущности типа электрона, фотона, ячейки памяти (в т.ч. квантового регистра) или файлхендла, с которыми так обращаться нельзя. Очень сложно переходить к такой ambient logic, т.к. математика очень привыкла работать только со значениями, и буквально везде значения клонируют и отбрасывают почём зря.
Давайте попытаемся разобрать, что это означает на практике, на примере групп. Группа это, значить, во-первых множество G с ассоциативной операцией композиции _·_, и нейтральным относительно неё элементом. На языке струнных диаграмм, это формулируется вот так:
(q) https://dkwise.wordpress.com/tag/weak-hopf-algebras/
Во вторых есть на нём операция $ нахождения обратного относительно композиции, то есть если взять x, построить $x, то x·$x = $x·x = e. Так, товарищи, что-то здесь, не то... Мы взяли один икс, потом изготовили из него $икс, значит исходного икса у нас вообще говоря не осталось, соответственно записать x·$x уже не получится! Каков же выход?
Выход заключается в том, чтобы сказать, что мы вообще умеем определять группы только если в их элементы умеют клонироваться, то есть наряду с операцией композиции типа G × G -> G, у нас должна быть операция дупликации: G -> G × G. Эта операция коассоциативна, т.е. если мы решим вместо пары попродить тройку, то сперва можно наклонировать пару, а потом склонировать любой из оставшихся элементов, всё равно какой. Кроме этого, надо как-то сформулировать, что каждый из новополучившихся элементов равен исходному, а для этого понадобится операция поглощения, чтобы можно было лишнюю копию снова отбросить: тогда подтверждение, что операция дупликации действительно копирует исходный элемент -- это просто аксиома о том, что если сначала склонировать, а потом один из элементов отбросить, то мы как бы ничего и не сделали:
Правда симпатично, что это в точности перевёрнутые диаграмы сверху? :-)
( Read more... )