?

Log in

No account? Create an account
Alexander Kuklev's Journal

> recent entries
> calendar
> friends

> profile
> previous 20 entries

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

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

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

(5 comments | comment on this)

Sunday, September 29th, 2019
6:21 pm - 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/

(7 comments | comment on this)

3:49 pm - Вертолётное
На слово «вертолёт» я автоматически представляю себе сейчас 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 минут.

(6 comments | comment on this)

Saturday, September 21st, 2019
3:58 pm - Общий наркоз у маленьких детей
Плановой операции на зубах мы ждали несколько месяцев, т.к. для операции должны очень совпасть звёзды: наш детский стоматолог раз в месяц имеет операционный день в клинике, и в этот день там должны быть одновременно доступно два детских анестезиолога, т.к. для операций детям до 2 лет и 15 кг веса положено чтобы в операционной одновременно был анестезиолог-анестезиолог, и анестезиолог-реаниматолог. Типа при таком весе, если анестезиологу придётся заниматься реанимационными мероприятиями, то он может неуспеть уследить за собственно анестезией.

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

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

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

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

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

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

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

(3 comments | comment on this)

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

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

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

(2 comments | comment on this)

Tuesday, July 30th, 2019
3:05 pm - Карри-Говард для 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).

(9 comments | comment on this)

Tuesday, July 23rd, 2019
3:51 am - Laundry robots
Фирма Laundroid, которая обещала нам all-in-one-робота, который сразу делает с постиранным бельём всё, что нужно, увы, ожидаемо загнулась.

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

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

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

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

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

(10 comments | comment on this)

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

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

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

(5 comments | comment on this)

Monday, July 22nd, 2019
10:10 pm - Подземные парковки
(По следам переписки в комментариях с daedmen.)

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

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

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

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

(5 comments | comment on this)

8:17 pm - Кухонные приборы мечты
Может кто помнит, я несколько раз, начиная с 2003 года писал про то, что вот бы были посудомоечные машины, у которы ящики не просто выдвигаются, но и поднимаются, чтобы их загружать на уровне стола?

Оказывается ещё три года назад появились посудомоечные машины AEG Comfortlift, в которых нижний ящик именно что не выдвигается, а выдвигается и поднимается: https://youtu.be/Kazo9G2SSSg. Но вот к сожалению это всё не до уровня высоты стола, а ниже. Надо и нижний, и верхний ящик при выдвигании поднимались, и вот именно до высоты стола. А для пожилых людей желательно, чтобы выдвигание и задвигание можно было сделать нажатием кнопочки. Read more...Collapse )

(10 comments | comment on this)

Sunday, July 21st, 2019
12:22 am - К юбилею высадки на луну
SpaceX вообще молодцы, я с диким интересом слежу за разработкой двигателя Raptor и ракеты BFR.

