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

The Fleet architecture uses
a uniform switch fabric to simplify chip design.
A few thousand identical copies of a
programmable interface connect a
thousand or so repetitions of
basic arithmetic, logical, input-output,
and storage units to the switch fabric.
The uniform switch fabric and its
identical programmable interfaces replace
many of the hard parts of designing
the computing elements themselves.
http://syndicated.livejournal.com/planet_haskell/484984.html

Сейчас наблюдал увлекательнейшую дискуссию
на тему "Как правильно переводится "so fucking what".

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

Вот оно как!
http://topos-physics.org

А именно.

Отец купил пару ульев и завтра
я поеду ему помогать перевозить пчёл.
Так как с отцом я общаюсь часто,
то постепенно буду знать всё больше и больше
про пчёл, а главное, про правильный мёд :-)

Оказывается, если забыть перевести регистр,
то ПW-претопос и ПWM-претопос пишутся, как
ПЦ-претопос и ПЦЬ-претопос, соответственно!

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

Там много картинок этого "уровня" --
http://hectop.livejournal.com/719936.html

По-моему, восхитительно!
Нашёл через тов. nponeccop

Возникли у меня по поводу предстоящего
сборища "MskHUG" некоторые сложности.
Сложности не с тем, чтобы приехать.
А с тем, что есть куча глупых дел и думать
про действительно важные важные и нужные,
и что немаловажно, интересные вещи, сложновато.
Я пока не умею "5 минут подумать про категории",
надо как-то посидеть, "раскрутить мозги"...

( Но постараюсь. )

Вот подтверждающая ссылка --
http://ethology.ru/news/?id=541

Система -- 64-битный Gentoo Linux.
Можно сказать, специально
для предстоящего сборища
купил себе нотбук, а туут...
( Симптомы такие )
Проблема решилась установкой ядра 2.6.28.
Вникать подробнее нет никакого желания.

Цитирую --
"
Думайте о том, как применить навык
вашего персонала в новом деле, кризис --
это лучшее время для новых прорывных идей.

Технари, кого сократили и у кого руки
растут не из зада, обращайтесь ко мне.
Мне вы нужны.

Банковских работников и топ-топ-топ
менеджеров различных направлений --
просьба не беспокоить.
Мне вы не нужны.
"

Занимаются видеонаблюдением.
Это где-то в подмосковье.
Ссылка на конкретный пост --
http://tony-fly.livejournal.com/33495.html

Для дальнейших подробностей нужно
либо обратиться непосредственно к tony_fly,
либо посмотреть его журнал.

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

Категорная модель higher order типов -- это топос.
Категорная модель зависимых типов -- это Local CCC.

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

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

( Дополнение )

Начало декабря, а у нас всё небольшой плюс,
и из-за этого -- грязища страшная!...
Уж лучше небольшой холод в минус несколько,
чем тепло, но грязь... Гораздо лучше!

Во что обнаружил!
http://www.cs.man.ac.uk/~david/categories

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

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

Интересно.
Интересно, кому-нибудь, кроме меня,
такая мысль в голову приходила?

Во какое обнаружил!
Наш ответ на Шнобелевку.
http://molbiol.ru/cb/97497.html

На одном дыхании и без последующего редактирования.
( Осторожно! Тут что-то типа дыбра! И возможно, опечатки. )

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

( ТУТ )

Изучал я применения топосной логики
и для этого выбрал метод придумывания языка.
Ну так вот, в процессе попыток упрощения
пришёл к категорной семантике term rewriting.
Ну об этом как-нибудь потом, не люблю рассказывать
что-то, плохо додуманное, буду дальше читать.

Так вот, и тут-то я вспомнил про Maude,
за которым с давних пор время от времени поглядываю.
Настоятельно рекомендую всем его посмотреть --
http://www.cs.swan.ac.uk/~csneal/MaudeCourse/SubSorts.html
и далее по ссылкам "Next".
Эти мои изучения нежданно-негаданно
привели к пониманию Maude ;-)
Причём, и штука-то это очень простая!

Теоретически етой штукой можно описать что угодно --
хоть системы типов вплоть до навороченных зависимых.
Но что меня впечатлило, так это наглядная демонстрация
излишеств навороченных систем типов.
Я не говорю, что они совсем не нужны, но оказывается,
без них можно очень запросто обходиться во многих задачах,
имея не меньшую эффективность при решении!
Лично я заинтересовался Maude, как практическим пособием
по применению term rewriting'а для практических задач.
Term rewriting "был всегда" ;-), но вот оказывается,
под него можно вполне удобно делать многие вещи.
Просто технику программирования не развивали ;-)
Там есть замечательные примеры моделирования железяк.
Да, и Кнут-Бендикс для егоных систем тоже реализован.

Только недавно я понял близость term rewriting
с конструктивной теорией категорий, и Maude как-то лучше
очертил границы практической применимости этой близости :-)
В общем, вчера были сплошные инсайты ;-)
Но об этом -- в следующем посте.