Николай Иваныч ([info]nivanych) wrote,
@ 2008-12-26 13:14:00
Previous Entry  Add to memories!  Tell a Friend  Next Entry
Entry tags:category theory

Знающие люди, подскажите!
Категорная модель higher order типов -- это топос.
Категорная модель зависимых типов -- это Local CCC.

Естественно, что все-все возможные системы
с зависимыми типами на практике не нужны.
Какие-то из них вполне впихиваются в топосы.

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


"Полезные" системы определю так --
те, которыми можно описать основную функциональность
"обычного" процессора, описать все алгоритмы
в императивном (!) стиле, которые имеют
экспоненциальную сложность, сформулировать теоремы
про ExpTime/ExpSpace-сложность этих алгоритмов и доказательства.
По моему мнению, система, в которой можно
делать такие вещи, уже будет "полезная".

Почему в императивном, а только для того,
чтобы можно было производить reasoning
по поводу низкоуровневой оптимизации.
Думаю, за глаза хватит уникальных типов.


(13 comments) - (Post a new comment)


[info]nealar
2008-12-26 01:41 pm UTC (link)
1. Что такое "полезные" системы типов? Некоторым и сишной типизации хватает на все случаи жизни.
2. Логичней спросить это в ru_deptypes.
3. Сомневаюсь, что кто-то тут освоил и ТК и зависимые типы.

(Reply to this) (Thread)

[info]nivanych
2008-12-26 01:53 pm UTC (link)
> Что такое "полезные" системы типов?

Имеются ввиду достаточно мощные логики...
Например, достаточные для описания работы процессора
и утверждений с доказательствами про ExpTime/ExpSpace
сложности конкретных реализованных алгоритмов.
Этого, думаю, хватит для большинства практического.

Вот например, система типов Coq впихивается в топос?
Большую часть я знаю, как упихать, но есть ньюансы.
Но вроде бы, решаемые ньюансы.

Если буду знать, что таки можно обойтись топосами,
это очень многое упростит, и заодно, читать меньше надо будет.
Интуиция говорит, что можно...

> Логичней спросить это в ru_deptypes

Уже...

> Сомневаюсь, что кто-то тут освоил
> и ТК и зависимые типы.

А что же делать?...
Ну, читать дальше.

Однако, ответ меня как-то бы направил.
А то всё подряд читать -- это много.

(Reply to this) (Parent)

[info]antilamer
2008-12-26 04:31 pm UTC (link)
Эх, что-то ты все про топосы да про топосы. Надо, чтоль, и мне их постичь. Порекомендуй какой-нибудь вдохновительный источник, чтоб не просто определение, а со смыслом?

(Reply to this) (Thread)

[info]nivanych
2008-12-27 07:10 am UTC (link)
> Эх, что-то ты все про топосы да про топосы.

Красивая теория, вот и заболел ;-)

Процитирую классиков (J. Lambek, P.J. Scott) --

We decry overzealous application of Occam's razor.

We believe that type theory is
the proper foundation for mathematics

We believe that free topos, constructed linguistically
but determined uniquely (up to isomorphism)
by it's universal property, is an acceptable
universe of mathematics for a moderate intuitionist,
and therefore, that Platonism, formalism and intuitionism
are reconciable philosophies of mathematics.
;-)

Не могу сказать, что хорошо освоил эту теорию ;-|
И поэтому, наверное, квалифицированно посоветовать,
с какой именно книжки начать, не смогу, на мой взгляд,
тут всё очень и очень интересное (всё такое вкусное).

Топосы замечательно описывают большую часть как геометрии,
так и логики, а что тебе больше интересно, я не знаю.
У Джонстона весьма полное описание, но читать его задолбаешься.
Я начинал с "Intro to higher order categorical logic".
Сейчас читаю про "Sheaves in Geometry and Logic",
потом буду читать про конструктивную теорию категорий на ML.

Для прочтения многих из этих книжек желательно знать
теорию категорий до понимания сопряжённых функторов.

Прочитал не всё (отчасти, поэтому и задал вопрос в посте).
Но по крайней мере, каждую из них внимательно просмотрел.