SpaceX удачно завершают первую стадии стратегического развития — они сделали двухступенчатые ракеты космического назначения (Falcon-9 и Falcon Heavy) на нетоксичном доступном топливе с возвращаемыми и подлежащими многократному использованию первыми ступенями. Добились стабильной посадки этих ступеней и довольно твёрдо идут к тому, чтобы посаженную ступень можно было повторно использовать уже через несколько суток — сейчас на то, чтобы привести использованный бустер в рабочее состояние уходит чуть больше двух месяцев. Попутно они развили несложный (по меркам современных ракетных двигателей) и не новый (базирующийся на недоделаном NASA'вском двигателе Fastrac) до конфетки в своём классе, имеющей рекордную тяговооруженность среди всех ракетных двигателей для систем запуска орбитального класса.

Именно чтобы добиться этих результатов как можно скорее, SpaceX изначально шли на много компромиссов — Falcon'ы имеют малый диаметр, Merlin базируется на изначально устаревшем подходе к двигателестроению и т.д. На второй стадии они делают ракету толще и двигатель, который базируется на самом совершенном из известных подходов к двигателестроению. При этом на ещё более нетоксичном и дешёвом топливе — метане. (Хотя при этом избегают пока экспериментов с переходом от классических к клиновоздушным двигателям в качестве стартово-посадочных, хотя это теоретически даёт выигрыш в топливной экономии и в тяговооруженности за счёт экономии на подвесе. Но нельзя же экспериментировать со всем одновременно.)

Надо помнить, что первоочередная задача в том, чтобы снизить цену вывода грузов на орбиту. И самый радикальный способ снизить эту цену сейчас — сделать вторую ступень тоже возвращаемой. И переход к двигателю Raptor и ракете BFR на самом деле ради этого. Уже потом, когда это, ттт, заработает, можно будет думать о дальнейшем повышении тяговооруженности и топливной экономии двигателей. Ну, а когда выжимать топливную экономию и снижать массу двигателя и судна будет некуда, ещё можно перейти к старту с экватора, тем самым повысив количество полезной массы, которую ракета может вывести на орбиту, на 20-50% (в зависимости от характера миссии) чисто благодаря точке старта.

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

А вообще, и Tesla и SpaceX можно рассматривать как подготовку площадки, чтобы когда наконец возникнут термоядерные электростанции и термоядерные ракетные двигатели, всё сразу было готово к тому, чтобы начать ими пользоваться всласть. (Использовать ТЯРД нужно только в открытом космосе, для взлёта и посадки обычные двигатели подходят гораздо лучше.) А этим уже занимается совсем не Elon Musk, а TAE Technologies и НИИ ядерной физики имени Будкера. Вот если у них всё получется, то будет вам и декарбонизация, и энергии завались, и эффективный транспорт в пределах солнечной системы, и перспективы межзвёздных полётов к землеподобным планетам.

(15 comments | comment on this)

Saturday, July 20th, 2019
11:18 pm - Taxi for one
(Ежегодный пост)

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

Идеальным такси для одного пассажира является беспилотный микроэлектромобиль с закрытым, шумоизолированным, кондиционируемым салоном, куда влезает один пассажир, один большущий чемодан и один элемент ручной клади (чемоданчик или городской рюкзак). Микроэлектромобиль должен иметь длину в пределах 2300мм (чтобы парковаться поперёк) и ширину в пределах 900мм — тогда допустимо использовать одну (например, автобусную) вдвоём, а также совершать на ней обгон, когда другая машинка остановилась для посадки/высадки пассажира. Ну и ехать такая штука должна уметь хотя бы 80км/ч. Не считая отсутствия беспилотности, к этому близки Renault Twizy Cargo 80 и Toyota i-Road.

(18 comments | comment on this)

Monday, July 1st, 2019
4:03 pm - О понятиях множества и класса
“Eine Menge ist eine Zusammenfassung bestimmter wohlunterschiedener Objekte unserer Anschauung
oder unseres Denkens — welche die Elemente der Menge genannt werden — zu einem Ganzen.”
— Georg Cantor, «Grundlagen einer allgemeinen Mannigfaltigkeitslehre»

(“Множество это собрание воедино определённых различимых объектов нашего представления или нашего мышления, называемых элементами множества.”)

§ О слове множество.

Когда говоришь про теории множеств, многие думают что там слово “множество” используется в обыденном смысле, как “множество всех молекул, из которых состоит стул”, но на самом деле речь совершенно не об этом.

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

Однако теория множеств, вошедшая в математику на столетие в качестве ассемблера, на который транслируют определения, построения и доказательства, это вполне конкретная теория множеств ZF(C) и её близкородственные вариации, называемые membership-based pure set theories. И они вообще говоря совершенно не о том, чтобы описать язык и поведение совокупностей объектов. Это о расширении логики первого порядка принципом рефлексии.Read more...Collapse )

(46 comments | comment on this)

Thursday, June 27th, 2019
4:27 pm - Ещё одно введение в теории типов
В математике понятие “теория типов” развивается, и ещё непонятно в какой общности нужно будет давать определение. В контексте информатики теориями типов называют обобщения λ — просто типизированного лямбда-исчисления.

