(no subject)

Не могу не процитировать коллегу zabolekarя:

Видел плакат: «в любой войне цивилизованного человека с дикарём будь за цивилизованного человека. Против джихада».

Феноменальный аргумент вообще. «В любой войне цивилизованного человека с дикарём будь за цивилизованного человека. За римлян. Против Бар-Кохбы».

Джихад я видал азой тиф ин др эрд, аз ди эрд из гурништ азой тиф. Не о нём речь. Речь о понятии цивилизованности. У большинства говорящих о ней это не понятие вовсе, а нечто смутное, вида «кто мне нравится, тот и цивилизованный». Простой пример — Вторая Мировая. Кто не любит русских, пишет, как советские варвары не щадили никого. Кто не любит европейцев, пишет про примитивных и жестоких варваров с континента Europa. Я думаю, если Юрий Нестеренко и Фридомкрай встретятся, они аннигилируют. Оба хорошие поэты, оба любят тонко провоцировать, оба резки и принципиальны, у обоих довольно нестандартные взгляды, и насколько же эти взгляды различаются!

Говорят, когда Ганди спросили, что он думает о западной цивилизации, он ответил: «было бы неплохо».

(no subject)

Когда я разрабатывал метод фильтрации фона в изображениях для проведения измерений, я всё думал, как же именно наш глаз это делает, неужели просто вычетает плавно меняющуюся во времени и пространстве часть видеопотока? Да! Именно так он и делает, см. http://avva.livejournal.com/2487551.html. Да, действительно, если смотреть в центр этой картинки не моргая и не двигая взглядом, через приблизительно 20 секунд на месте картинки белый фон. Когда я научился фиксировать взгляд, мне стало хватать 5 секунд.

Без коментариев

История от dirinfo: “Мама, двое детей дошкольного возраста, бабушка, дедушка. Мама заканчивала нашу школу. Мама умирает в возрасте около тридцати - пневмония, врачи упустили. Бабушка с дедушкой, порядочные люди, любящие своих внуков и готовые на все ради них, само собой, начинают оформлять опеку на детей. Знаете, что им сказали в опеке? Там сказали - ваши доходы не позволяют оформить опеку на обоих. Только на одного. Второго — в детдом. Так что решайте сами, кого куда.”

Первый комментарий (annakora): “.. семья должна быть абсолютно прозрачной. Контроль за семьями должен быть пристальным и жёстким. У нас такое в семьях, за закрытыми дверьми, творится — Хичкоку не снилось.
А когда каждая мамашка будет знать, что за нерадивость она будет наказана, и жёстко наказана — может, меньше детей будет погибать и калечиться.”

Спасает этот треш только разумный комментарий vitus_wagnerа: “[..] требование от семьи соответствовать каким-то формальным критериям может привести к бесчеловечным результатам. Никакое совершенствование формальных правил тут не поможет, потому что жизнь бесконечно разнообразнее любых формальных правил.
[..]
Ему /чиновнику опеки/ надо, чтобы инструкция была выполнена. Те, кто его будет контролировать, никогда не увидят за строчками отчетов живых детей. Поэтому карьера чиновника, прибавка в зарплате в пару тысяч рублей зависит от соблюдения инструкций. А значит, если инструкции противоречат жизни, и ради их выполнения нужно сломать несколько судеб, судьбы будут сломаны.”

Upd: Это я к тому, что именно священнозлобный пыл людей вроде автора комментария выше делает возможным существование органов опеки (во многих странах) в их текущем виде — молохов, наделённых исключительным правом нарушать habeas corpus и презумпцию невиновности; организаций, лишенных легитимности, прозрачности и ответственности суда, но наделённых властью, даже превышающей судебную.

Желание обратиться к такому людоедскому Левиафану, чтобы «нерадивых матерей жестоко наказывали» со стороны, вероятно, такой же матери, только ”радивой“ очень напоминает мне трагикомическую историю двух последних евреев Афганистана (Зебулона Симентова и покойного Исаака Леви), которые не поделили кабульскую синагогу и исправно писали друг на друга доносы в Талибан, который по очереди их арестовывал и подвергал пытком, а в итоге просто уничтожил предмет раздора — ценнейший экземпляр Торы XV века.

И я понимаю, зачем нужны и чем ценны уроки этики и права в немецких школах — очень, очень важно на всем понятных примерах донести до как можно более широких слоёв населения (прежде чем они смогут голосовать!), что первобытные средства поддержания порядка — ярось, злоб и месть — конечно естественные, ”правильные“ и ценные чувства, но крайне плохие советчики. Что характерной чертой варварского общества, необходимой и достаточной, явлется неумение/нежелание/непривычка их членов тем или иным образом канализировать деструктивные эмоции и включать голову.

Веха