Saunders Mac Lane
leke Moerdijk --
"Sheaves in Geometry and Logic,
A First Introduction to Topos Theory"
Сейчас читаю. Как раз про "смысл" топосов много.

Peter T. Johnstone --
"Sketches of an Elephant, A Topos Theory Compendium"
Эта метафора в названии именно про "three blind man",
учитывая объём книжки в 1100 страниц, интригует ;-)
Оно хоть и большое, и в него, как выражается [info]ivan_ghandhi,
"всего понапихано", но там хорошо рассказано про логику
(в ней я уже немного разбираюсь, и думаю, смог оценить).

P. T. Johnstone --
"Topos Theory".
Его более ранняя книжка, которую [info]ivan_ghandhi
более рекомендовал, чем "наброски слона".
Есть в русском переводе, только пара страниц испорчена.

J. Lambek, P.J. Scott --
"Introduction to higher order categorical logic"
Хорошая книжка от классиков (я с неё начинал).

B. Jacobs --
"Categorical Logic and Type Theory"
Она мне не очень нравится по стилю,
но содержит много интересного.
Может, потом возьмусь прочитать полностью.

Чуть не забыл.
Р. Голбдлатт --
"Топосы.
Категорный анализ логики"
Где-то было и на английском.
Но на мой вкус, по бОльшей части,
перевод хороший, вполне нормально
и на русском читается.
Если читать сначала, то как мне показалось,
почти не требует знания математики, то есть,
как введение в теорию категорий тоже годится.
Почему она мне в школе или
на первом курсе не попалась?... ;-\

Michael Barr, Charles Wells --
"Toposes, Triples and Theories"
Как ты, наверное, понял, "triples" -- это монады.
Надо будет почитать, интересно про монады в топосах.

D.E. Rydeheard, R.M. Burstall --
"Computational Category Theory"
Тут всё на ML, и топосы тоже затрагиваются.
Как дочитаю "Sheaves in Geometry and Logic",
примусь за эту книжку, думаю, быстро прочитаю.

John L. Bell --
"The Development of Categorical Logic"
Тут кратенько всё про всё
и Kripke-Joyal в частности.

Benno van den Berg --
"Predicative topos theory and
models for constructive set theory"
Может быть, будет интересно...
"Constructive set theory" --
это ж и как язык программирования годится.


Остальное из того, что у меня есть,
я либо не очень подробно смотрел,
либо мне не понравилось.

"Есличо", моё емыло и джаббер --
Nick сабака Ivanych.net

(Reply to this) (Parent)(Thread)

[info]antilamer
2008-12-27 09:21 am UTC (link)
Ох, ничего себе! Спасибо; вскоре доберусь и почитаю что-нибудь; начну, пожалуй, с Computational category theory - я ее уже мельком видел и она мне очень понравилась.

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-27 10:08 am UTC (link)
> Ох, ничего себе!

А то! ;-)

> начну, пожалуй, с Computational category theory

У меня есть, в том числе, и личный интерес к тому,
чтобы побольше людей занимались этими вещами.
Кому-нибудь помогу, глядишь, и мне кто-нибудь потом поможет ;-)
Одному всегда сложно.

Надо бы составить список книжек для совсем начинающих.
Обещался, в конце концов...

> я ее уже мельком видел и она мне очень понравилась

Я где-то половину прочитал, не очень понравилось.
Но дальше, вроде, гораздо красивее.

(Reply to this) (Parent)

[info]beroal
2009-01-02 02:22 pm UTC (link)
Слушай, а что ты можешь сказать про связь топосов и алгебраической геометрии и алгебраической топологии? А то Джонстон для меня слишком заумен, а сентенции типа:
space ∼ logical theory
point ∼ model of the theory
open set ∼ propositional formula
sheaf ∼ predicate formula

слишком расплывчаты.

(Reply to this) (Parent)(Thread)

[info]nivanych
2009-01-04 10:09 am UTC (link)
> Слушай, а что ты можешь сказать про связь
> топосов и алгебраической геометрии
> и алгебраической топологии?

Во-первых, скажу, что в геометрии я плохо разбираюсь.
И в топосной геометрии тоже, я её начну подробно читать
после того, как сочту, что с логикой разобрался достаточно.

