?

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)

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).

(3 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 )

(3 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 )

(9 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)

Sunday, June 16th, 2019
5:51 pm - HoTT
Первая половина 2019-го оказалась урожайна на результаты касательно семантики Гомотопической Теории Типов.Read more...Collapse )

(8 comments | comment on this)

Thursday, June 13th, 2019
2:05 am - Радио
Уж довольно много лет назад, плата за общественное радио и телевидение в Германии перестала взыматься по факту наличия радио или телевизора, а стала просто ещё одним налогом. Не платой за потребление контента а налогом на поддержание платформ, где проходят предвыборные дебаты и другие подобные общественно не просто полезные, но необходимые вещи. Пока я хоть иногда смотрел телевизор, меня постоянно бесило, что деньги платятся, а контент (новости и всякие передачи на общественные темы) очень среднего качества. Ну да, дебаты бывают хорошие, да и вообще попадаются хорошие и качественно сделанные передачи, но в целом уровень экспертизы очень так себе. Как всегда, эффект Гелл-манна — низкий уровень экспертизы особенно замечаешь, когда вякнут какую-нибудь несусветную дичь и несуразицу про Россию, Украину или Белоруссию, или про какие-нибудь научные новости и ядерную энергетику, потому что в этих вопросах можешь отличить откровенные ляпы. Больше низкого уровня экспертизы бесят только передёргивания — общественное телевидение всё-таки должно стараться не быть тенденциозным, с чем оно не справляется ни в отношении внутренней, ни в отношении международной повестки.

Так вот, с тех пор как я езжу на машине, я иногда слушаю радио. И вот надо сказать, что радио на удивление гораздо лучше телевизора. Там даже про Трампа могут говорить без снобизма, про Израиль без передёргиваний и про Брексит спокойно. А давеча я вообще удивился. Щёлкнул на DLF, а там вдруг Окуджава поёт. Стал дальше слушать, а там интересная передача про советских военнопленных. И прямо кусочки интервью на русском языке дают, и перевод потом (кусочек на русском коротенький, а перевод обычно подлиннее) — так я прямо удивился, во-первых кусочек на русском прерывают не на полуслове, а аккуратно в конце мысли, во-вторых переводы хорошие — не просто точные, но и стилистически адекватные. А потом ещё подбор песен удивил — это не просто хороший какой-нибудь Окуджава, или отрывок из «Тёмная ночь», а _подходящий_ Окуджава, и _подходящий_ по контексту отрывок, кроме того там были и малоизвестные фронтовые песни, и песни советских военнопленных на немецком языке (о том, что такие есть я вообще не подозревал). В общем, я, внезапно, в восхищении.

Ещё я пару раз попадал вечерами пятницы то на передачу под названием «Шалом» на DLF, то на «Шаббат шалом» на NDR Info, и то что-нибудь интересное светскому человеку по части иудаики рассказывают, то про историю евреев Германии интересное что-нибудь, то про Израиль без охаивания. Не то чтобы я там тоже прям пребывал в восхищении — нет ну передачи как передачи, но на фоне телевизора это действительно другой уровень.

(6 comments | comment on this)

Thursday, June 6th, 2019
3:28 am - Математическое
Я только что обнаружил, что Ален Конн выпустил две новые публикации про топосы и “поле” характеристики 1 — «Spec Z and the Gromov norm» и «Un topo sur les topos». Первую я только начал просматривать, а
вторая оказалась по-французски (так что я там очень не всё понимаю), но не техническая, а обзорная, очень клёвая. http://www.alainconnes.org/en/downloads.php

(comment on this)

> previous 20 entries
> top of page
LiveJournal.com