nivanych

Наконец-то (как выражается афтар поста),
все мы можем погладить кота в хорошем разрешении!

http://galeonis.livejournal.com/698726.html
И в частности --
http://pics.livejournal.com/galeonis/pic/003bd5qw

Обязательно повешу на стенку. С надписью.
Как там было в оригинале?...

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

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

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

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

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

( ТУТ )