В сущности, теория типов — набор правил, которые позволяют конструировать выражения из подвыражений, в ситуации когда не любые выражений комбинируются, а только правильно стыкующиеся. Чтобы выразить “стыкуемость” вводится понятие типов (и набор правил, как эти типы записывать). Если терм x имеет тип T, пишут x : T. В λ всегда имеется какой-то набор базовых типов (например, тип Nat, содержащий все натуральные числа), и типы, получаемые из базовых X и Y путём применения оператора X -> Y.

После того как описано, какие бывают типы, можно записывать те самые правила конструирования выражений. Например:
  f : X -> Y    x : X
————————————––––––––––—
         f(x)


Для того, чтобы получившиеся выражения тоже можно было стыковать с чем-то дальше, в теорию типов добавляются дополнительные виды правил, как минимум требуется указать тип для любого сконструированного выражения:
  f : X -> Y    x : X
————————————––––––––––—
       f(x) : Y


Но в более сложных системах может хотеться, чтобы можно было применить f : X -> Y к такому x : X', что X и X' не совпадают “побуквенно”, но одно и то же по-существу (ну либо X' является подтипом X). Тогда нам нужны ещё правила конверсии типов, которые говорят в каких случаях X' ≼ X. Давайте предположим, что мы добавили в базовые типы нашего λ кроме самого Nat ещё типы Fin(n) дла каждого n : Nat, содержащие натуральные числа меньше n. То есть, у нас появились зависимые типы (такие операторы, которые превращают выражение какого-то фиксированного типа в тип, Fin(n) — как раз пример такого). Теперь нам хочется, чтобы туда, где требуется Fin(n) можно было подставить Fin(m), если n и m равны. То есть нам уже нужны правила равенства и для выражений. И правило, что если n = m, то Fin(n) ≼ Fin(m).

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

λ(Nat) и λ(Nat, Fin) можно сформулировать обоими способами. Можно сказать, что тип Nat состоит из лямбда-выражений
(\f ↦ (\x ↦ x))
(\f ↦ (\x ↦ f(x)))
(\f ↦ (\x ↦ f(f(x))))
...
А типы Fin(n) из нижних подмножеств этих выражений. Типы X -> Y, понятное, дело, тоже из лямбда-выражений. Тогда у нас, получается, любые типы состоят из лямбда-выражений, и для выражения любой “программы” не требуется ничего, кроме абстракции и применения. Между прочим, эта система типов позволяет записать в точности все рекурсивные функции, тотальность которых доказывается в арифметике первого порядка PA, и наоборот любому утверждению на языке арифметике первого порядка можно сопоставить функцию, определимую в этой теории типов, тотальность которой эквивалентна верности исходного утверждения. Можно также расширить λ(Nat, Fin) до λ×→(Nat, Fin) типом пар X × Y, и сказать что пара (x, y) это на самом деле лямбда-выражение (\f ↦ f(x)(y)). Всё ещё все типы населены только лямда-выражениями. Кстати, добавления типа пар добавляет λ только выразительности, но не силы — определимые там и там рекурсивные функции совпадают.

Такой подход называется PTS — Pure Type Systems. Активно разрабатываемая сейчас система Cedille показывается, что в рамках PTS можно сделать очень мощные системы типов, в частности включающие MLTT c Π, Σ и W-типами (более того, индексированными индуктивными типами), а ещё вероятно интенсиональными Id-типами (без UIP), но без вселенных и large elimination.

Можно, наоборот, сказать, что в λ(Nat) тип Nat состоит из особенных атомов Zero, Succ(Zero), Succ(Succ(Zero)) и т.д., и для них есть оператор паттерн-матчинга, а лямбда-выражения между двумя типами строятся индуктивно при помощи собственно конструкторов лямбда-выражений и операторов паттерн-матчинга. На этом пути, добавляя другие базовые типы и конструкторы типов мы тоже можем обобщать теорию без видимых пределов.

(2 comments | comment on this)

Wednesday, June 26th, 2019
9:26 pm - Несправедливо малозамеченная статья
Год с небольшим назад вышла статейка “Leibniz Equality is Isomorphic to Martin-Löf Identity”.

Она люто офигенная. Цитатка: Leibniz equality can be viewed as the Church encoding of Martin-Löf identity.

Вопрос: можем ли мы в Cedille вывести закон индукции для Leibniz equality, т.е. J rule?

А если можем, то мы, наверное, можем определить и тип Prop := Σ(T : *) Π(a b : T) a = b и дальше всевозможные импредикативные представления quotient inductive types следуя https://arxiv.org/abs/1802.02820.

Можно ли будет добавить туда “large eliminations” в Prop и в частности доказать 0 ≠ 1 естественным путём, а не как сейчас?

(comment on this)

6:02 pm - Разница между параметром и аргументом
Зависимые теории типов с иерархиями вселенных не позволяют говорить о вещах типа “категория всех групп”, они лишь позволяют говорить о “категориях всех U-малых групп”, проблема хорошо известная людям, занимающимся теорией категорий в теории множеств Тарского-Гротендика (ZFC + всякое множество содержится в какой-то вселенной Гротендика). Как в случае теории множеств, так и в случае теории типов есть сильные результаты, что утверждения для U-малых групп на самом деле переносятся на любой U', но чисто онтологически утверждения выглядят менее красиво, чем могли бы.

Для теорий множеств известен выход из этой неприятной ситуации. Для всякой теории множеств можно построить расширение, в котором можно говорить о классах (для ZFC оно называется NBG), тогда становится можно говорить о “категории всех групп”, но с ней ничего толком нельзя сделать, т.к. она класс, а не множество. Ну и можно построить теорию множеств вроде ZMC/S, добавив в ZFC принцип рефлексии, что есть такое множество U, являющееся вселенной Гротендика (т.е. моделью класса всех множеств), что любое утверждение 𝜑 равносильно утверждению 𝜑𝑈 (т.е. 𝜑 относительно U, синтаксической модификации утверждения 𝜑, где все классы заменили на соответствующие подмножества 𝑈).

Разумеется, хочется сделать такой же финт ушами и для теорий типов.

* * *


Вот рассмотрим f : ∀(T : *), T -> T. Это параметрическое семейство функций. Будучи специализированно для конкретного типа T, это функция T -> T.

В System F и её расширениях мы можем доказать, что всякое определимое семейство этого типа равно семейству idT = (\x : T) ↦ x.

В MLTT нет различия между параметром и аргументом. Путём введения типа Type («вселенной»), зависимость от параметра класса * представляется как зависимость от аргумента типа Type. То есть, idT типируется через (T : Type) -> T -> T. Благодаря отсутствию элиминаторов у вселенных, зависимость от аргумента типа Type остаётся в данном конкретном случае параметрической (“generic”, в частности мы не можем получить в указанном случае ничего кроме функции id, потому что не можем split by cases аргумент T — его тип Type не поддерживает spliting by cases и никакой другой интроспекции).

Проблема в том, что кроме интроспекции есть ещё один способ непараметрически использовать аргумент кроме интроспекции: его можно вернуть.

Терм (\T : Type) ↦ T имеет тип (T : Type) -> Type, и тут зависимость от T непараметрическая.

С точки зрения экспрессивности таким образом целесообразно иметь раздельно зависимые типы и оператор ∀. Тогда в подлежащей теории нужно уметь всё же говорить не только о типах, но и о классах (вообще их обычно называют kinds, но сейчас я предпочитаю такое название). Единственное использование классов именно в том, что когда мы пишем ∀(x : K) справа стоит не тип а класс. Блестящим такой теории является Cedille, причём там экспрессивность тамошних классов (замкнутость относительно зависимых сумм и произведений) как раз оправдывает использование слова “класс” — мы можем говорить о классе * всех типов, о классе всех групп и т.д.

Но при этом в Cedille нет large eliminations, а чтобы они там появились очень хочется пойти по пути ZMC/S и добавить просто какой-то сильнейший принцип рефлексии, который автоматически сгенерирует нам вселенные, с которыми удобно работать.

Вот например можно попробовать сказать, что у нас есть такой тип 𝑈 : *, и такая специальная метаоперация, которая превращает любое определение класса 𝜑 : 𝜅 в тип 𝜑𝑈 : *, путём замены в определении всех нужных * на 𝑈. Кстати, *𝑈 = 𝑈. А дальше какая-то схема правил, говорящая, что 𝜑𝑈 должно быть “малой” внутренней моделью 𝜑. Что-то типа метаоперации кодирования любого типового выражений класса 𝜑 в элементы 𝜑𝑈, и оператора декодирования в обратную сторону, но только это надо сделать как-то так аккуратно, чтобы не возникло противоречий. В частности, видимо, нужно чтобы композиция кодирования и декодирования давала не равенство, а изоморфизм. А невозможность прямого переноса терма вдоль изоморфизма предотвращала парадокс Расселла.
Очень мило, кстати, получается, что тут иерархия вселенных будет в другую сторону. * настоящая вселенная, *𝑈 = 𝑈 отражающая её “малая”, 𝑈𝑈 ещё более малая, и т.д.

(5 comments | comment on this)

Tuesday, June 25th, 2019
1:29 am - А что делать с супергидридом иттрия YH10?
Металлический водород, если он существует (на днях этому нашлось новое подтверждение: https://arxiv.org/pdf/1906.05634.pdf), вероятнее всего является классическим сверхпроводником с необыкновенно высокой критической температурой. У всех известных классических (т.е. БКШ-)сверхпроводников, не содержащих водород, это температуры в пределах 40 градусов от абсолютного нуля, а у металлического водорода, вероятно, между 40 и 80 °C. И вот это удивительное свойство металлического водорода проявляется под очень большими давлениями у соединений водорода, особенно супергидридов. Группа Еремеца занимается металлическим водородом, и они сперва предсказали, а потом, лет пять назад, экспериментально доказали, что при чудовищных давлениях в полтора миллиона атмосфер сероводород H2S является классическим сверхпроводником с критической температурой аж −70 °C, потом предсказали и в мае этого года (DOI: 10.1038/s41586-019-1201-8) окончательно доказали экспериментально, что у декагидрида лантана LaH10 при таком же чудовищном давлении в 200 ГПа критическая температура аж −23 °C. Ну и вот сейчас теоретически предсказали, что у декагидрида иттрия YH10 при ещё более чудовищном давлении в 2-3 миллиона атмосфер критическая температура будет аж 36 °C.

Но может ли это как-то быть использовано инженерно, как-то помочь разработке комнатных сверхпроводников, работающих при обычном давлении?

(5 comments | comment on this)

Sunday, June 23rd, 2019
11:47 pm - 1 TB
Оказывается, с мая сего года есть наконец microSD-карты на 1TB. А Everspin буквально на днях начала производство гигабитных DDR4 чипов STT MRAM (энергонезависимой и очень быстрой памяти).

(comment on this)

1:57 pm - Транспортное
Доехать на машине из Подберлинья в Подмосковье менее чем за 24 часа двумя водителями с двумя детьми — check. Потребление, кстати, на каждого пассажира 1.8 литра на 100км, раза в полтора-два ниже, чем если самолётом лететь.

(1 comment | comment on this)

Thursday, June 20th, 2019
3:40 pm - Из комментов, про HoTT
Из комментов, цитата 1: «В смысле "когда RedPRL станет столь же удобен как ХХХ, то можно считать, что [..] применима в учебном процессе" - что здесь будет ХХХ?»

Такого XXX сейчас нет целиком, но можно собрать по частям. Read more...Collapse )

(4 comments | comment on this)

> previous 20 entries
> top of page
LiveJournal.com