От теории множеств к теории типов
Jan. 8th, 2013 02:50 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо
alexey_rom за ссылку.
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
no subject
Date: 2013-01-08 09:10 am (UTC)no subject
Date: 2013-01-08 09:25 am (UTC)no subject
Date: 2013-01-08 05:20 pm (UTC)no subject
Date: 2013-01-08 04:31 pm (UTC)no subject
Date: 2013-01-09 02:17 pm (UTC)Но зато "у них" какая-то фигня с функторами должна получаться, ибо теперь он должен различать BA?
no subject
Date: 2013-01-09 02:39 pm (UTC)А что такое "различать B^A"?
no subject
Date: 2013-01-09 04:56 pm (UTC)Конечно, о функторе я вспоминаю только потому, что в программировании он есть, значит, в теории типов тоже должен как-то быть.
no subject
Date: 2013-01-09 05:23 pm (UTC)Функции с двумя параметрами могут быть классически представлены стрелками в экспоненты x → (y→z), ну или стрелка x → (z^y).
Можно раскрыть и поточечный взгляд, согласно которому, мы постоянно отслеживаем композиции со стрелками 1→x или "значениями типа x". В "программистских" категориях это именно, что значения. В таком случае, композиция с этой стрелкой-значением даст нам стрелку-значение типа-экспоненты или "имя стрелки", так его называют.
Функтор-экспонента, по отношению к функториальности, имеет дополнительные свойства. Например, согласно свойствам экспоненты, её дальше можно eval ивсётакое.
Ну а про "функтор должен знать" — грубо говоря, функтор "создаёт" для этого типы, а стрелка уже куда надо соединяется. Стрелки он тоже отображает и должно быть понятно, как.
no subject
Date: 2013-01-09 10:53 pm (UTC)о, а заодно. А правда, что раз X = 1 → X, то ap = композиция?
Типа, у апликативного функтора (F f) `ap` (F x) = F (f x), что при условии X = 1 → X получается (F f) `ap` (F x) = F (f oC x) = (F f) oD (F x)
no subject
Date: 2013-01-10 07:13 am (UTC)Какое-такое X и почему оно равно 1→X??...
Что это за равенство?... Равенство типов? Стрелок?
Я говорил про совершенно примитивные вещи — о представлении значений типа a стрелками 1→a.
Если этот тип экспонента y^x, то и значениями этого типа будут функции x→y, но в "закодированной" форме, которой можно воспользоваться через свойства (определение) экспоненты.
Если предположить, что это равенство и обозначает "значения типа X это 1→X", тогда насчёт аппликативых функторов всё легко подставить и получить в каждом конкретном случае. А в общим случае, стоит заметить, что тип f (a→b) → f a → f b не подразумевает обязательность каких-то 'значений'.
Но эти вот 'программистские' категории такие вот замечательные (well-pointed), что любая стрелка a→b может быть полностью определена композицией со стрелками-значениями 1→a. И если две `параллельные` стрелки различны, то должна найтись такая стрелка-значение в область определения (домен) стрелок, что композиции с ней будут не равны.
http://en.wikipedia.org/wiki/Well-pointed_category
http://ncatlab.org/nlab/show/generator
no subject
Date: 2013-01-10 08:01 am (UTC)я хотел сказать, что вроде как выводят, что X = 1 x X - поскольку при наличии в категории терминального объекта существует стрелка в 1 и стрелка в само себя, то любое X можно представить и как произведение 1 x X; так можно и вывести X = X1 = 1 x X1, где id = curryid, коий есть представление 1 → X.
"Well-pointed category"
можно то же перефразировать, что терминальный объект не является инициальным? Или существуют другие условия, когда p: 1 → A, f o p = g o p для произвольных f /= g, кроме когда 1 является инициальным?
no subject
Date: 2013-01-10 09:08 am (UTC)В обычной категории, на объектах не рассуждают о равенстве, а только об изоморфизме.
Ну не определено никакое равенство на объектах категории!
Хотя и оно может быть определено на тех сущностях, из которых категорию "сгенерировали".
Да, очевидно доказывается, что в любой категории с терминальным объектом и произведениями X ≈ X×1
Только вот, _изоморфен_, а не равен.
Есть точка зрения (например, так говорит тов. Манин), что от любой категории надо рассматривать её скелет (категория, факторизованная по отношению изоморфизма).
Я бы согласился, но с такой большой поправкой — нужно стремиться к этому, но к сожалению, не всегда это получается "малой кровью".
Простой пример — X×Y ≈ Y×X, но знак равенства ставить будет практически неудобно ;-)
> Или существуют другие условия,
> когда p: 1 → A, f o p = g o p
> для произвольных f /= g, кроме
> когда 1 является инициальным?
Во-первых, несложно придумать такую категорию специально.
Во-вторых, при чём тут well-pointed'ность? Оно не подразумевает такие условия.
Судить о равенстве стрелок можно по их композициям со всеми функциями от генератора (в данном случае, 1).
Можно переформулировать (как в ncatlab-статье) ещё так, что функтор Hom(1,_) — строгий (или как там в переводе Маклейна — "унивалентный").
По ссылке
http://ncatlab.org/nlab/show/generator
есть пример про модули. Можно придумать подобное для топологических пространств.
no subject
Date: 2013-01-10 09:25 am (UTC)А как мы можем отличить, у кого X слева, а у кого - справа? Как мы даже можем отличить, что у них X с разных сторон? Вроде бы всё, что можно заключить, так это что "это тоже X×Y, хотя и не идентичный объект". Я правильно понимаю, что это просто так визуально на бумаге отображают, а на самом деле X×Y может быть выражено более, чем двумя способами?
"Во-вторых, при чём тут well-pointed'ность?"
Ну я думал, что well-pointedность сводится к тому, что 1 - не инициальный объект. Хотя на самом деле, если смотреть поточечно, то нужно наличие морфизмов из 1 в каждую точку каждого X.
Хом-функторы - это мне ещё предстоит...
no subject
Date: 2013-01-10 10:04 am (UTC)Даже X может быть выражено более, чем двумя способами ;-)
Множества из 3 стульев дома и 3 стульев в рабочем кабинете — не равны, но изоморфны! ;-)
no subject
Date: 2013-01-10 10:07 am (UTC)ок, я думаю, пример понятный, спасибо.
no subject
Date: 2013-01-10 10:13 am (UTC)Отрезки натуральных чисел [0,100] и [100,200].
Отрезки вещественных чисел [0,1] и [100,200].
no subject
Date: 2013-01-10 09:46 am (UTC)Только вот, _изоморфен_, а не равен."
а как тогда сказать, что X is X×1?
Т.е. для любого X существуют морфизмы, которые можно взять за проекции в 1 и X со всеми свойствами произведения. Т.е. можно и сказать, что он изоморфен любому другому X×1, но тут же какое-то другое высказывание?
Или эти два высказывания изоморфны? :)
no subject
Date: 2013-01-10 10:29 am (UTC)"X is" это оборот речи, а "изоморфен" — строгое определение! ;-)
То есть, зависит от того, что понимается под "is".
> которые можно взять за проекции в 1 и X
Проекции _из_ произведения, а не в него!
Для любого X существуют морфизмы, которые можно взять за проекции 1 ← 1×X → X
> А как мы можем отличить,
> у кого X слева, а у кого - справа?
Если мы собираемся все конструкции производить "по модулю" изоморфизма, тогда придётся как-то по-другому определять произведение. Способы подсказывает классическая теория множеств, впрочем.
Но на мой взгляд, лучше смириться с тем, что не всегда бывает удобно отождествлять изоморфное.
no subject
Date: 2013-01-10 10:42 am (UTC)ага, я это и хотел сказать - проекции в 1 и в X (поотдельности)
"Если мы собираемся все конструкции производить "по модулю" изоморфизма, тогда придётся как-то по-другому определять произведение. Способы подсказывает классическая теория множеств, впрочем.
Но на мой взгляд, лучше смириться с тем, что не всегда бывает удобно отождествлять изоморфное."
да я бы и рад не отождествлять :)
про "слева" и "справа" я расспрашиваю исключительно потому, что раз пишем X×Y ≈ Y×X, то имеем в виду..........просто, что они разные? Я не пойму, как можно "направленность" определить, раз объекты не тождественные.
Примерно так:
когда в х-е пишем fst, то, конечно, легко видеть, что существенна "направленность" - кто там первый X или Y. Но в теор кате стрелки из одного объекта не имеют отношения к стрелкам из другого объекта, т.е. нет способа выразить "полиморфные" стрелки fst, которые делают что-то там одинаково. Или такой способ есть?
Для себя я объясняю эту разницу тем, что на самом деле в х-е fst работает не с прямо объектами X×Y, а с изоморфными им объектами Pair, построенными конструктором (PairY)X - а вот здесь уже порядок X и Y можно определить из порядка eval.
no subject
Date: 2013-01-10 11:31 am (UTC)> просто, что они разные?
Когда так пишут, это дословно означает, что существует изоморфизм. Вне зависимости от того, разные они там или одинаковые.
> когда в х-е пишем fst
Ну так и в категориях есть первая и вторая проекции.
Если не стараться отождествлять изоморфное, то и различать запросто.
> Но в теор кате стрелки из одного объекта
> не имеют отношения к стрелкам из другого объекта,
Если эти два объекта изоморфны, то имеет же.
Можно просто и тупо делать композицию с этим изоморфизмом.
> т.е. нет способа выразить "полиморфные" стрелки fst,
> которые делают что-то там одинаково.
Функтор произведения имеет соответствующие свойства, что создаёт соответствующие "вспомогательные" стрелки.
В хацкеле с категорной семантикой мутновато. Но в довольно хорошем первом приближении, можно считать, что пары, это такие "хитрые" начальные алгебры.
no subject
Date: 2013-01-10 11:37 am (UTC)хм. я думал из определения следует "одна и другая" проекции :) типа как здесь:
"Можно просто и тупо делать композицию с этим изоморфизмом."
но тогда не ясно, как это отличается от композиции с snd вместо fst :)
ок, пора почитать про произведение заданное через функтор.
no subject
Date: 2013-01-10 11:53 am (UTC)> если порядок есть, то тогда понятно.
Скажем так — порядка нет, но это setoid.
То есть, элементы индексов мы можем отличать друг от друга.
И естественно, что конечное множество (мы вообще говорили о двух элементах) мы вполне можем вполне упорядочить, но в данном случае, это не важно.
Есть элемент i есть элемент k. Вот и будет говорить об i-й проекции и k-й проекции, не упорядочивая множество индексов.
no subject
Date: 2013-01-10 11:55 am (UTC)no subject
Date: 2013-01-10 12:14 pm (UTC)Несколько образно, индексами мы обозначаем места, куда можно что-то "положить".
Так вот, если есть два индекса x и y, то мы на место x можем "положить" Y, а можем и X, например.
Декартово произведение задаёт с собой сразу и проекции. Это хорошее такое произведение.
Но не каждое моноидальное произведение позволяет потом "раздербанить" произведение по составляющим.
no subject
Date: 2013-01-10 12:22 pm (UTC)да, я это понимаю. я пытаюсь понять, "направленность" у X×Y "глобально видима" или как? То есть, "какое-то представление индексов" понятно.
Я оба произведения понимаю, и понимаю, почему изоморфны. Я не знаю наверняка, существенно ли, что Y×X пишется в обратном порядке. Это просто запись такая, чтобы не выглядело тавтологично "X×Y ≈ X×Y"? Или есть способ выделить "направленность" и для каких-то двух объектов можно выяснить, что они одинаковой "направленности"?
(ну, я не знаю - может, где-то в какой-то книжке написано, а я читал не то? из того, что я читал, никак не следует, что можно выяснить "направленность" двух разных произведений)
no subject
Date: 2013-01-10 12:41 pm (UTC)Исходя из каких данных выяснить?
Произведение уже направлено по определению — есть две различимых проекции, составляется произведение тоже вполне так "направленно".
Принято в n-арном произведении всякое умножаемое писать упорядоченной цепочкой типа XxYxZxTxUxV или (X,Y,Z,T,U,V). И то, что отдаст первая проекция, принято писать слева. Соответственно, отличать XxY от YxX, если как-то отличаем X и Y.
Тем не менее, в категорном, достаточно часто выписывают проекции явно, тем самым, устраняя ещё одну возможность неоднозначности понимания. И это хорошо, как правило.
no subject
Date: 2013-01-10 12:53 pm (UTC)"Исходя из каких данных выяснить?"
ага, это мой вопрос.
"Произведение уже направлено по определению"
блин, ну, как же направлено, если проекции индексируются сетоидом I. Я понимаю, что можно записать сетоид в виде списка. Я понимаю, что сетоида достаточно, чтобы знать, как применить проекцию.
давайте попробую ещё раз по частям.
∏{X}{i,j} и ∏{X}{i,k}
1. это произведения одного и того же Xi и разных Xj, Xk? или в каждом случае i - просто индекс, а потому Xi первого не обязательно Xi второго? Типа как в арифметике запись ΣXi i не означает ничего, кроме способа выбрать Xi в этой одной сумме, и не означает, что в двух разных записях Xi references одно и то же значение.
2. если Xi в обоих записях означает один и тот же Xi, то что задаёт порядок i в сетоиде, ...кроме договорённости записывать i, j, k в алфавитном порядке.
3. Я сейчас считаю, что ∏{X}{i,j} эквивалентно записи Xi×Xj и эквивалентно записи Xj×Xi, поскольку порядок i, j отсутствует. Откуда тогда следует направленность произведения?
no subject
Date: 2013-01-10 01:55 pm (UTC)Строго говоря, классические проекции индексируются дискретной категорией (в которой стрелки только единичные).
И произведение, это предел некоторого функтора из этой категории.
Какие претензии к этом определению? ;-)
А касаемо вопросов — это должно быть всегда ясно из контекста.
Если не ясно, значит херово написали.
no subject
Date: 2013-01-08 10:15 pm (UTC)