Николай Иваныч ([info]nivanych) wrote,
@ 2008-12-02 16:27:00
Previous Entry  Add to memories!  Tell a Friend  Next Entry
Computational Category Theory
Во что обнаружил!
http://www.cs.man.ac.uk/~david/categories

Подробно ещё не смотрел, но похоже, что это
то же самое, что делает [info]ivan_ghandhi, только на ML.
И топосы, топосы там есть, в отличие от [info]ivan_ghandhi ;-)

На всякий случай уточню, "что делает [info]ivan_ghandhi" --
http://docs.google.com/View?docid=dc7rg5cv_24ftbwjrgm

(36 comments) - (Post a new comment)


[info]kurilka
2008-12-02 01:54 pm UTC (link)
А что он делает?

(Reply to this) (Thread)

[info]nivanych
2008-12-02 02:29 pm UTC (link)
Да много всякой фигни делает ;-)
(Я добавил в пост)

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-02 02:33 pm UTC (link)
А, это он чтоль написал?
Ну бум знать (правда почитать так руки и не дошли)

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-02 02:36 pm UTC (link)
Да, это он написал ;-)

Во всех отношениях замечательная вещь,
кроме как выбора языка...

Ну не могу я воспринимать на Java,
да ещё и такие вещи...

(Reply to this) (Parent)

[info]nivanych
2008-12-02 04:25 pm UTC (link)
Вот подумалось, а ведь такое
можно и на PHP сделать, в принципе!
Только я не возьмусь -- не выдержу.

Эхх... а как было бы круто --
конструктивная теория категорий для веб-программистов...

;-)

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-02 04:26 pm UTC (link)
А ты злой, оказывается :)

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-02 04:40 pm UTC (link)
Нет, ты что.
Я теперь совсем добрый.
Про PHP только угрожаю.

(Reply to this) (Parent)

[info]kurilka
2008-12-02 04:27 pm UTC (link)
А бывает ещё неконструктивная ТК?

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-02 04:42 pm UTC (link)
Конечно.
Основанная на неконструктивной логике.
Например, классических предикатах.

Что-нибудь существует -- бери его по правилу E.
И совсем другое дело построить программу,
которая "это дело" (с "этими свойствами") построит.

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-02 04:44 pm UTC (link)
Е - это что? Квантор существования?

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-02 04:54 pm UTC (link)
Есть такое -- Правило E.
Так и называется.
Приблизительно означает, что если есть утверждение
про существование объекта с "такими-то свойствами",
то для дальнейших рассуждений можно этот объект
как-бы "взять", например --
для любого x существует такой y, что y*y = x.
Построить ты этот y, в общем случае, не сможешь,
но рассуждать о том, что если это утверждение верно,
то я могу условно "взять этот y", вполне можно.
Это доказывается, кстати, и несложно ;-)
Только для полного объяснения нужно зафиксировать
конкретную теорию предикатов и конкретно объяснить.
Смысла в этом не вижу.

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-02 04:58 pm UTC (link)
загадочно, гугл ничего не выдаёт :)

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-02 05:04 pm UTC (link)
Очень странно.
Классическая теория предикатов первого порядка.

(Reply to this) (Parent)

[info]nivanych
2008-12-02 05:05 pm UTC (link)
Но название это правило получило,
разумеется, от квантора существования.

(Reply to this) (Parent)

[info]nivanych
2008-12-02 05:17 pm UTC (link)
У меян дома есть книжка.
Тов. Мендельсона, зелёная такая.
Но смотреть врядли имеет смысл,
эта вещь уж слишком фундаментальная,
врядли я где мог ошибиться.

(Reply to this) (Parent)

[info]nivanych
2008-12-02 04:44 pm UTC (link)
Но в теории категорий очень многое можно построить.
Она "в значительной мере конструктивная",
даже если основывать её на классических предикатах.

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-02 04:45 pm UTC (link)
А неконструктивный пример не дашь?

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-02 04:59 pm UTC (link)
Ну хорошо.
Ради прикола, специально, на некоторых вещах
внимание не буду останавливать, скорее, наоборот.

Возьмём категорию, в которой существуют декартовы квадраты.
Вот 2 объекта -- a и b. Откуда мне взять из декартово произведение?
А именно, 2 морфизма --
pa : axb -> a
pb : axb -> b
и для любого объекта c с двумя морфизмами
ca : с -> a
cb : c -> b
должен существовать морфизм
caxcb : c -> axb
да так, чтобы
pa o caxcb = ca
pb o caxcb = cb

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-02 07:15 pm UTC (link)
в "pa o caxcb" о - это оператор композиции?
Некоструктивизм в том, что произведение берётся "аксиоматически", типа без построения его?

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-03 07:45 am UTC (link)
> в "pa o caxcb" о - это оператор композиции?

Да, это оператор композиции.
Неохота было стрелочки рисовать.

> Некоструктивизм в том, что произведение берётся
> "аксиоматически", типа без построения его?

Ага.
Правда, в случае с произведением
в большинстве случаев можно его вычислить.

(Reply to this) (Parent)(Thread)

[info]kurilka
2008-12-03 08:13 am UTC (link)
Поясни недалёкому, что значит в данном случае "вычислить"?

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-03 08:59 am UTC (link)
Значит, представить программу, которая
сконструирует объект с нужными свойствами.

(Reply to this) (Parent)

[info]nivanych
2008-12-02 05:02 pm UTC (link)
Мы можем знать, что что-то существует,
но конкретное его "устройство" дать можно не всегда.
В случае с примером про декартов квадрат это ерунда.
Оно, как раз-таки, во многих случаях, строится.

