В современной теории типов выделяют два основных класса равенств: Definitional equality и Propositional equality. 
 ( Ого! Ну-ка, ну-ка... )

 Ян 

( Read more... )

Итоги сессии. Досаждающей популярностью стали пользоваться микронаушники. Вот раскопал рекламу:

Click to view

Если использование обычной шпаргалки выявить при должном тщании и опыте довольно просто, то в случае микронаушника уход студента в несознанку требует действий на грани вторжения в личное пространство. При этом само выявление использования происходит по ( Read more... )

Обогатил ру-Википедию стать ей про это дело. Ловите. Надо бы ещё, конечно, понаписать про точное определение и всякие свойства, но пока лень.
UPD: Понаписал про формальности.
UPD2: Добавил типизацию по Карри с классическим примером, демонстрирующим, что System F богаче просто-типа-лямбды. И готовящим читателя к рассуждениям про импредикативность и ( Read more... )

Originally posted by alliruk at Это даже не децимация
По ссылке из обсуждения в "Коммерсанте" интервью Я.Кузьминова (спасибо некой vasilisa44 с пустым журналом) обнаружил любопытный документ:

План мероприятий «Изменения в отраслях социальной сферы, направленные на повышение эффективности образования и науки» (дорожная карта), утвержденный распоряжением ( Read more... )

Блин, поганый ЖЖ!
Случайно, одним неловким движением, удалил весь десяток своих комментов к посту http://deni-ok.livejournal.com/47912.html#comments.

И где undo?

Originally posted by prahvessor at УИКи: краткий отчет о непроделанной работе и ЦУ
29 (по другим сведениям, 23) января заканчивается срок приема заявок на то, чтобы стать членом УИК с решающим голосом. Ну это так было удобно устроено, чтобы на новогодние каникулы пришлось. Говорят ТИКи работают (Кто говорит? - Чуров говорит (с)), но проникнуть в них нельзя - ( Read more... )

От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо 

( Read more... )

Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите. Originally posted at http://deniok.dreamwidth.org/47521.html. Feel free to comment here or there.

Поправил в ru-Википедии своё же описание понятия зависимости одного от другого, долгое время меня раздражавшее. Поправил на более аккуратное, основанное на PTS-подходе. Что-то больно формально вышло, но проще уже слишком много профанации. Держите, вобщем. Originally posted at http://deniok.dreamwidth.org/47237.html. Feel free to comment here or ( Read more... )