ДР Цертуса 2011

(no subject)

Настоящим объявляю, что все мои персональные данные, тексты, фотографии, рисунки, переписка и т.п. являются объектами моего авторского права (согласно Бернской Конвенции), и оповещаю «ЖЖ» (LiveJournal, Inc / SUP Media) о том, что разглашение, копирование, распространение моей личной информации в коммерческих целях равно как и любые другие противоправные действия по отношению к моему профилю в социальной сети строго запрещены.

Для коммерческого использования всех вышеупомянутых объектов авторского права в каждом конкретном случае необходимо мое письменное разрешение.

Гёттинген
17 января 2015 г.
Александр Куклев
ДР Цертуса 2011

Интуиционистская лемма Цорна

Как известно, в интуиционистских теориях типов определимы только вычислимые тотальные `f : A -> B`. Теория типов не утверждает, что внутри типа функций `A -> B` не живёт ещё каких-нибудь (невычислимых) функций, но вот конкретно предьявить можно только тотально-вычислимые. А это означает, что у нас не может быть Тьюринг-полноты, т.е. как бы не была совершенна наша конкретная интуиционистская теория типов, найдутся такие (Тьюринг-)вычислимые функции из `A` в `B`, которые мы не сможем выразить термом `f : A -> B`. Тем не менее, в некоторых интуиционистских теориях типов, поддерживающих индуктивно-индуктивные фактортипы (гомотопическая теория типов и её близкие родственники) можно определить монаду ℧ частично-вычислимых функций, т.е. функций, которые могут в процессе вычисления значения “зависнуть”. И тут уж верно, что термом `f : A -> ℧(B)` можно выразить любую вычислимую функцию из `A` в `B`. Но этот тип, разумеется, содержит кроме тотально-вычислимых функций ещё и функции, которые на каких-то аргументах могут зависать.[1]

Разумеется, мы можем записать вот такой тип:
Property Totality[on f : X -> ℧(Y)]:
  ∀(x : X) ¬(f(x) = ⊥)
Разумеется было бы прикольно иметь оператор
totalize(f : X -> ℧(Y) with Totality) : X -> Y
Правильно ли я понимаю, существование такого оператора это в точности интуиционистская Лемма Цорна?

(NB: Без закона исключённого третьего, из Леммы Цорна никак не доказываются Аксиома Выбора и её эквиваленты.[2])

(NB: Разумеется, наличие такого оператора “небесплатно”. Как минимум, его наличие превращает разрешимость проверки доказательств в полуразрешимость. Но вполне возможно, что оно ещё как-нибудь хитро ломает вычислимость.)

[1] https://arxiv.org/abs/1610.09254
[2] John L. Bell, “Some New Intuitionistic Equivalents of Zorn’s
Lemma”, http://publish.uwo.ca/~jbell/Some%20New%20Intuitionistic%20Equivalents%20of%20Zorn.pdf
ДР Цертуса 2011

Medical imaging

Я очень давно не писал о прорывах по части томографии.

Во-первых, Philips уже аж год назад выпустила MRT-аппарат Ingenia Ambition, в котором для охлаждения катушек используется не тысячи литров жидкого гелия, а ровно семь. И в дозаправках не нуждается. Ну то есть раз в пять лет дозаправка производится в рамках техсервиса, и это всё. В качестве побочного эффекта, аппарат жрёт на порядок меньше электричества, и не нуждается в надёжных источниках бесперебойного питания. В отличие от обычных аппаратов, в которых если питание отключить, тысяча-другая литров жидкого гелия (дорогущего и ценного невозобновимого ресурса) просто улетит в атмосферу, и надо будет заливать новый, тут ничего такого страшного не произойдёт. Просто после включения электричества назад какое-то время оно всё будет охлаждаться, и всё.[1]

Во-вторых, начали массово заходить малые MRT-аппараты “для головы и конечностей”[2]. Они маленькие, они потребляют в разы меньше электричества, на порядок меньше гелия, при этом дают картинку лучше чем обычный аппарат (потому что отверстие для конечностей и головы можно делать более узким)[3], они вызывают на порядок меньше проблем у людей с клаустрофобией. Если говорить о чуть более дорогих аппаратах с полем 3T, то они ещё и очень быстрые — буквально три минуты чтобы отснять сустав или сломанную конечность, восемь минут на подробный снимок головы. Вот выпустит Philips (или конкуренты) такой вот аппарат с ультранизким потреблением гелия, и можно будет в каждый травмпункт ставить.

