Здравствуйте, Lazy Cjow Rhrr, Вы писали:
M>>Конечные булевы топосы применяются для моделирования онтологий. LCR>Чего такое "онтология"? Термин "онтология" мне известен с пар по философии, но я не уверен, что в данном случае это то же самое. Еще чуть более реальный пример можно?
Онтолоигия — термин, применяющийся в математике для обозначения моделей, т.е. моделей как совокупности объектов и отношений между ними. Т.е. предполагается, что люди видят мир более-менее одинаково и способ видения основан на расчленении реальности на совокупности объектов. Объекты связаны между собой какими-то отношениями. Вот онтология — это и есть модель некоторой части реальности, формализованная в виде такой совокупности. Причем, реальная модель подразумевает, что объектов есть конечное число и отношений между объектами также конечное число. Моделировать реальности можно с помощью разных математических подходов. Наиболее распространненный из них — это использование формальных логических языков. Там семантика заранее известна, так что описание онтологии есть просто текст на таком языке, например программа на Прологе. Используются еще так называемые семантические сети — более свободный стиль описания объектов с отношениями в виде ориентированных графов. Подход описания онтологий, о котором писал я, это использование алгебры и теории категорий. Он идет от теории абстрактных типов. Абстракный тип — это набор множеств (объектов), набор операций между ними и некоторая сосвокупность формул, задающих ограничения на применение операций. Первоначально, в 70-х годах, когда теория алгебраических типов бурно развивалась, ее целью было построение строгого обоснования типизации. Но вот оказалось, что эту теорию можно использовать для построения онтологий. Каждое понятие реальности, которая строится, можно рассматривать как алгебраический тип. Но хотелось бы иметь инструмент для автоматического построения онтологий. Для этого надо строго определить язык, на котором эти онтологии задаются, а значит определить его синтаксис и семантику. Синтаксис можно взять из алгебраической теории типов, там есть понятие терма как основной синтаксической структуры. Любое предложение языка определения онтологий можно проебразовать в терм. А семантику этих термов можно задавать по разному, в частности, с помощью алгебраических топосов. Такой топос должен быть конечным, т.е. содержать только конечное число элементов. Также для построения онтологии годятся не все топосы, а только те, для которых выполняетс классическая логика. если Голдблатта читал, то знаешь там есть такое понятие "булев топос". Это топос, структура которого такая же как у множества в том смысле, что семантика любой классической логики классическая. Т.е. есть только два элемента в классификаторе подобъектов: истина и ложь. Мой руководитель, профессор Бенимиаминов из РГГУ, построил теория таких алгебраических булевых топосов и реализовал систему построения онтологий на основе этой теории. Можно с ней поиграться, взять ее можно здесь.
Здравствуйте, EvilChild, Вы писали:
EC>Есть ещё такая: Andrea Asperti, Giuseppe Longo "Categories types and structures — An Introduction to Category Theory for the working computer scientist". EC>О её доступности судить не могу — не читал ещё :)) EC>В осле находится без вопросов.
Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>А вот можно глупый вопрос: где в реальной жизни мне можно применить теорию категорий? Функторы пучковизации и топосы — это конечно круто звучит и не каждому доступно понять, только вот даже алгебраисты (ну вы же знаете — гиперболические группы без кручения и всё такое) не всегда в курсе, зачем ТК нужна.
Теория категорий — это альтернативный (по отношению к теории множеств) язык для описания математических структур и их свойств. Ты же не спрашиваешь зачем нужна теория множеств, правильно? Овладеть ее методами трудно, но если это сделать, то получишь более компактный и точный способ для выражения своих мыслей. К тому же из-за своей абстрактности ТК позволяет прояснить связи между разными разделами математики. Типа можно один раз и навсегда сформулировать что такое изоморфизм и т.п.
Что касается реальной жизни, то это вопрос сложный.
Здравствуйте, EvilChild, Вы писали:
EC>Здравствуйте, Achill, Вы писали:
A>>Недавно у нас вышла книга: С.В. Косиков "Информационные системы: категорный подход". EC>Где её купить можно? На сайте не увидел, на озоне её нет. Может она в цифре доступна?
Quintanar,
Q>Тут кто-то интересовался теорией категорий в доступнов виде. Нашел одну книгу как раз по теме, правда я ее из осла скачал. Называется Computational Category Theory. В ней описаны основные конструкции и заодно приводятся примеры программ на ML, которые их в лоб имплементируют. Надо сказать, программы выглядят крайне оригинально, хотя я пока не понял, как для мирных целей можно применить построение пределов, копределов и сопряженных функторов. Может их и можно как-нибудь приспособить как монады, все-таки предел — это очень мощное понятие.
А вот можно глупый вопрос: где в реальной жизни мне можно применить теорию категорий? Функторы пучковизации и топосы — это конечно круто звучит и не каждому доступно понять, только вот даже алгебраисты (ну вы же знаете — гиперболические группы без кручения и всё такое) не всегда в курсе, зачем ТК нужна.
Хотя бы какой-нибудь гипотетический пример гипотетической ситуации
Здравствуйте, Quintanar, Вы писали:
Q>Тут кто-то интересовался теорией категорий в доступнов виде. Нашел одну книгу как раз по теме, правда я ее из осла скачал. Называется Computational Category Theory.
А она чем-нибудь отличается от свободно доступной версии: http://www.cs.man.ac.uk/~david/categories/book/book.pdf
? Q>В ней описаны основные конструкции и заодно приводятся примеры программ на ML, которые их в лоб имплементируют. Надо сказать, программы выглядят крайне оригинально, хотя я пока не понял, как для мирных целей можно применить построение пределов, копределов и сопряженных функторов. Может их и можно как-нибудь приспособить как монады, все-таки предел — это очень мощное понятие.
Как приспособить для мирных целей — я тоже не понял.
Но независимые попытки реализации монад для ML встречаются:
pa_monad: http://www.cas.mcmaster.ca/~carette/pa_monad/
Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>А вот можно глупый вопрос: где в реальной жизни мне можно применить теорию категорий? Функторы пучковизации и топосы — это конечно круто звучит и не каждому доступно понять, только вот даже алгебраисты (ну вы же знаете — гиперболические группы без кручения и всё такое) не всегда в курсе, зачем ТК нужна. LCR>Хотя бы какой-нибудь гипотетический пример гипотетической ситуации
Конечные булевы топосы применяются для моделирования онтологий.
Тут кто-то интересовался теорией категорий в доступнов виде. Нашел одну книгу как раз по теме, правда я ее из осла скачал. Называется Computational Category Theory. В ней описаны основные конструкции и заодно приводятся примеры программ на ML, которые их в лоб имплементируют. Надо сказать, программы выглядят крайне оригинально, хотя я пока не понял, как для мирных целей можно применить построение пределов, копределов и сопряженных функторов. Может их и можно как-нибудь приспособить как монады, все-таки предел — это очень мощное понятие.
Здравствуйте, Quintanar, Вы писали:
Q>Тут кто-то интересовался теорией категорий в доступнов виде. Нашел одну книгу как раз по теме, правда я ее из осла скачал. Называется Computational Category Theory. В ней описаны основные конструкции и заодно приводятся примеры программ на ML, которые их в лоб имплементируют. Надо сказать, программы выглядят крайне оригинально, хотя я пока не понял, как для мирных целей можно применить построение пределов, копределов и сопряженных функторов. Может их и можно как-нибудь приспособить как монады, все-таки предел — это очень мощное понятие.
Недавно у нас вышла книга: С.В. Косиков "Информационные системы: категорный подход".
Вроде нет.
Q>>В ней описаны основные конструкции и заодно приводятся примеры программ на ML, которые их в лоб имплементируют. Надо сказать, программы выглядят крайне оригинально, хотя я пока не понял, как для мирных целей можно применить построение пределов, копределов и сопряженных функторов. Может их и можно как-нибудь приспособить как монады, все-таки предел — это очень мощное понятие. PA>Как приспособить для мирных целей — я тоже не понял. PA>Но независимые попытки реализации монад для ML встречаются:
Монады — это только одна из конструкций. Те же пределы — это обобщенный алгоритм вычисления объектов с некоторыми уникальными свойствами на основе пары более простых конструкций.
Здравствуйте, Quintanar, Вы писали:
Q>Тут кто-то интересовался теорией категорий в доступнов виде. Нашел одну книгу как раз по теме, правда я ее из осла скачал. Называется Computational Category Theory. В ней описаны основные конструкции и заодно приводятся примеры программ на ML, которые их в лоб имплементируют. Надо сказать, программы выглядят крайне оригинально, хотя я пока не понял, как для мирных целей можно применить построение пределов, копределов и сопряженных функторов. Может их и можно как-нибудь приспособить как монады, все-таки предел — это очень мощное понятие.
Есть ещё такая: Andrea Asperti, Giuseppe Longo "Categories types and structures — An Introduction to Category Theory for the working computer scientist".
О её доступности судить не могу — не читал ещё
В осле находится без вопросов.
mefrill,
LCR>>Хотя бы какой-нибудь гипотетический пример гипотетической ситуации
M>Конечные булевы топосы применяются для моделирования онтологий.
Чего такое "онтология"? Термин "онтология" мне известен с пар по философии, но я не уверен, что в данном случае это то же самое. Еще чуть более реальный пример можно?
Здравствуйте, Achill, Вы писали:
A>Недавно у нас вышла книга: С.В. Косиков "Информационные системы: категорный подход".
Где её купить можно? На сайте не увидел, на озоне её нет. Может она в цифре доступна?
Здравствуйте, FR, Вы писали:
FR>Здравствуйте, Lazy Cjow Rhrr, Вы писали:
FR>Большая часть современной математики вообще не приминима в реальной жизни, что однако не делает ее не нужной и бесполезной.
насколько я понял, вопрос был не о бесполезности, и с учётом специфики сайта о применении в программировании
единственное приминение которое я знаю это разработка и формализация языков программирования, и то сама теория категорий там больше применяется как язык, а не как средство
было бы интересно узнать ещё какие-то ...
Quintanar,
Q>Теория категорий — это альтернативный (по отношению к теории множеств) язык для описания математических структур и их свойств. Ты же не спрашиваешь зачем нужна теория множеств, правильно? Овладеть ее методами трудно, но если это сделать, то получишь более компактный и точный способ для выражения своих мыслей. К тому же из-за своей абстрактности ТК позволяет прояснить связи между разными разделами математики. Типа можно один раз и навсегда сформулировать что такое изоморфизм и т.п. Q>Что касается реальной жизни, то это вопрос сложный.
Надо сказать, что я совсем не против теории, причём теория которая обобщает множество всяких частных случаев сама по себе ценна. Просто мне хотелось узнать, может быть кроме теоретической ценности ТК имеет и практические приложения (хотя тут merfill вроде одно привёл).
Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>Надо сказать, что я совсем не против теории, причём теория которая обобщает множество всяких частных случаев сама по себе ценна. Просто мне хотелось узнать, может быть кроме теоретической ценности ТК имеет и практические приложения (хотя тут merfill вроде одно привёл).
Так ведь и используются — Монады, Arrows, функторы в SML, в OCaml модули. Может не один в один, но идеи оттуда.
mefrill,
LCR>>Чего такое "онтология"? Термин "онтология" мне известен с пар по философии, но я не уверен, что в данном случае это то же самое. Еще чуть более реальный пример можно?
M>Онтолоигия — термин, применяющийся в математике для обозначения моделей, т.е. моделей как совокупности объектов и отношений между ними...
) не всегда в курсе, зачем ТК нужна.
quicksort =: (($:@(<#[),(=#[),$:@(>#[)) ({~ ?@#)) ^: (1<#)
