deniok: (Default)
[personal profile] deniok
От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо [livejournal.com profile] alexey_rom за ссылку.

Date: 2013-01-08 09:10 am (UTC)
From: [identity profile] migmit.livejournal.com
Чем ему теория категорий не нравится?

Date: 2013-01-08 09:25 am (UTC)
From: [identity profile] deni-ok.livejournal.com
не знаю, спроси там. Я по таким темам читатель, а не писатель.

Date: 2013-01-08 05:20 pm (UTC)
From: [identity profile] migmit.livejournal.com
Там очень TL. Я DR.

Date: 2013-01-08 04:31 pm (UTC)
From: [identity profile] nivanych.livejournal.com
Выводят, понимаешь, лямбды всякие из готовых работающих категорных конструкций!

Date: 2013-01-09 02:17 pm (UTC)
From: [identity profile] sassa-nf.livejournal.com
Ну я не знаю, а как лямбду нормально в теор кате описать? Для каждой стрелки городить curry? Тогда не очень ясно, как красиво сделать higher order функции.

Но зато "у них" какая-то фигня с функторами должна получаться, ибо теперь он должен различать BA?

Date: 2013-01-09 02:39 pm (UTC)
From: [identity profile] nivanych.livejournal.com
higher-order-функции — это элементы объекта экспонент.
А что такое "различать B^A"?

Date: 2013-01-09 04:56 pm (UTC)
From: [identity profile] sassa-nf.livejournal.com
Ну функтор же функции должен отображать специальным образом. В теор кате это задано явно - функтор стрелки и объекты отображает по отдельности. А в теории типов лямбды не отличаются от других типов. Значит, функтор должен "знать", что это не просто C, а именно какое-то BA, который должен отобразиться в две вещи: F (BA) как объект, и в (F B)F A как стрелка.

Конечно, о функторе я вспоминаю только потому, что в программировании он есть, значит, в теории типов тоже должен как-то быть.
Edited Date: 2013-01-09 04:57 pm (UTC)

Date: 2013-01-09 05:23 pm (UTC)
From: [identity profile] nivanych.livejournal.com
Произведение — это тоже функтор с двумя параметрами. Но экспонента контрвариантна по первому аргументу (как и Hom-функтор).
Функции с двумя параметрами могут быть классически представлены стрелками в экспоненты x → (y→z), ну или стрелка x → (z^y).
Можно раскрыть и поточечный взгляд, согласно которому, мы постоянно отслеживаем композиции со стрелками 1→x или "значениями типа x". В "программистских" категориях это именно, что значения. В таком случае, композиция с этой стрелкой-значением даст нам стрелку-значение типа-экспоненты или "имя стрелки", так его называют.
Функтор-экспонента, по отношению к функториальности, имеет дополнительные свойства. Например, согласно свойствам экспоненты, её дальше можно eval ивсётакое.
Ну а про "функтор должен знать" — грубо говоря, функтор "создаёт" для этого типы, а стрелка уже куда надо соединяется. Стрелки он тоже отображает и должно быть понятно, как.

Date: 2013-01-09 10:53 pm (UTC)
From: [identity profile] sassa-nf.livejournal.com
мда. Я про это всё читал. Видимо, углубить нужно.

о, а заодно. А правда, что раз 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)
Edited Date: 2013-01-09 10:54 pm (UTC)

Date: 2013-01-10 07:13 am (UTC)
From: [identity profile] nivanych.livejournal.com
Что такое "раз X=1→X", я не понимаю.
Какое-такое 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

Date: 2013-01-10 08:01 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
"X = 1 → X"

я хотел сказать, что вроде как выводят, что 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 является инициальным?
Edited Date: 2013-01-10 08:08 am (UTC)

Date: 2013-01-10 09:08 am (UTC)
From: [identity profile] nivanych.livejournal.com
> X = 1 x X

В обычной категории, на объектах не рассуждают о равенстве, а только об изоморфизме.
Ну не определено никакое равенство на объектах категории!
Хотя и оно может быть определено на тех сущностях, из которых категорию "сгенерировали".

Да, очевидно доказывается, что в любой категории с терминальным объектом и произведениями 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
есть пример про модули. Можно придумать подобное для топологических пространств.

Date: 2013-01-10 09:25 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
"X×Y ≈ Y×X, но знак равенства ставить будет практически неудобно ;-)"

А как мы можем отличить, у кого X слева, а у кого - справа? Как мы даже можем отличить, что у них X с разных сторон? Вроде бы всё, что можно заключить, так это что "это тоже X×Y, хотя и не идентичный объект". Я правильно понимаю, что это просто так визуально на бумаге отображают, а на самом деле X×Y может быть выражено более, чем двумя способами?


"Во-вторых, при чём тут well-pointed'ность?"