В-третьих, выпустили аппарат не только с открытым столом (очень помогает людям с клаустрофобией, позволяет без проблем делать MRT людям с подключенной капельницей, позволяет проводить биопсии и хирургические операции под MRT-контролем), но и при этом с наклоняющимся столом, чтобы снимать позвоночник под естественной нагрузкой.[4]

В-четвёртых, рентгеновская оптика дозрела и можно снизить радиационную дозу, получаемую при CT (компьютерной томографии) по меньшей мере в 300 раз без потери в качестве картинки.[5] Вот сейчас радиационная нагрузка от CT-скана всего тела около 20 мЗв. Для ударного облучения (т.е. не размазанного на многие месяцы, а вот в течение одного дня) это приличная доза. С одной стороны, при лечении рака лучевой терапией дозы бывают в сотни раз больше, с другой стороны, после получения такой дозы на производстве по нормативам положен полугодовой отпуск. А вот если уменьшить в 300 раз, то это уже будет выходить, что CT всего тела облучает меньше чем один трансконтинентальный перелёт на самолёте или стандартный рентген-снимок грудной клетки, это совершенно “ни о чём”. Если, как спекулируют авторы, можно дожать технологию и снизить облучение не в 300, а в 1500 раз без потери качества, то CT можно будет рутинно применять в том числе у новорожденных детей и беременных женщин. Комбинирование CT и MRI в одном приборе позволяет одновременно на порядок снизить количество артефактов (т.к. CT и MRT подвержены совершенно разным артефактам), вдвое уменьшить время процедуры и получить картинку со значительно большим количеством данных, чем CT и MRT дают по отдельности (это и данные о плотности костей, и более детально дифференцированные ткани).[6,7]

_______
1 — https://www.philips.com.au/healthcare/product/HC781356/ingenia-ambition-excel-in-your-daily-mr-services-helium-free
2 — https://www.esaote.com/en-GB/dedicated-mri/mri-systems/p/o-scan/
3 — https://www.ncbi.nlm.nih.gov/pubmed/29536587
4 — https://www.esaote.com/en-GB/dedicated-mri/mri-systems/p/g-scan-brio/
5 — https://www.ncbi.nlm.nih.gov/pubmed/29162913
6 — https://www.ncbi.nlm.nih.gov/pubmed/26429262
7 — https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4930897/
ДР Цертуса 2011

Вертолётное

На слово «вертолёт» я автоматически представляю себе сейчас Eurocopter EC-135 или MD Explorer — два очень похожих вертолёта для скорой помощи и поисково-спасательных операций. Оба имеют ротор диаметром чуть больше 10 метров, длину корпуса около 10 метров, и вмещают пилота, дюжего медбрата, врача и носилки-каталку. Размер достаточно маленький, чтобы можно было садиться на дорогу или на поле, вместимость как раз чтобы подходило в качестве скорой помощи. Разница между ними в основном в том, что Eurocopter использует в качестве хвостового ротора фенестрон, а MD Explorer — NOTAR. Оба вертолёта вышли на рынок примерно в середине 90ых годов, и вообще это очень хорошие вертолёты.

Одна беда — медленновато: у обоих крейсерская скорость в районе 250 км/ч.

А ведь за те годы, что прошли с разработки этих вертолётов, научились новому. Вот-вот в серию пойдут военные американские вертолёты Sikorsky S-97 и Sikorsky–Boeing SB-1 с крейсерскими скоростями 410 и 460 км/ч соответственно, демонстратор Eurocopter X³ ещё шесть лет назад показал скорость 472 километра в час, когда же уже выйдет вертолёт скорой помощи с крейсерской скоростью больше 400 км/ч? Eurocopter, точнее, Airbus Helicopters, как они сейчас называются, уже много лет работают над таким проектом — Airbus Racer. Вроде как в 2020-ом первый полёт, очень ждём.

В Германии вертолёты скорой помощи (в основном, DLR и ADAC) базируются в 73 равномерно распределённых по стране точках: https://www.rth.info/stationen.db/stationen.map.php, в до любой точки, где случилась авария, вертолёт долетает не более чем за 15 минут (время полёта, без учёта взлёта, посадки и поиска площадки для посадки). Поднятие крейсерской скорости с 250 до 400 снизит это время до 9 минут.
ДР Цертуса 2011

Общий наркоз у маленьких детей

Плановой операции на зубах мы ждали несколько месяцев, т.к. для операции должны очень совпасть звёзды: наш детский стоматолог раз в месяц имеет операционный день в клинике, и в этот день там должны быть одновременно доступно два детских анестезиолога, т.к. для операций детям до 2 лет и 15 кг веса положено чтобы в операционной одновременно был анестезиолог-анестезиолог, и анестезиолог-реаниматолог. Типа при таком весе, если анестезиологу придётся заниматься реанимационными мероприятиями, то он может неуспеть уследить за собственно анестезией.

