nivanych: A Topos Foundation for Theories of Physics

Николай Иваныч (

nivanych) wrote,
@ 2009-01-28 20:15:00

A Topos Foundation for Theories of Physics
Зацените!
В том числе, это то,
о чём я давно говорил.
Только уже реализованное.
http://math.ucr.edu/home/baez/topos_physics
Спасибо

dsav, это он нагуглил.

(71 comments) - (Post a new comment)

	kurilka 2009-01-28 08:10 pm UTC (link)
	Ты это прочитал? Вкратце не скажешь что там у них получилось? Коммент "no figures" как-то смущает :) Даже диаграмм нету чтоль? (Reply to this) (Thread)

nivanych
2009-01-29 07:26 am UTC (link)

Нет, я не прочитал.
У меня и так дофига, чего читать... (вроде как, оправдение)
Только кратко просмотрел.

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

Описание топосной модели -- это уже половина пути
к представлению моделируемого в компутерном языке.

А представление физики в языках программирования,
по-моему, это очень и очень круто и правильно.
Если представили в топосе, значит, при некоторых упрощениях
возможно представить и в зависимых типах (Agda/Coq).

(Reply to this) (Parent)(Thread)

	kurilka 2009-01-29 07:32 am UTC (link)
	Блин, может подскажешь как в эти топосы проще всего повникать? Почитал определение, увидел знакомые и не очень слова, но толком не понял о чём речь :) (Reply to this) (Parent)(Thread)

nivanych
2009-01-29 07:45 am UTC (link)

Как раз думаю, как попроще повникать.
Ну вот, с точки зрения языка программирования.
Пока что попробуй порассматривать категории,
как их ... ну короче, в которых есть
начальный-терминальный объекты и
(ко)произведения с экспонентами.
Рассмотри такие категории, как языки программирования.
Только про равенство не забывай.
Бидекартово замкнутые, что-ли...
Потом попробуй понять, что такое уравнитель.
Потом -- коуравнитель.
Потом -- любые пределы.
Потом классификатор.
Если стрелки не слишком мощные,
и (ко)уравнители всегда можно вычислить,
то это получится уже будет один из вариантов
так называемого pretopos'а или predicative topos'а.
Вроде, не ошибся.

Есличо, обращайся.
Мне ж надо тренироваться объяснять ;-)
Да и сам я не скажу, что самый понимающий,
в процессе объяснения и пойму лучше.

P.S.
А "тот самый" язык придумался.
На 90% это (наверное) максимально возможно простая
система с зависимыми типами, в которой, из вредности,
всё обозвали категорными терминами ;-)
Одновременно получилось простое объяснение зависимых типов.
Сейчас вот не дышу, боюсь спугнуть :-)
Смотрю, где ж я ошибся.
Более-менее впихну это в свою голову,
проверю, всё ли правильно, тогда расскажу.

	ivan_ghandhi 2009-01-28 08:13 pm UTC (link)
	О. Осуществилась вековая мечта человечества... может быть, и математики в конце концов признают, а? Было бы любопытно. (Reply to this) (Thread)

	kurilka 2009-01-28 08:20 pm UTC (link)
	А чего, есть какое-то неприятие топосов в стане математиков? (Reply to this) (Parent)(Thread)

	ivan_ghandhi 2009-01-28 09:12 pm UTC (link)
	У меня было такое ощущение, что топосы по-прежнему считаются "абстрактной чепухой". (Reply to this) (Parent)(Thread)

	kurilka 2009-01-28 09:18 pm UTC (link)
	Ну для меня пока они таковыми остаются, ну, надеюсь, пофиксим этот недочёт. (Reply to this) (Parent)

	nivanych 2009-01-29 07:29 am UTC (link)
	+1 (Reply to this) (Parent)

	nivanych 2009-01-29 07:26 am UTC (link)
	Боюсь, математики будут последними, кто признает ;-) ;-) (Reply to this) (Parent)

	nivanych 2009-01-29 07:34 am UTC (link)
	Кратко проглядел, ощущения похожие. Сейчас я хоть понимаю ;-) (Reply to this) (Parent)(Thread)

	kurilka 2009-01-29 07:35 am UTC (link)
	Хоть - это по сравнению с чем? (Reply to this) (Parent)(Thread)

	nivanych 2009-01-29 07:48 am UTC (link)
	Ну, по сравнению со мной же, но раньше. Радуюсь я за себя, понимаешь? ;-) Просто были моменты, когда всё это было, как и сейчас, жутко интересно, но нихрена не понимал. (Reply to this) (Parent)(Thread)

	beroal 2009-01-29 12:17 pm UTC (link)
	О. Так я давно об Isham слышал. Почитайте этот комментарий. (Reply to this) (Thread)

	nivanych 2009-01-29 03:18 pm UTC (link)
	Мда. Откуда же, всё-таки, такая тенденция общаться со мной на "вы" ;-) Обязательно прочитаю. Но только завтра :-) (Reply to this) (Parent)(Thread)

	beroal 2009-01-29 03:35 pm UTC (link)
	Я обращаюсь ко всем читателям твоего блога! :) (Reply to this) (Parent)

	nivanych 2009-04-12 03:41 pm UTC (link)
	Да, причём, на прологе ;-) Имеется ввиду, что топосное описание, это уже почти что описание в интуиционистской логике. Язык же, конечно, должен быть "достаточно сложным". Скажем, Coq/Agda подойдут. (Reply to this) (Parent)(Thread)

	kurilka 2009-04-12 02:52 pm UTC (link)
	Физику описывать на языке программирования? (Reply to this) (Parent)(Thread)

	vlkamov 2009-05-19 10:16 am UTC (link)
	> Andreas Döring and Chris Isham Дюринг !? (Reply to this) (Thread)

	nivanych 2009-05-19 10:19 am UTC (link)
	;-) Нет, Энгельс. Евгений Дюринг уже умер. А Энгельс живёт вечно. (Reply to this) (Parent)

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

About

Help

Get Involved

Legal

Store

LJ Labs