Напомню, что HoTT это такая теория типов с филигранным подходом к равенству. Казалось бы, чего можно офилигранить в том, что 1=1?

Мотивация: предположим, у нас есть две абстрактные прямые А и B, обе состоят из континуума плотно линейно упорядоченных точек. Равны ли они?
Они конечно равны однако существует масса неэквивалентных способов идентифицировать на них точки!
Чтобы идентифицировать прямые конкретно, нужно на каждой из прямых выделить по две точки — ноль и единицу, тогда получается что точки каждой из прямых идентифицированны с действительными числами, а стало быть между собой!

Равенство это не «факт», а множество способов идентификации двух объектов.
В HoTT мы пишем A = B и подразумеваем, что множество идентификаций А и B, обозначаемое [A = B] не пусто.

Сами «идентификации», это такие зверьки которые позволяют из фактов про A выводить факты про B. То есть, если для утверждения p про A есть доказательство ev: p(A), то идентификация t: [A = B] даёт нам доказательство t(ev): p(B) такого же утверждения про B.

В том числе, если f(x) = z и t: [x = y], то f(y) = z и в частности f(x) = f(y). Конечно же, использование разных идентификаций из [x = y] даёт разные идентфикации f(x) = f(y).

Примечание 1:
Среди идентификаций двух прямых A и B не существует какой-то выделенной, все их них равноправны. Одну и ту же прямую (скажем, A) тоже можно идентифицировать с собой множеством способов, однако среди них есть выделенный — каждая точка идентифицируется сама с собой. В отличие от классической математики, HoTT понятия «такой же» и «тот же самый» различаются. «Такой же» — это наблюдаемая эквивалентность, максимум что можно сказать о двух данных объектах, не зная их “происхождения”, это что они равны то есть «A такой же как B». Понятие «тот же» это не объективное, а номинальное свойство: A и B ссылаются на один и тот же объект в том и только в том случае, если B было определено через let B := A или соответственно А через let B := A. Для номинальных свойств не выполняется preservation, т.е. подстановка определения вместо определяемого, стирает информацию о тождественности. Данная ситуация совершенно эквивалентна нарушению preservation отношению подтипизации в DOT, что подсказывает возможные пути развития DOT — при необратимых подстановках следует генерировать свидетельство отношения подтипизации и таскать его с собой.

Примечание 2:
Пример с прямыми обобщается на любые алгебраические структуры: с точки зрения HoTT изоморфные реализации алгебраичсккой структуры равны, а изоморфизмы это «способы идентификации». Доказательство этого примечательного факта было опубликовано три дня назад, и это капитальная веха на пути подтверждения состоятельности HoTT.
(http://homotopytypetheory.org/2012/09/23/isomorphism-implies-equality/, не обращайте внимания на идеосинкратическое кодирование модулей, это издержки обозначений.)

Примечание 3:
Объекты (в т.ч. реализации алгебраических структур) равные себе одним единственным образом, называются жёсткими. Равенство между жесткими объектами с одной стороны очень похоже на обычное теоретиком-множественное равенство, а с другой гораздо лучше отражает интуитивно-верную суть вещей, т.к. не делает разницы между разными моделями одной и той же сущности: так например разные модели ряда натуральных чисел (скажем, модель Frege и модель Peano) в теории множеств не равны, тогда как разные минимальные реализации структуры NatObject в HoTT равны. Более того числа 2_Frege и 2_Peano не равны в теории множеств, не сравнимы (будучи объектами разных типов) в ITT и ETT, и равны в HoTT, что полностью соответствует интуитивному пониманию вопроса.

Платоническую мотивацию я, вроде объяснил, но некоторые программисты, даже очень уважающие философию, всё-таки жаждут конкретных примеров практического применения.

Приложение в математике:
Тип С «набор из N элементов» в обычных типизированных лямбда-исчислениях сконструировать невозможно — у всякого типа данных D должны быть нормальная форма, которая позволяет проверить равенство двух выражений типа D приведением к нормальным формам и сличением. А у «наборов из N элементов» нормальной формы нет — нельзя на компьютере сохранить набор произвольных элементов таким образом, чтобы элементы при этом оставались равноправными, как не извращайся, в процессе сохранения прийдётся расположить элементы в каком-то произвольном порядке.

Что же делать? В HoTT требование канонической нормальной формы смягчается, тут можно изготовить из типа нормальных форм (L = «список из N элементов») и группы симметрий, действующей на нём (тип S = «перестановка списка из N элементов») фактортип M = L/S. Это такой тип который технически состоит в точности из элементов L, однако функции из него f': M => X это только такие функции f: L => X из списков, для которых доказано, что они не зависят от порядка элементов в списке, т.е. s: S => f.s = f. Таким образом получается, что каждый элемент M эквивалентен сам себе |S| разными способами.

Приложение в физике:( Read more... )