Во-вторых, топос Гродентика (плоховато понимаю, что это такое) --
это частный случай элементраного топоса, то есть, описывается в его рамках.

> А то Джонстон для меня слишком заумен,

И для меня, пока что, тоже...
Ну ничего, сегодня продолжил читать
"Sheaves in Geometry and Logic".
Одновременно читаю про конструктивную
теорию категорий на ML, там и топосы есть.
А Джонстон... я до него ещё доберусь ;-)

> а сентенции типа:

> space ∼ logical theory

Это может быть так.
Может быть и не так.

> point ∼ model of the theory

"point", как я понимаю, это 1 -> a ?
Тогда это тоже спорно.
Хотя и можно построить такой топос.

> open set ∼ propositional formula

Непонятно.

> sheaf ∼ predicate formula

.

Не берусь полноценно это комментировать ;-)
Поскольку эти высказывания такие, что либо
я их не очень понимаю (и надо требовать уточнения),
либо о этом кратко не расскажешь.

> слишком расплывчаты.

Да уж.
Где ты это взял?... ;-)

(Reply to this) (Parent)(Thread)

[info]beroal
2009-01-04 01:41 pm UTC (link)
> point ∼ model of the theory
"point", как я понимаю, это 1 -> a ?
Тогда это тоже спорно.

Думаю точка топоса. Топос — это обобщение топологического пространства, точнее, категории пучков над топологическим пространством. Ну а у пространства есть точки. Таблица из
Steven Vickers. Locales and toposes as spaces.

(Reply to this) (Parent)(Thread)

[info]nivanych
2009-01-04 02:40 pm UTC (link)
В теории категорий (и топосах в частности)
считается стандартным считать за "точку" стрелку 1 -> a.
Это так же в топол. пространствах и множествах,
по крайней мере, основанных на топосах.

В терминологии теории типов это "терм типа a".

Если 1 -> a -- это точка и модель теории,
то это значит, что составили такую категорию,
где объекты это формальные теории. Это возможно.
То есть, 1 -> a -- это некая конкретная теория,
ну и a -- это некая "общая теория".
Как-то так...

Ничего. Опять разгребу накопившиеся дела, продолжу читать.

Кстати, я вот тут пытаюсь сделать что-то типа
ещё одной конструктивной теории, где объектов нет,
где их заменяют, как написано у тов. Маклейна, id-стрелки.
Категория -- это частичная полугруппа с левыми-правыми единицами.
Впрочем, любую полугруппу (и частичную тоже)
всегда можно дополнить левыми-правыми единицами.
На первый взгляд, получается проще и красивее.

Книжку скачал, просмотрю.

P.S.
А у меня теперь новый нотбук --
могу читать хоть в сортире ;-)

(Reply to this) (Parent)

[info]nivanych
2008-12-27 07:21 am UTC (link)
Подскажи-ка мне вот ещё что...
Я вот написал про "практически полезные" системы.
Но действительно, надо было сразу сформулировать чётче.

В ответе [info]nealar'у я написал про то,
что формальная система, в которой можно описать
работу процессора, алгоритмы до экспоненциальных,
что забыл подчеркнуть, в императивной формулировке
и утверждений с доказательствами про их ExpTime/ExpSpace,
будет достаточной для практических применений.

Вроде бы, и правда достаточно.
А ты как думаешь?

Есть ещё тонкий момент, касающийся корекурсии,
но его пока касаться не будем.

(Reply to this) (Parent)(Thread)

[info]antilamer
2008-12-27 09:30 am UTC (link)
Ну вообще совсем уж практически полезными по-моему можно назвать только "тьюринг-полные" системы - а то что это такое: интерпретатор брейнфака не написать.
То есть, утверждение "нам не нужны задачи со сложностью в худшем случае больше экспоненциальной" не совсем верно: скорее, нам не нужны худшие случаи этих программ.
Для системы типов, допускающей все практически полезные алгоритмы на всех разумных входных данных, понадобится поставлять с каждым входом доказательство того, что сложность алгоритма на нем будет субэкспоненциальной, что, по-моему, не выглядит практичным. Например, для интерпретатора брейнфака это будет полный пипец.