Букет препаратов, которые берут чтобы сделать маленькому ребёнку общий наркоз, нынче обширен.

— Дома, за час с небольшим до операции кожу в локтевом сгибе мажут мазью с местным обезболивающим лидокаин и несколькими кожеразмягчающими средствами, сверху заклеивают таким специальным очень тонким тянущимся прозрачным пластырем. Кстати, вот с момента “за час до операции” начинается запрет на то, чтобы что либо пить. Если очень хочется, можно давать чистую воду по чайной ложке (“так она не остаётся в желудке, а практически сразу всасывается, но жажду снимает”). Есть нельзя с вечера, можно только пить прозрачные жидкости без газа и без осадка (смузи, соки с мякотью и любые молочные продукты нельзя). Есть исключение для материнского молока — его можно употреблять ночью, но нужно прекратить не менее чем за два часа до операции, как раз за два часа оно заведомо переваривается (с 90% вероятностью оно переваривается за 50-80 минут, запас делается ради тех 5% случаев, когда дольше).

— В больничке пластырь снимают и ставят туда тоненький венозный катетер. Нынче они без иглы, то есть игла используется для введения, но потом сразу снимается, и остаётся только такая “резиновая” трубочка в вену, так что всё руку можно свободно гнуть и ничего не болит. Туда сразу колят очень маленькую дозу мидазалама — короткодействующего успокаивающего/седативного. Во-первых, чтоб ребёнку было менее страшно и ребёнок меньше брыкался, во-вторых из-за занятного побочного эффекта — ретроградной амнезии. Т.е. того, что было за несколько минут до укола и несколько минут после ребёнок на следующий день чаще всего не помнит.

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

— Ребёнка укладывают на операционный стол и дают маску, а потом и ставят в катетер маленькую стартовую инъекцию пропофола, после чего ребёнок засыпает. С момента захода в дверь операционной, до момента, когда она заснула прошло меньше 30 секунд, я серьёзно. Потом два ассистента одновременно подключают кардиомонитор и ЭЭГ-монитор на голову, через 5 секунд оба монитора работают, и к катетеру подключают помпу, которая дают туда пропофол, суфентанил и ремифентанил, анестезиолог смотрит в ЭЭГ-монитор и выставляет дозировки. Ещё в катетер поставили ампулу, кажется, миорелаксанта, но я сейчас не могу вспомнить название, кажется на “ir” что-то. Ну а потом родителю предлагают выйти. И, как мы выяснили позже, в этот момент вставляют трубку для вентиляции лёгких.

Назад в комнату для просыпающихся больных нас позвали через 50 минут, девочка проснулась ещё через 15-20 минут, в не очень хорошем настроении. Медсестра сразу отключила капельницу с физраствором и сказала что можно взять на ручки. А потом пыталась георически удержать на девочке кардиомонитор и мониторилку насыщения крови кислородом, в результате чего девочка забрыкалась, взволновалась и мониторы немедленно запищали, но мимо как раз пробегал, готовящий следующего пациента, анестезиолог и сказал что можно это всё снять. Сказал, что через час можно снимать венозный катетер и ехать домой, дома пить можно сразу, а есть если она сможет нормально пить.

Ещё минутки через три, оглядевшись, девочка очень захотела грудь. Мы все вместе (я, Аня и медсёстры) пытались её всячески отвлечь от этой идеи, пока снова мимо не пробежал анестезиолог и не сказал прямо на бегу (к вящему удивлению медсестёр), что ”вот это как раз можно, пусть”. Через некоторое время он объяснил, что ему по показаниям ЭЭГ-монитора как-то понятно, когда наркоз прошёл хорошо, и тошноты не ожидается.
ДР Цертуса 2011

Айлин, речь

У Айлин за последний месяц большой прогресс. Месяц назад её словарный запас фактически исчерпывался словами «мам!», «пап!», «ам!» (есть), «бау» (животное), «бу» (так она назвала любимую куклу), «мау» (кошка) и «дададаааа!» (увидела детскую площадку и хочет туда). Недель пять назад появились «нянь!» (Настя), «кука» (кукла) и «би» (машина). В первые дни июля добавилось «гага» (гуси-гуси га-га-га, означает водную птицу). Потом разом «да» (сопровождается утвердительным киванием) и «ниии» (сопровождается отрицательным качанием головой) и «тяй» (чай), а потом уже ни дня без нового слова: «Фýфу» это сушка, «афьа» — вафля, «папий» — памперс, «попий» — попа, абака — облака (белогривые лошабки), «баба», «пиком» (пешком, значит хочет слезть и идти сама, либо чтобы её подержали за руку, когда она идёт по бордюру) и, самое главное «пьик!» (прыг!), это говорится когда она скачет по полу, когда прыгает с разных объектов в низ или когда хочет чтобы её подстраховали/взяли за руку перед прыжком.