Но в случае про, например, извлечение корня
это уже становится вполне хорошим примером.
Корень существует? Да!
Ну-ка, покажи мне корень из 2-х?...

(Reply to this) (Parent)(Thread)

[info]migmit.vox.com
2009-05-30 09:23 am UTC (link)
f(x) = sup {y | y2 < 2x2 }, x > 0
f(0) = 0
f(-x) = -f(x)

(Reply to this) (Parent)(Thread)

[info]nivanych
2009-05-30 12:15 pm UTC (link)
И как эти супремумы складывать, умножать и делить?
Нет, конечно, это можно сделать.
Но по простоте будет немногим
отличаться от чисел в виде пределов.

(Reply to this) (Parent)(Thread)

[info]migmit.vox.com
2009-05-30 12:30 pm UTC (link)
Наоборот. Я использовал довольно редко встречающееся, но очень удобное представление вещественных чисел в виде почти линейных функций. При этом сложение производится поточечно, а умножение представляет собой композицию.

(Reply to this) (Parent)(Thread)

[info]nivanych
2009-05-30 12:45 pm UTC (link)
"Почти линейные" будет "almost linear"?
Очень любопытно. А моожно ссылок?
Ничего путного я сходу не нашёл.

(Reply to this) (Parent)(Thread)

[info]migmit.vox.com
2009-05-30 01:04 pm UTC (link)
"Это формула Сабанеева? - Нет. - А чья? Ваша? - Она всегда была".

Проще объяснить так. Функция типа Z -> Z является линейной, если дифференциал от неё равен нулю; дифференциал считается как df(x,y) = f(x+y) - f(x) - f(y). Назовём функцию почти линейной, если её дифференциал - ограниченная функция. Ясно, что если функция сама по себе ограничена, то её дифференциал тоже ограничен, а потому эта функция почти линейна. Вещественные числа - это фактор группы почти линейных функций по подгруппе ограниченных, где операция - это поточечное сложение.

(Reply to this) (Parent)(Thread)

[info]nivanych
2009-05-30 01:42 pm UTC (link)
Изящно. Спасибо.

Надо подумать, где это будет удобно, а где нет.

(Reply to this) (Parent)

[info]nivanych
2009-05-30 12:47 pm UTC (link)
Есть книжки на эту тему?...
Видимо, ближе к концу лета
начну этим интересоваться подробнее.

(Reply to this) (Parent)

[info]beroal
2008-12-04 06:41 am UTC (link)
Скажи мне такую вещь: категории групп, колец, модулей являются топосами?

(Reply to this) (Thread)

[info]nivanych
2008-12-04 09:20 am UTC (link)
Кстати, мне не нравится перевод
"конечный объект", предпочитаю "терминальный".

Возьмём, для примера, моноиды.

Произведение моноидов, очевидно, всегда
существует, и его легко построить.
Экспонента тоже существует, и для
конечных моноидов её можно построить.
Кстати, интересно вообразить, что это такое ;-)
И классификатор подобъектов тоже существует,
и его тоже можно построить для конечных моноидов.

Но вот с начальными-терминальными объектами неувязочка.
Очевидно, что одноэлементный моноид
является терминальным объектом.
Однако, он же является и начальным --
единица должна отображаться в единицу.

То есть, в категории моноидов и их гомоморфизмов
начальный и терминальный объекты изоморфны.
То есть, этот топос вырожденный.

Но есть и "нормальные" топосы, в которые он вкладывается.

(Reply to this) (Parent)(Thread)

[info]beroal
2009-01-28 06:47 am UTC (link)
Обнаружил:

Ab is not cartesian closed (and therefore also not a topos) since it lacks exponential objects. NationMaster - Encyclopedia: Category of abelian groups.

(Reply to this) (Parent)(Thread)

[info]nivanych
2009-01-28 09:19 am UTC (link)
Ага, ступил.
Экспонента exp(A, B) в этом случае --
это набор гомоморфизмов A -> B,
который, как правило, не группа.
Вот категория изоморфных групп
будет вырожденным топосом %)

Но по крайней мере, конечные алгебры
замечательно исследуются в рамках топоса.
То есть, вкладываются в подходящий топос.
Правда, логика в топосе отличается от классической.

(Reply to this) (Parent)

[info]maxim
2009-05-30 12:55 am UTC (link)
Мне больше нравится

Steven Awodey, Andrej Bauer: "Lecture Notes: Introduction to Categorical Logic".

Ктоме того, хотел бы обратить ваше внимание на CPL — Categorical Programming Language, авторства Tatsuya Hagino, тоже из семейства категориальных метаязыков. Он построен тоже на базе категорийной абстрактной машины, такой как CAM в ML языках, но которая использует другие правила вывода (операции). Его КАМ построена не на базе ДЗК, и например определение ДЗК в ней будет выглдеть так:

# terminal object
right object 1 with ! is
end object;

# product functor
right object prod(X,Y) with pair is
pi1: prod -> X
pi2: prod -> Y
end object;

# exponential functor
right object exp(X,Y) with curry is
eval: prod(exp,X) -> Y
end object;

Реализация на Ruby и Haskell этого CPL можна найти здесь, авторства Masahiro Sakai.

(Reply to this) (Thread)

[info]nivanych
2009-05-30 12:33 pm UTC (link)
> Steven Awodey, Andrej Bauer:
> "Lecture Notes: Introduction to Categorical Logic"

Уже прочитал ;-)

> авторства Tatsuya Hagino

Hagino тоже читал.
И Charity изучил.

А вот про реализацию CPL любопытно, спасибо.

(Reply to this) (Parent)

(36 comments) - (Post a new comment)

Create an Account
Forgot your login or password?
Login w/ OpenID
English • Español • Deutsch • Русский…