Так, похоже, можно и придти к неутешительному выводу, что из системы типа Coq "слова не выкинешь", и системы с зависимыми типами обречены на простые алгоритмы или огромные усилия для их запуска.

(Reply to this) (Parent)(Thread)

[info]nivanych
2008-12-27 10:48 am UTC (link)
> Ну вообще совсем уж практически полезными
> по-моему можно назвать только "тьюринг-полные" системы

Скажем так, все знают, что ими получится
описать любую из практических задач.

Посему предлагаю метаязык, по мощности
превосходящий любые Agda/Coq'и --
бестиповая лямбда с возможностью
обозвать любой терм одним словом ;-)

Шутки шутками, но такой язык и правда
получается заметно мощнее Coq/Agda'ы.
Более того, (теоретически) можно составить
библиотеку, с помощью которой даже не будет
сильно менее удобно программировать, чем в Coq.
Наверное, это минимальный язык, имеющий мощность Lisp'а.

> а то что это такое: интерпретатор брейнфака не написать.

Да, косяк.
Но можно написать интерпретатор brainfuck'а
с зависимыми типами, без общей рекурсии, то есть ! ;-)
Это было бы сильным цирковым номером :-)
Только вот, с точки зрения решения практических задач,
накойхер нам brainfuck или бестиповая лямбда?

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

Так оно.
Правда, даже просто-типа-лямбда
с (ко)рекурсией может уже сверхэкспоненциальное.
Coq со своими зависимыми типами может уже ооочень многое.

> Для системы типов, допускающей все практически полезные алгоритмы
> на всех разумных входных данных, понадобится поставлять с каждым входом
> доказательство того, что сложность алгоритма на нем будет субэкспоненциальной

Зачем?...
Я говорил о системе, в которое это _возможно_ сделать,
про возможность, как об одном из критериев "полезности"...
Просто лучше пока не придумал.

Ну пусть ограничимся 2^(2^(2^N)), один хрен,
алгоритм с такой худшей сложностью уже малоприемлем.
А если добавить ещё одну 2-ку, так и совсем.
И Coq это может.

Правда, стоит заметить, что я не слышал доказательств
про то, что любая программа (например) на просто-типа лямбде
с (ко) рекурсией не будет иметь сложность, более такой-то.
Но наверное, это так.

Не очень уверен, но всё-таки уверен, что по крайней мере,
большинство алгоритмов можно навостриться писать,
используя (ко)рекурсию и испытывать при этом удобство ;-)

Ну и к тому же, можно отдельно вставить общую рекурсию.
И 100 раз написать, что "мы не хотели, но пришлось".
Ну и к ней всякие фишки типа вывод типа рекурсии,
прикидываю, что можно сделать вывод, который
довольно часто будет способен вывести тип рекурсии.
Если отмести корекурсию, то я даже знаю, как это сделать.
Наполовину доказываюсь, как быть и в случае корекурсии.
Просто почти не думал об этом.

> Так, похоже, можно и придти к неутешительному выводу,
> что из системы типа Coq "слова не выкинешь",

Пожалуй.
Выкинуть можно только типы Type и Prop.
Но в полезности или вреде этого я окончательно не уверен.
Во всяком случае, в рамках дискуссии,
ничего кардинально это не перевернёт.

Вот что точно, так это то, что тактики должны
реализовываться правильным метапрограммированием,
а не подъязыком, заложенным в основной.
Может, я что-то не понимаю?...

> и системы с зависимыми типами обречены на простые алгоритмы

Не уверен.
Вспоминая, например, алгоритмы на графах,
могу сказать, что, как минимум,
многие из них реализуются красиво.

Но конечно, у меня тут опыта мало.
Много алгоритмов на графах я писал
ещё тогда, когда даже не подозревал
о существовании мощных теорий типов ;-)

> или огромные усилия для их запуска.

Мне кажется, что разговор вполне сводится
к дискуссии о практическом (не)удобстве
программирования, используя только (ко)рекурсию.
Вот что точно, так это многое тут делается
просто и красиво _даже_ без зависимых типов.

(Reply to this) (Parent)

(13 comments) - (Post a new comment)

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