Прыг появился в вторник, а сегодня (в среду) сегодня случился прорыв — она сказала «не пиком» (то есть «не пешком»), когда я пытался спустить её с рук. Появилась грамматика!

Настя тем временем замечательно рифмует свои присказки, а нерифмованное запоминает по смыслу, а не дословно: сегодня вот застал её за следующими рассуждениями вслух: “каждый — к — красный, охотник — а, нет о — оранжевый, желает — желтый, знать — зелёный, где — г — голубой, находится — нн — эээ, где находится дикая лесная курица на ф — фиолетовый”.
ДР Цертуса 2011

Карри-Говард для FOL

Как все тут знают, по соответствию Карри-Говарда интуиционистской логике высказываний (логике нулевого порядка) соотведствует просто-типизированное лямбда-исчисление с произведениями STLC.

Утверждениям в логике соответствуют типы в STLC, доказательствам утверждений — термы соответствующих типов. У STLC с произведениями есть прекрасная категорная семантика — декартово-замкнутые категории.

С логикой первого порядка всё чуть сложнее. Там кроме утверждений появляются предикаты и отношения — утверждения, зависимые от одной или нескольких переменных, которые тоже имеют свои типы, в зависимости от подлежащей теории. Например, если мы в рамках логики первого порядка описываем линейные пространства, у нас будут типы K скаляров и V векторов.

То есть тут у нас есть такие сущности:
– Типы элементов (например, скаляров и векторов), они образуют категорию с конечными (декартовыми) произведениями. Среди них выделенный тип “1” — нейтральный элемент произведений. Назовём эту категорию T, и в ней особо выделим проекции X ↠ Y (морфизмы, которые выделяют из произведения A × B ×···× D подпроизведение, скажем, B × C, и, опционально, меняют порядок аргументов).
– Типы предикатов P(x : T), где T какой-то тип элементов. Отношения суть предикаты на произведении нескольких элементарных типов отношений, например Id(p : T × T), а обыкновенные высказывания суть предикаты на 1. Если мы хотим чтобы у нас была логика первого порядка с равенством, то как раз постулируется что для каждого типа элементов автоматически есть предикат Id(x : T, y : T).
– Мы хотим, чтобы совокупность предикатов над одним и тем же типом была реализацией логики высказываний (т.е. категория предикатов над T была декартово замкнутой)
– Мы хотим, чтобы каждая проекция в категории элементов X ↠ Y порождала контравариантный функтор между категориями предикатов над Y и предиктов над X (это значит мы можем менять местами переменные у предикатов и добавлять переменные, которые никак не используются), сохраняющий структуру декартовой замкнутости.
— Далее мы хотим, чтобы у нас были кванторы — функторы сопряженные с вложениями слева и справа, соответственно предикаты P(x : X, y : Y) в предикаты (∀x,P)(y : Y) и (∃y,P)(y : Y). То есть мы уменьшаем количество переменных (можем уменьшить и до нуля, тогда получатся предикаты над единицей, то есть высказывания), замыкая убираемые переменные квантором всеобщности или существования.

Вот собственно и вся категорная семантика FOL, называются такие штуковины гипердоктринами (или, соответственно гипердоктринами с равенством, если требуются id-типы). Привожу определение по Pierre Clairambault, “From Categories with Families to Locally Cartesian Closed Categories”:

Screen Shot 2019-07-30 at 15.03.07

А вообще это классика, R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für math. Logik und Grundlagen der Math., Band 29, 505-542 (1983).
ДР Цертуса 2011

Laundry robots

Фирма Laundroid, которая обещала нам all-in-one-робота, который сразу делает с постиранным бельём всё, что нужно, увы, ожидаемо загнулась.

Самое нужно устройство после стирки — это такая штука, чтобы туда сунуть корзину белья из стиралки, а на выходе все рубашки-футболки-платья развешены на плечики, а всё остальное — и штаны-юбки-полотенца, и носки, и тряпочки, развешено на прямые вешалки с прищепками, причём парные вещи (особенно носки) повешены рядом.

Вот это нужно в первую очередь, а дальше оно уже удачно дополняется устройствами, которые сейчас в активной разработке и вот-вот выйдут на рынок, если всё сложется экономически:

– Эффи (https://helloeffie.com), такой шкафчик, в который вешаешь на плечиках набор рубашек, футболок, платьев, юбок и всего такого, и получаешь через некоторое время назад отглаженное паром и высушенное.

– FoldiMate, который складывает бельё в аккуратные стопочки. Им можно складывать либо то, что только что выглажено в Эффи, и должно не висеть, а лежать (футболки, например), либо то, что в стиральной машине сразу высушено до состояния “можно сразу складывать и в шкаф”. Ежели в него бы ещё можно было сразу пихать два носка, и он их аккуратно складывал друг-в-друга, вообще бы цены ему не было.

Вся эта машинерия не покрывает одного важного случая — постельного белья. Для постельного белья нужен особо крупный крупный FoldiMate, совмещённый с гладильным катком — подаёшь туда пододеяльники, пледы, простыни, наволочки, а он их складывает в ровные стопочки, по дороге проглаживая ровно. Или складывет без проглаживания — режим, нужный для одеял, которые как раз можно в стиральной машине высушивать досуха, и, возможно, трикотажных простыней.
ДР Цертуса 2011

Робопылесосы

Оказывается, iRobot выпустили новый офигенский робопылесос Roomba S9+, традиционно с пылесосной станцией, успешно компенсирующей малый объем пылесборника. Ругают его пока за сыроватый софт, но это невпервой, за годик они всё починят и апдейты пришлют. А вот само устройство меня впечатлило (ценой, правда, тоже впечатлило — $1500). Они сдались и наконец отказались от круглой формы робопылесоса и перешли в новой модели S9+ к логичной D-образной форме, а ещё радикально увеличили силу всасывания —теперь 2.6 кПа, и мощность всасывания — теперь 22 Вт (это не потребляемая, а производимая мощность). По обоим показателям это на порядок с лишним ниже, чем у любого нормального большого пылесоса, но для аккумуляторных пылесосов это невиданный прорыв. А вот шумовые показатели в районе 65-68 дБ. Эх, вот кабы 55-58... Мечты-мечты.

Удивительным образом, для меня препятствием к использованию робопылесоса является шум — пылесосит эта штука очень долго, ночью из-за шума не запустишь, днём под ногами мешается и бесит шумом, неприятных, к тому же частот. У нас Roomba 760, формально он даёт уровень шума в районе 65 дБ — казалось бы немного, но звук уж больно противный. У более новых моделей звук существенно менее противный, кстати, так что может быть те 65-68 дБ и не очень плохи.

Можно ли сделать мощный, но тихий пылесос?
Если его не нужно запитывать от батарейки и упихивать в очень маленький корпус, то да! Collapse )
ДР Цертуса 2011

Подземные парковки

(По следам переписки в комментариях с daedmen.)

Вы заезжаете на обычное такое наземное парковочное место — 2.30м в ширину, 6м в длину, может вдоль дороги параллельно, может перпендикулярно с отдельным въездом, только вместо того что границы нарисованы на земле белой линией, границы физические — под автомобилем не асфальт, а гидроизолированная стальная решётка*. Перед вашим капотом невысокий заборчик, 1.15м в высоту, в него вмонтирован аппарат оплаты парковки. Выходите, прикладываете платёжную карту, нажимаете на столбике рядом кнопочку что “в машине никого не осталось, в особенности не осталось ни детей, ни животных”, и тут с оставшихся трёх сторон парковки из земли медленно поднимаются ещё три заборчика, тоже 1.15м в высоту, причем с длинных сторон — непременно из стальной решетки. Потом ваша машина вместе со стальной решёткой медленно опускается, а длинные стороны заборчика складываются внутрь, образуя новую стальную решётку из двух половинок. Что характерно, общей шириной в те же 2.30м. Заборчик сзади просто опускается. Всё, парковка готова принимать следующего посетителя. Если у вас электромобиль или гибрид, он ещё и подзарядится там внизу.

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

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

Если мы делаем каршеринг микромашинок вроде Toyota i-Road, то можно сделать то же самое, с парковочными местами в два раза уже и в два раза короче (тогда платформы, кстати, не нужно делать двухстворчатыми), и благодаря тому что машинки в парковке будут взаимозаменяемыми, на выездном месте всегда будет стоять готовая к выезду машина, а иметь дополнительное место внизу для пересортировывания машин будет не нужно. Таким образом парковки с наземным футпринтом менее чем в одно парковочное место обычной машины, и глубиной всего в 6 метров хватит на целых десять машин. А для 6 машин хватит глубины всего в 3 метра.Collapse )