Ну я думал, что well-pointedность сводится к тому, что 1 - не инициальный объект. Хотя на самом деле, если смотреть поточечно, то нужно наличие морфизмов из 1 в каждую точку каждого X.

Хом-функторы - это мне ещё предстоит...

Date: 2013-01-10 10:04 am (UTC)
From: [identity profile] nivanych.livejournal.com
> X×Y может быть выражено более, чем двумя способами?

Даже X может быть выражено более, чем двумя способами ;-)
Множества из 3 стульев дома и 3 стульев в рабочем кабинете — не равны, но изоморфны! ;-)

Date: 2013-01-10 10:07 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
но это же разные 3 стула :)

ок, я думаю, пример понятный, спасибо.

Date: 2013-01-10 10:13 am (UTC)
From: [identity profile] nivanych.livejournal.com
Ну или более строгие примеры.
Отрезки натуральных чисел [0,100] и [100,200].
Отрезки вещественных чисел [0,1] и [100,200].

Date: 2013-01-10 09:46 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
"Да, очевидно доказывается, что в любой категории с терминальным объектом и произведениями X ≈ X×1
Только вот, _изоморфен_, а не равен."

а как тогда сказать, что X is X×1?

Т.е. для любого X существуют морфизмы, которые можно взять за проекции в 1 и X со всеми свойствами произведения. Т.е. можно и сказать, что он изоморфен любому другому X×1, но тут же какое-то другое высказывание?

Или эти два высказывания изоморфны? :)
Edited Date: 2013-01-10 09:47 am (UTC)

Date: 2013-01-10 10:29 am (UTC)
From: [identity profile] nivanych.livejournal.com
> а как тогда сказать, что X is X×1?

"X is" это оборот речи, а "изоморфен" — строгое определение! ;-)
То есть, зависит от того, что понимается под "is".

> которые можно взять за проекции в 1 и X

Проекции _из_ произведения, а не в него!
Для любого X существуют морфизмы, которые можно взять за проекции 1 ← 1×X → X

> А как мы можем отличить,
> у кого X слева, а у кого - справа?

Если мы собираемся все конструкции производить "по модулю" изоморфизма, тогда придётся как-то по-другому определять произведение. Способы подсказывает классическая теория множеств, впрочем.
Но на мой взгляд, лучше смириться с тем, что не всегда бывает удобно отождествлять изоморфное.

Date: 2013-01-10 10:42 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
"Проекции _из_ произведения, а не в него!"

ага, я это и хотел сказать - проекции в 1 и в X (поотдельности)


"Если мы собираемся все конструкции производить "по модулю" изоморфизма, тогда придётся как-то по-другому определять произведение. Способы подсказывает классическая теория множеств, впрочем.
Но на мой взгляд, лучше смириться с тем, что не всегда бывает удобно отождествлять изоморфное."

да я бы и рад не отождествлять :)

про "слева" и "справа" я расспрашиваю исключительно потому, что раз пишем X×Y ≈ Y×X, то имеем в виду..........просто, что они разные? Я не пойму, как можно "направленность" определить, раз объекты не тождественные.

Примерно так:

когда в х-е пишем fst, то, конечно, легко видеть, что существенна "направленность" - кто там первый X или Y. Но в теор кате стрелки из одного объекта не имеют отношения к стрелкам из другого объекта, т.е. нет способа выразить "полиморфные" стрелки fst, которые делают что-то там одинаково. Или такой способ есть?

Для себя я объясняю эту разницу тем, что на самом деле в х-е fst работает не с прямо объектами X×Y, а с изоморфными им объектами Pair, построенными конструктором (PairY)X - а вот здесь уже порядок X и Y можно определить из порядка eval.

Date: 2013-01-10 11:31 am (UTC)
From: [identity profile] nivanych.livejournal.com
> раз пишем X×Y ≈ Y×X, то имеем в виду..........
> просто, что они разные?

Когда так пишут, это дословно означает, что существует изоморфизм. Вне зависимости от того, разные они там или одинаковые.

> когда в х-е пишем fst

Ну так и в категориях есть первая и вторая проекции.
Если не стараться отождествлять изоморфное, то и различать запросто.

> Но в теор кате стрелки из одного объекта
> не имеют отношения к стрелкам из другого объекта,

Если эти два объекта изоморфны, то имеет же.
Можно просто и тупо делать композицию с этим изоморфизмом.

> т.е. нет способа выразить "полиморфные" стрелки fst,
> которые делают что-то там одинаково.

Функтор произведения имеет соответствующие свойства, что создаёт соответствующие "вспомогательные" стрелки.

В хацкеле с категорной семантикой мутновато. Но в довольно хорошем первом приближении, можно считать, что пары, это такие "хитрые" начальные алгебры.

Date: 2013-01-10 11:37 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
"Ну так и в категориях есть первая и вторая проекции."

хм. я думал из определения следует "одна и другая" проекции :) типа как здесь: - я не знаю, означает ли это, что порядок у I есть? если порядок есть, то тогда понятно.


"Можно просто и тупо делать композицию с этим изоморфизмом."

но тогда не ясно, как это отличается от композиции с snd вместо fst :)

ок, пора почитать про произведение заданное через функтор.

Date: 2013-01-10 11:53 am (UTC)
From: [identity profile] nivanych.livejournal.com
> порядок у I есть?
> если порядок есть, то тогда понятно.

Скажем так — порядка нет, но это setoid.
То есть, элементы индексов мы можем отличать друг от друга.
И естественно, что конечное множество (мы вообще говорили о двух элементах) мы вполне можем вполне упорядочить, но в данном случае, это не важно.
Есть элемент i есть элемент k. Вот и будет говорить об i-й проекции и k-й проекции, не упорядочивая множество индексов.

Date: 2013-01-10 11:55 am (UTC)
From: [identity profile] sassa-nf.livejournal.com
вот я так себе и представлял. А отсюда следует, что и у X×Y, и у Y×X один и тот же сетоид используется? Если нет, то хотя мы и можем выбрать i-ю проекцию X×Y, может у Y×X её и нет вообще?
Edited Date: 2013-01-10 11:58 am (UTC)

Date: 2013-01-10 12:14 pm (UTC)
From: [identity profile] nivanych.livejournal.com
Из записи XxY не следует какое-то представление индексов, а только то, что их два штук.
Несколько образно, индексами мы обозначаем места, куда можно что-то "положить".
Так вот, если есть два индекса x и y, то мы на место x можем "положить" Y, а можем и X, например.

Декартово произведение задаёт с собой сразу и проекции. Это хорошее такое произведение.
Но не каждое моноидальное произведение позволяет потом "раздербанить" произведение по составляющим.

Date: 2013-01-10 12:22 pm (UTC)
From: [identity profile] sassa-nf.livejournal.com
"Из записи XxY не следует какое-то представление индексов, а только то, что их два штук."

да, я это понимаю. я пытаюсь понять, "направленность" у X×Y "глобально видима" или как? То есть, "какое-то представление индексов" понятно.

Я оба произведения понимаю, и понимаю, почему изоморфны. Я не знаю наверняка, существенно ли, что Y×X пишется в обратном порядке. Это просто запись такая, чтобы не выглядело тавтологично "X×Y ≈ X×Y"? Или есть способ выделить "направленность" и для каких-то двух объектов можно выяснить, что они одинаковой "направленности"?

(ну, я не знаю - может, где-то в какой-то книжке написано, а я читал не то? из того, что я читал, никак не следует, что можно выяснить "направленность" двух разных произведений)

Date: 2013-01-10 12:41 pm (UTC)
From: [identity profile] nivanych.livejournal.com
> выяснить "направленность"

Исходя из каких данных выяснить?
Произведение уже направлено по определению — есть две различимых проекции, составляется произведение тоже вполне так "направленно".
Принято в n-арном произведении всякое умножаемое писать упорядоченной цепочкой типа XxYxZxTxUxV или (X,Y,Z,T,U,V). И то, что отдаст первая проекция, принято писать слева. Соответственно, отличать XxY от YxX, если как-то отличаем X и Y.
Тем не менее, в категорном, достаточно часто выписывают проекции явно, тем самым, устраняя ещё одну возможность неоднозначности понимания. И это хорошо, как правило.

Date: 2013-01-10 12:53 pm (UTC)
From: [identity profile] sassa-nf.livejournal.com
Я не знаю, как уточнить свой вопрос. Пока что понятно не стало.

"Исходя из каких данных выяснить?"

ага, это мой вопрос.


"Произведение уже направлено по определению"

блин, ну, как же направлено, если проекции индексируются сетоидом 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 отсутствует. Откуда тогда следует направленность произведения?
Edited Date: 2013-01-10 01:01 pm (UTC)

Date: 2013-01-10 01:55 pm (UTC)
From: [identity profile] nivanych.livejournal.com
> проекции индексируются сетоидом I.

Строго говоря, классические проекции индексируются дискретной категорией (в которой стрелки только единичные).
И произведение, это предел некоторого функтора из этой категории.
Какие претензии к этом определению? ;-)

А касаемо вопросов — это должно быть всегда ясно из контекста.
Если не ясно, значит херово написали.

Date: 2013-01-08 10:15 pm (UTC)
From: [identity profile] nponeccop.livejournal.com
Мне никогда не нравилась идея "if the monster simple group happens to be a real number, then its square is nonnegative”. А теперь я знаю, как она называется!

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 20th, 2025 09:40 am
Powered by Dreamwidth Studios