|
|
Saturday, January 17th, 2015
| |
2:17 pm
|
Настоящим объявляю, что все мои персональные данные, тексты, фотографии, рисунки, переписка и т.п. являются объектами моего авторского права (согласно Бернской Конвенции), и оповещаю «ЖЖ» (LiveJournal, Inc / SUP Media) о том, что разглашение, копирование, распространение моей личной информации в коммерческих целях равно как и любые другие противоправные действия по отношению к моему профилю в социальной сети строго запрещены.
Для коммерческого использования всех вышеупомянутых объектов авторского права в каждом конкретном случае необходимо мое письменное разрешение.
Гёттинген
17 января 2015 г.
Александр Куклев
|
|
(6 comments | comment on this)
|
| Thursday, June 5th, 2025
| |
11:37 pm
|
Что-то захотелось послушать «Снегопад» Виктора Берковского, «Снега выпадают и денно и нощно, стремятся на землю, дома огибая...» И вот я дома, в Омске на восьмом этаже, на окне узор изморози, за окном падает снег, а внутри тепло и защищённо. На контрасте настоящего хруского мороза снаружи и тепла внутри, дом особенно ощущается домом, а стены дома — каменными стенами, незыблимыми границами своего кусочка вселенной.
Из нашего окна в гостиной, там на Добровольского 1, открывался свободный вид на восток: перед домом в ту сторону было большое открытое пространство, за ним улица Орджоникидзе с непрерывным потоком снующих машин, за ней с дальней стороны двухэтажные домики красного кирпича постройки конца 19го века в чёрными коваными оградами на балкончиках, бог его знает что там было — какие-то магазинчики, ведомства, да и жил вроде кто-то. За ними ещё какие-то строения, потом на углу Тарской и улицы Рабиновича над этими постройками возвышалась стройная и скромная, белая-белая Тарская церковь с маленькими маковками куполов, она восхитительно смотрелась в снежные дни, и так же звучало колокольное многоголосье звонким, прозрачным и солнечным зимним утром. Слева от неё исторический архив на Третьяковской.
На улицах была жизнь, всё время что-то происходило, на улицах тогда было как-то больше людей чем сейчас — одни торопились, другие шли ровным целенаправленным шагом, третьи прогуливались. А дома было тепло и спокойно, иногда радостно-спокойно, иногда скучно-спокойно, но всегда живо. Машины на Орджоникидзе весело месили серебристый мокрый снег, ещё не превратившийся грязную слякоть, ведь это был совсем свежий снег. Когда я вижу граниторы, перемешивающие фруктовый снег (такие итальянские десертные машины с непрерывно крутящимся шнеком внутри прозрачного цилиндра), всегда вспоминаю, какой он на ощупь ногами и руками, этот мокрый снег, когда его много-много.
А вечером потихоньку темнело и начинали зажигаться огоньки — фонари, окна, фары машин, неоновая реклама. Нет, там не было “огней большого города”, это как раз были огни города маленького. Большие и разноцветные огни города случались если мы ехали куда-то через самый центр на машине. Вид с моста через Омку, ночной цветомузыкальный фонтан и трамплин музыкального театра, потом красивые, насыщенные огнями улицы. На Масленникова мы обычно сворачивали налево, и мамины родители, и мамина бабушка жили там. Но самый красивый вид открывался, если повернуть направо на Ленинградский мост. Там как раз островок посередине, и раздваиваясь перед ним Иртыш становится особенно широк, метров 700, так что с моста открывался вид на широченный ночной Иртыш и его правый берег с огоньками-огонькам-огоньками.
|
|
(8 comments | comment on this)
|
| Saturday, January 11th, 2025
| |
2:04 am - Зима как стихийное бедствие
|
А вчера в Гёттингене внезапно выпало приличное количество снега и было очень скользко, по какому поводу автобусное предприятие решило остановить работу всех автобусов, создав в городе полнейший транспортный коллапс и дичайшие пробки, каких я вообще ещё ни разу не встречал. Доехать до школы забрать Настю у меня заняло 50 минут против обычных 13, а потом потом поездка длиной в 20 минут заняла кажется два часа.
Я не понимаю, как мы дошли до жизни такой, почему автобусы не могут нормально ездить в гололёд (в Баварии и Австрии почему-то спокойно могут) и как можно допустить чтобы городское транспортное предприятие, монополист, просто лишило город на почти целый день общественного транспорта!
|
|
(11 comments | comment on this)
|
| |
1:58 am - Дворик
|
|
Оживлённый центр европейского города, невысокие дома разной степени старинности с идеально оштукатуренными фасадами, внутри магазины, кафе, банки, аптеки. Надо признать большей частью, довольно одинаковые внутри. Но за фасадами иногда бывают дворы — дворы, со стороны которых неумытые и зачастую ржавые “газельки” завозят во все эти магазины товары. Там разгрузочные рампы с ржавыми поручнями и щербатыми лестницами, кривые водосточные трубы, местами неровно зафанеренные окна, щербатый асфальт или неровная многовековая брусчатка, странные деревянные пристройки. Я люблю иногда заходить в такие задние дворики (прямо под знак «посторонним в»), они вдыхают в меня ощущение жизни.
|
|
(7 comments | comment on this)
|
| Saturday, April 13th, 2024
| |
3:16 am - Про принцип Маркова, Verse Calculus и их связь с линейной логикой
|
Принцип Маркова это невыводимое в интуиционистской логике предикатов утверждение, которое тем не менее выполняется в вычислительной/конструктивной интерпретации оной.
Пусть у нас есть
– P(n) разрешимый предикат на натуральных числах, т.е. ∀(n : ℕ) P(n) ∨ ¬P(n) и
– доказательство, что ¬∀(n : N) P(n), то есть что этот предикат выполянется не для всех n.
Тогда мы можем начать пробовать последовательно все натуральные числа одно за другим на то, выполняется ли
это для них P(n), и заведомо найдём в какой-то момент такое, для которого ¬P(n). То есть при наших вводных, выводимо конструктивное существование
∃∀(n : ℕ) ¬P(n)
С точки зрения функционального прораммирования, фильтруя натуральные числа на предмет того, чтобы для них выполнялось ¬P(n), мы получаем ленивую последовательность всех таких чисел, а принцип Маркова гарантирует нам, что она непуста. Если мы вместо натуральных чисел возьмём произвольное непустое перечислимое множество (т.е. такое множество T, что есть сюрьекция ℕ ↠ T, а чтобы включить пустые, нужно требовать сюрьекции ℕ ↠ 1 + T), то мы тоже можем получить такую гарантированно непустую ленивую последовательность всех таких чисел, вот только порядок в ней зависит от способа нумерации.
И вот verse calculus дают нам способ работать с такими possibly infinite choice sequences (мне нравится название junctions), при которой вычисление зависит от порядка нумерации, результат в правильном смысле инвариантен относительно этого порядка. Но verse calculus не типизирован, а предположим мы сделали для него (инспирированную аффинной логикой) типизацию, где есть монада ‽T, которая делает для из любого непустого перечислимого типа T делает тип непустых junctions его значений.
В обычных зависимо-типизированных языках у нас есть тип зависимых пар (x : X, y : Y(x)) также обозначаемый Σ(x : X) Y(x). Тут нам понадобится расширить это определение для случая, когда левая переменная многозначная — тогда правая переменная тоже должна быть многозначной, сцепленной с ней, и в сценарии, где x : ?X имеет конкретное значение t, будет иметь конкретное значение типа Y(x).
Такой тип мы будем обозначать ⅋(x : ?X) Y(x).
На этом языке принцим Маркова говорит нам, что для непустого перечислимого типа T и разрешимого утверждения P(x)
q : ¬∀(n : T) P(n)
––––––––––––––
e : ⅋(n : ?T) ¬P(n)
или
q : ¬∀(n : T) P(n)
–––––––––––––––
e : ?Σ(n : T) ¬P(x)
* * *
Как выясняется, мы можем отказаться от требований к типу T и предикату P (теперь не нужна ни перечислимость первого, ни разрешимость второго), если устрожим требования к доказательству q и ослабим возможности использования недетерминистской переменной e. Сейчас я постепенно объясню, как сформулировать такое утверждение (будем называть его формальным принципом Маркова).
Ещё в 1970ых [citation needed] заметил, что если запретить использование одной и той же переменной более одного раза (на самом деле, не обязательно запретить, а ограничить строгими правилами), то использование наивного правила формирования множеств не приводит к парадоксу Кантора: сформировать множество, содержащие все множества кроме самого себя, становется невозможно синтаксически. {x | x ∉ x} требует использования одной и той же переменной x дважды в такой форме. Такой контроль также позволяет амнистировать некоторые “неконструктивные доказательства” — при детальном анализе выясняется, что замкнутые доказательства от противного, где контропозитивная гипотеза используется в точности один раз, оказываются конструктивными.
В функциональном языке программирования/исчислении построений (я сейчас о Verse Calculus и Lean/Coq/Agda/Arend одновременно) можно допустить наряду с обыкновенными переменными ещё и переменные одноразовые, и тогда оказывается, что вселенную утверждений Prop можно значительно обогатить!
Наряду с интуиционистскими утверждениями (их proof-terms можно использовать сколько угодно раз в доказательствах) там добавляются ещё недекартовы утверждения. В доказательствах недекартовых утверждений, констатации/опровержения других недекартовых утверждений можно использовать лишь один раз, подробности можно почитать вот тут: https://arxiv.org/pdf/1805.07518.pdf
Я сейчас не предлагаю это читать, а расскажу оттуда некий минимум, нужный чтобы понимать о чём я говорю дальше.
Во-первых, у нас появляется на утверждениях операция -P, такая что -(-P) = P. Загвоздка в том, что для обычного декартового утверждения P его обратное утверждение -P недекартово: это оказывается как бы наше обычное ¬P := P → 𝟘, но только одноразовое. Помните я выше писал, что если в замкнутом доказательстве от противного использовать контрапозитивную гипотезу в точности один раз, то оно получается конструктивным? Вот это и даёт нам идемпотентность такого отрицания, --P = P. При этом надо понимать, что никакого волшебства тут нет — просто далеко не всякое (интуиционистское) доказательство ¬P приводимо к форме -P. Утверждение -P это более сильное утверждение, его сложнее доказать. Но зато, если получилось, то это идемпотентное отрицание.
Сейчас я опишу ещё две операции, при помощи которых формируются недекартовы типы (пока мы не добавили в язык одноразовых переменных, эти операции нам недоступны):
Пусть T некий тип значений, а P(x) предикат на нём, тогда существуют одноразовые обратимые типы
⊓(x : T) P(x) where -⊓(x : T) P(x) := ⊔(x : T) -P(x)
and
⊔(x : T) P(x) where -⊔(x : T) P(x) := ⊓(x : T) -P(x)
Они называются аддитивной (или биконструктивной) конъюнкцией и дизьюнкцией соответственно.
Использование в качестве типа X типа из двух значений позволяет получить бинарные коньюнкцию и дизьюнкцию соответственно, а использование в качестве X пустого типа — нейтральные элементы этих операций.
Биконструктивными они назваются потому что из доказательства или опровержения утверждения с таким квантором впереди всегда извлекается пример/контрпример или прямое доказательство всеобщности. Но за всё приходится платить:
Во-первых доказать ⊓/⊔(x : T) P(x) гораздо сложнее чем ∀/∃(x : T) P(x) — такое доказательство требует вот этой вот недекартовой формы с одноразовым использованием всего, и часто бывает, что ∀/∃(x : T) P(x) доказуемо, а ⊓/⊔(x : T) P(x) нет.
Во-вторых биконструктивности является одноразовость — посылку такого типа в последующем доказательстве недекартового утверждения можно применить лишь один раз.
Есть у нас и оператор !_, превращающая недекартово утверждение Q в декартово !Q с частичной потерей конструктивности:
Для декартовых предикатов P(x) (но не произвольных зависимых типов!) верно
!⊔(x : T) P(x) = ∃(x : T) P(x) ≠ -!⊓(x : T) -P(x)
и
!⊓(x : T) P(x) = ∀(x : T) P(x) ≠ -!⊔(x : T) -P(x)
[Первые равенства также выполняются, если P(x) декартов предикат, но не в случае произвольного зависимого типа P(x)]
Модальность !_ имеет структуру комонады. Есть у него и двойственный оператор, который мы уже видели — монада ?_, сопоставляющая каждому типу значений T junction type ?T всех его значений, мы правда не упомянули что тип ?T вообще говоря недекартов, и поэтому правильнее его называть не junction type, а spectral type.
На данный момент в указанной работе Майка Шульмана, на которую я выше сослался, для типов утверждений (propositional types) выводится вариант аффинной логики, но я полагаю, что такой логике подчиняются только propositional types в univalent dependently-typed verse calculus, а для включения в неё обыкновенных типов (value types) и typed junctions нам потребуется ослабить систему до bi-intuitionistic linear logic.
Теперь вернёмся к принципу Маркова, напомню как он выглядел:
q : ¬∀(n : T) P(n)
–––––––––––––––
e : ?Σ(n : T) ¬P(x)
Если мы усилим требования сверху до недекартового ¬⊓(x : T) P(x), и ослабим результат снизу до недекартового ?⊔(x : T) -P(x), то безо всяких ограничений на предикат P мы получим линейно-логическое тождество
p : ¬⊓(x : T) P(x)
===============
εᵖ : ?⊔(x : T) -P(x)
Чтобы продемонстрировать его, нам понадобятся мультипликативные кванторы — уже знакомый нам
⅋(n : ?T) P(n) и более простой для понимания ⊗(n : !T) ¬P(n).
Впрочем, для демонстрации идеи давайте обойдёмся их бинарными версиями, прекрасно описанными в литературе мультипликативной конъюнкцией и дизьюнкцией, естественным образом возникающими если в качестве типа T подставить булев тип 𝔹 := {tt, ff} с ровно двумя значениями:
X ⅋ Y = ⅋(c : ?𝔹) (if c then X else Y)
X ⊗ Y = ⊗(c : 𝔹) (if c then X else Y)
Теперь давайте выведем “формальный принцип Маркова”:
¬(P ⊓ Q)
========
-!(P ⊓ Q)
=========
-(!P ⊗ !Q)
=========
-!P ⅋ -!Q
=========
?-P ⅋ ?-Q
=========
?(-P ⊔ -Q)
А теперь давайте ещё посмотрим на двойное интуиционистское отрицание ¬¬P. По законам линейной логики ¬¬P = -!(-!P) = ?(-(-!P)) = ?!P. Если посмотреть на правила поведения этого двойного оператора, получается что это propositional lax modality, давайте обозначим её через ⁰P, широко известно что эта модальность вкладывает классическую логику с исключённым третьим в линейную логику. Но это ещё не всё.
Рассмотрим тип значений T. Пользуясь уже описанными выше эквивалентностями,
!⊔(x : T) 𝟙 = ∃(x : T) 𝟙 = |T|, где знаком модуля мы обозначаем propositional truncation. Таким образом с точностью до одноразовости, получаем
p : ⁰P
======
εᵖ : ?|T|
Ой! То есть модальность ⁰_ даёт не просто классическую логику, но ещё и совместимый с унивалентностью оператор выбора эпсилон, у всякого непустого типа есть формальный (недетерминистский и одноразовый) элемент ε. Это даёт нам в точности ту неконструктивную модальность, о которой я писал в предыдущем посте, и которая позволяет внутри унивалентного и в полном смысле конструктивного (decidable typechecking, normalization, canonicity) исчисления построений иметь загончик, в котором можно заниматься классической теорией множеств с аксиомой выбора, более того оно консервативное расширение теории множеств с аксиомой выбора и соответствующим количеством вселенных.
* * *
Я предполагаю, что типизировав verse calculus, и обогатив его всеми фичами HOTT (Higher Observable Type Theory), мы получим квазивычислительную интерпретацию для би-интуиционистской линейной (или аффинной) логики. Для типов вроде натуральных чисел ℕ и булеанов 𝔹 (hereditarily-pure quotient-inductive-inductive type families) там будет выполняться честная skew-canonicity, так что это будет честная вычислительная интерпретация, а для утверждений оно даст как минимум Krivine-type realizability semantics, а в идеале, quantum game semantics.
В 1958 году великий Курт Гёдель стремясь получить убедительное доказательство непротиворечивости арифметики, придумал вычислительную интерпретацию арифметики первого порядка — Dialectica Interpretation.
Отец-основатель линейной логики Jean-Yves Girard начал свою большую карьеру с того, что развил работу Гёделя и разработал вычислительную интерпретацию для арифметики второго порядка (арифметика второго порядка достаточно выразительна, чтобы описывать и вещественный анализ).
Его линейная и аффинная логика это конечно же о том, чтобы завершить эту программу и получить вычислительную интерпретацию для “всей математики” в смысле ZFC and beyond. И сейчас уже реально виден берег.
|
|
(8 comments | comment on this)
|
| Sunday, February 4th, 2024
| |
3:07 am
|
Создатель языка Haskell, сэр Simon Peyton Jones сейчас занимается новым поделием под названием Verse Core. Я немного получше сегодня разобрался в этой штуке, и мне кажется понимаю как вкладывать новшества этой штуки в обыкновенные языки программирования.
Во-первых, зачем это нужно? Нужно это для того, чтобы сделать язык более декларативным. Например, можно будет вот так:
Example 1
let x, y, z
x = (y, 3)
x = (2, z)
x
и вот так
Example 2
let x y : ℚ
x + y = 3
2x + y = 5
print(x)
В первом случае уравнения будут решены при помощи унификации, во втором солвером линейных уравнений. Важно что мы это не руками делаем, а пишем условия, а компьютер нам сам находит подходящее решение.
* * *
В качестве базы синтаксиса возьмём идеализированный академический флейвор Котлина, только с let вместо val для введения локальных констант.
На уровне выше всех остальных свободных от побочных эффектов конструкций языка мы введём четыре оператора:
all {body}, one {body}, a | b и _|_.
“Оператор выбора” | проходит через все конструкции языка. Например для любой функции f : (Int)-> Int
мы можем написать
f(1 | 2 | 3) и получить f(1) | f(2) | f(3). Если функция была от нескольких аргументов g : (Int, Int)-> Int, делаем все комбинации, отсортированные лексикографически:
g(1 | 2, 3 | 4) даст g(1, 3) | g(1, 4) | g(2, 3), g(2, 4).
На первый взгляд может показаться, что (1 | 2 | 3) формирует осообе значение типа ChoiceSequence(1, 2, 3), и применение функций к таковому даёт новый ChoiceSequence, но нет, семантика тут не такая. Выбор не функционирует на уровне значений, let x = (1 | 3) присваивает x значение 1, и если что-то пойдёт в будущем не так, то произойдёт fallback и всё последующее (и предыдущее) вычисление будет произведено заново с вариантом x = 3.
Пустая choice sequence обозначается _|_ и к чему её ни примени, получится оно самое.
Оператор one {body} берёт первый из подходящих результатов либо возвращает _|_ если нет ни одного.
Оператор all собирает все результаты в список:
Example 3
all {let x = (3 | 4); x + 1}
Применение операции с побочными эффектами (скажем, print) к значению энфорсит единственность, т.е. если там не ровно один вариант ответа, кидается exception.
Теперь расширим конструкцию let. Прежде у нас всегда был только короткий вариант `let name = value`.
Сейчас мы позволим этой конструкции во-первых вводить неинициализированные переменные
`let name : Type` или даже просто `let name` в ситуации если тип выводим по контексту.
Более того, если Type перечислимый, то тогда конструкция
`let name : Type` эквивалентна `let name = t1 | t2 | ...`, например
`let n : Nat` то же самое что `let n = 0 | 1 | 2 | ...`.
В индентированном блоке после инструкции let мы позволим вводить дополнительные условия на любые переменные или аргументы. Это выше использовалась в примерах 1 и 2. Собственно конструкция `let x = 5` эквивалентна
let x
x = 5
Приведём также следующие примеры
let n : Int
1 < n
n < 5
print(all {n})
# prints 2, 3, 4
А, например, вот такая конструкция
fun factorial(n : Int)
let
n ≥ 0
...
означает, что если факториал попытаются вызвать с отрицательным аргументом, вычисление не начнётся, а сразу будет выдано _|_. А вот вызов factorial(1 | -1) напротив выдаст один единственный результат.
Example 4
let x, f
f = {v ↦ let {v = (3 · 3, 4 + 4)}}
f(x)
print(x)
# (9, 8)
Вызов f(x) принуждает значение x.
Example 5
let list = listOf(10, 20, 30)
let i
list[i]
# third line enforces i = (0, 1, 2), thus the whole program returns (10 | 20 | 30).
Вот такая экспрессивная штука выходит.
|
|
(1 comment | comment on this)
|
| |
1:07 am - Объекты в качестве параметров типов
|
Вот бывают в программировании типы с параметром, например тип List<T> — это списки, у которых элементы типа T.
Функция, которая может работать со списком любого типа элементов, тоже имеет параметрический тип:
reverse<T>(list : List<T>) : List<T>
В языках вроде Java параметром типа может быть только тип. Но когда система типов покруче, бывает что в качестве параметра выступает значение. Например бывают в математике такие матрицы n на m, где n и m натуральные числа, и вот для них удобно иметь тип Mat<n m : ℕ>.
Умножать матрицы ведь можно только если количество столбцов в левой совпадает с количеством строк в правой.
multiply<m, n, p>(a : Mat<m, n>, b : Mat<n, p>) : Mat<m, p>
В общем полезная штука, когда в качестве параметра типа может фигурировать число или значение какого-нибудь иного типа.
Но осмысленно ли, чтобы в качестве параметра фигурировало не значение, а объект?
В 2016ом, когда я читал первый условно-публичный препринт МакБрайдовского опуса “I Got Plenty o' Nuttin'” на его гитхабе, я никак не мог придумать, зачем бы такое было нужно. И вот читая «Functional Ownership through Fractional Uniqueness» Маршалла и Орхарда я наконец понял, картанка сложилась.
Знаете, в языке Rust можно создать изменяемую переменную. Это как раз пример объекта (а не значения). Например, у нас будет тип MutStr, мутабельная переменная, хранящая строку.
Позже там можно создать на неё readonly-ссылки, и пока все ссылки назад не сдашь, она остаётся заблокированной на запись.
Теперь давайте придумаем как красиво на уровне системы типов принудить к такому поведению.
Для этого у нас будет тип ссылок только для чтения с дробными весами: ReadonlyStrRef<weight : ℚ>,
где вес — положительное дробное число не более единицы.
Блокируя мутабельную переменную (запрещая запись в неё), мы будем получать ссылку на чтение веса 1:
lock(consume v : MutStr) : ReadonlyStrRef<1>
(Блокировка на уровне системы типов заключается в том, что эта операция поглощает нашу переменную v. Её больше нет в контексте и модифицировать нечего.)
Затем такие ссылки мы можем разбивать надвое. . То есть если r : ReadonlyStrRef<s>, то есть поглащающая r операция split, которая возвращает две ссылки весом вполовину меньше:
let (a, b) = split(r),
где
a : ReadonlyStrRef<s/2>
b : ReadonlyStrRef<s/2>
(По факту веса ссылок у нас всегда будут диадическими числами, то есть рациональными числами, где в знаменателе степени двойки.)
Теперь давайте думать, как же “сдавать назад” ссылки, чтобы разблокировать переменную. Давайте просто наивно напишем:
join(x : ReadonlyStrRef<a>, y : ReadonlyStrRef<a>)
: ReadonlyStrRef<a + b>
Так можно соединять ссылки назад, а когда мы назад собрали все получилась ссылка веса 1, и можно разлочить объект:
unlock(r : ReadonlyStrRef<1>) : MutStr
Кто внимательный, заметил проблемку. Мы можем по ошибке сджойнить ссылки на две совершенно разных переменных. Поэтому понадобится нам у ReadonlyStrRef ещё один параметр — собственно переменная, на которую мы ссылку сделали. ReadonlyStrRef<origin : MutStr, weight : ℚ>.
Только я, если можно, буду вместо двухместрых сигнатур использовать запись origin.ReadonlyRef, представив что позаимствовали в языке Scala path dependent types.
И тогда корректные сигнатуры станут такие:
lock(v : Mut<T>) : v.ReadonlyRef<1>
split<v, s>(r : v.ReadonlyRef<s>)
: (v.ReadonlyRef<s/2>, v.ReadonlyRef<s/2>)
join<v, a, b>(x : v.)
join(x : v.ReadonlyRef<a>, y : v.ReadonlyRef<b>)
: v.ReadonlyRef<a + b>
unlock<T, v : Mut<T>>(r : v.ReadonlyRef<1>) : Mut<T>
Важно отличать релевантное использование объекта (при котором объект вообще говоря консьюмится и становится недоступным) от использований в типовых аннотациях, при которых объект не консьюмится, а используется как абстрактное имя. Это то что у МакБрайда называлось в разных версиях статьи icon или ghost. Отметим также, что для использования функций join и unlock совершенно не нужно, чтобы объект v был внутри скоупа: он выводится унификацией параметров типов аргументов.
* * *
Мы тут пока рассуждали только о блокировке изменений переменной и получении на время блокировки реплицируемых readonly-ссылок.
Но возможна блокировка в другом смысле и получение accessors с другими capabilities: скажем можем мы сделать целочисленную переменную, и временно заблокировать как запись в неё напрямую, так и чтение из неё напрямую, получить реплицируемый accessor, позволяющий делать её инкремент (с репликацией тем же самым механизмом с дробными весами, split и join). Так мы получим Grow-only Counter, который нельзя ни считывать, ни сеттить пока кто-то может его инкрементить, а потом когда все “ручки, за которые можно инкрементить” сданы можно посмотреть сумму изменений. Разумеется, вместо Grow-only Counter подойдут любые CRDTы (Conflict-free replicated data type).
* * *
Читатель знакомый с concurrent separation logic заметит, что тройки (weight, original object, accessor capabilities) образуют тот самый частичный коммутативный моноид (PCM), описание которого в явном виде требуется для рассуждений о программе, если у нас появляются некие “вместилища объектов”, обеспечивающие возможность объектам выйти за локальный скоуп функции, где они были порождены.
В Rust'e таковы lifetimes для (мутабельных) переменных, в Kotlin'e coroutineScopes для джобов (запущенных корутин) — они позволяют объектам выйти за локальный скоуп, но всё ещё привязаны к лексическому скоупингу. Их кузены, не привязанные к лексическому скоупингу — персистентные вместищила объектов. Это Heap для переменных, Stage для акторов.
Получение вполне удовлетворительных теоретикотиповых описаний систем, где присутствуют такие сущности — важнейшая из не решенных на данный момент задач прикладной теории типов.
|
|
(1 comment | comment on this)
|
| Wednesday, December 13th, 2023
| |
5:48 pm - 𝔽₁
|
Я тут болею, последние ночи я очень плохо спал. И вчера наконец вкурил давным-давно лежавшую во вкладках статью по математике, которая была мне очень важна.
И поэтому сегодня я хотел поговорить о матрицах — прямоугольных табличках чисел, и эти таблички можно перемножать, если число столбцов в первой равно числу строчек во второй, и это умножение ассоциативно. И есть нейтральные элементы у этого умножения — квадратные матрицы n × n с единицами на главной диагонали и нулями за её пределами. Это по-математически называется “матрицы образуют категорию”.
А ещё матрицы совпадающей размерности можно складывать поэлементно, и это сложение ассоциативно, коммутативно, имеет нейтральные элементы и работает распределительный закон относительно умножения (дистрибутивность). По-математически это называется “матрицы образуют дистрибутивную симметричную моноидальную категорию”. Эти страшные слова ничего не значат кроме того что я выше сказал нормальными словами, если что.
Однако числа, как известно, бывают разные. Можно говорить о матрицах вещественных чисел или матрицах рациональных чисел, например. А имеет ли смысл говорить о матрицах, скажем, натуральных чисел?
В линейной алгебре изучают матрицы чисел, образующих поле, то есть таких которые можно складывать, вычетать, умножать и делить, и для этих операций выполняются законы арифметики. А натуральные числа нельзя ни вычитать, ни делить, но тем не менее матрицы с такими числами ещё как используются в математике.
Чтобы можно было определить умножение и сложение матриц, и все законы этих действий выполнялись (по-математически, “матрицы всё ещё образовывали дистрибутивную симметричную моноидальную категорию”), достаточно чтобы числа в них образовывали унитальное полукольцо. Такую структуру альтернативно называют https://ncatlab.org/nlab/show/rig. Натуральные числа его образуют.
Но это всё классика, а я хочу поговорить о некотором обобщении этого дела. Я часто имею дело с сепарационной логикой и линейными (точнее говоря, субструктурными) логиками. И там мы имеем дело с так называемыми частичными коммутативными моноидами. Это множество, снабженное ассоциативной, коммутативной и унитальной операцией (+) сложения, но операция эта определена не для любых комбинаций аргументов.
Так вот, это наводит на мысль ввести понятие “частичных унитальных полуколец” (partial rig) и матриц над ними.
Например мы можем взять комплексные числа по модулю не больше единицы, и, соответственно, все суммы выходящие по модулю за 1 запрещаются — это про амплитуды в квантовой механике. Или вещественные числа в интервале [0, 1] — это про вероятности. Или натуральные числа, в которых запретили все числа больше 1, — это получается partial rig (обозначим его через 𝔽₁) из двух элементов {0, 1}, а матрицы над ним — матрицы из нулей и единиц, где в каждом столбце разрешается не более одной единицы.
Матрицы над частичными унитальными полукольцами уже тоже не всегда можно складывать, но всегда можно перемножать. Матрицы любого фиксированного размера (включая векторы, которые можно рассматривать как матрицы из одного столбца) по сложению будут образовывать тот самый PCM, частичный коммутативный моноид.
Если partial rig обладает тем свойством, что всякая несигнулярная квадратная матрица над ним обратима, мы будем называть его partial field. Вот это вот вышеупомянутое 𝔽₁ оказывается partial field. И я много лет именно так думаю о так называемом “поле с одним элементом” (https://en.wikipedia.org/wiki/Field_with_one_element).
Категория матриц над ним (её ещё можно назвать “категория векторных пространств над полем с одним элементов”) — это в точности категория множеств с частичными отображениями между ними. Ну или, если угодно, эквивалентно категория пространств с выделенной точкой и сохраняющих точку отображений между ними.
Ещё, кстати, можно ввести гипотетическое определения partial ACF (алгебраически замкнутого частичного поля) — это такое частичное поле, что у всякой квадратной матрицы над ним существует собственный вектор.
* * *
Дело в том, что я занимаюсь сематникой языков программирования, и вообще формальных языков описания физической реальности, где в отличие от платонической математики, далеко не все объекты подлежат точному копированию и не все операции обратимы. Языки описания такой реальности называются субструктурными исчислениями предикатов, а языки описывающие манипуляцию такой реальностью — субструктурными исчислениями построений. Именно в их терминах следует понимать языки программирования, допускающие императивные взаимодействия с внешним миром и concurrency.
Теории типов и исчисления построений, оперирующие только платоническими математическими объектами сравнительно хорошо поняты, и ключевую роль там играют индуктивные типы (вообще говоря, фактор-индуктивные типы) — инициальные модели алгебраических теорий (https://en.wikipedia.org/wiki/Algebraic_theory), а произвольная модель алгебраической теории с носителем T это то же самое, что мотив элиминации из соответствующего индуктивного типа. То есть мы там имеем для каждой алгебраической теории F полиморфный тип F-алгебр Alg_F[T : *].
Для того чтобы разобраться с материальными исчислениями построений, нужно понять каковы будут аналоги индуктивных типов в этом контексте.
Статья которую я читал ночью — Functorial Semantics for Partial Theories (https://arxiv.org/abs/2011.06644), что выглядит для меня как корректно нащупанный подход к определению алгебраических теорий над частичным полем с одним элементом 𝔽₁.
Следующий шаг — понять как это должно работать для произвольного частичного поля, и как на самом деле правильно определять частичное поле. Вот уже семь лет как мне кажется, что правильный путь описан в статье Алена Конна и Катерины Консани https://arxiv.org/abs/1502.05585. Я убеждён, что в терминах таких теорий мы сможем элегантно описывать eventual consistency в распределённом программировани и квантовую спутанность в физике.
Upd: Пока я писал этот пост, я нашёл их новую статью про это https://arxiv.org/pdf/2307.06748.pdf, которую ещё не читал.
|
|
(2 comments | comment on this)
|
| Thursday, October 5th, 2023
| |
1:02 am - Счетные и вычислимые ординалы
|
§ Зачем нужны ординалы?
-----------------------
Ординалы — не просто математический курьёз. У счётных ординалов есть важнейшее практическое применение.
Одна из моих основных областей интересов, которыми я занимаюсь профессионально вот уже почти десять лет — формальное доказательство корректности компьютерных программ. Самая базовая задача — продемонстрировать, что тот или иной рекурсивный алгоритм всегда успешно завершается, т.е. ни при каких входных данных не входит в бесконечную рекурсию. Как подступиться к такой задаче?
Ну вот допустим у нас есть функция f(x, y,..., z), которая в зависимости от конкретных значений параметров (x, y,..., z) может вызывать саму себя с каким-то набором параметров. Чтобы показать, что она завершается, нам достаточно научиться оценивать сверху максимальную глубину рекурсии. То есть задать какую-то такую другую функцию n(x, y,..., z), которая возвращает натуральное число, и убедиться что в процессе исполнения f(x, y,..., z) вызывает саму себя только с такими аргументами (x', y',..., z'), что n(x', y',..., z') < n(x, y,..., z). Таким образом в ходе выполнения цепочка вызовов в какой-то момент закончится, ведь n(...) в какой-то момент в упрётся в ноль, и выполнение f(...) пойдёт по ветке, не содержащей рекурсии. Функция n(x, y,..., z), кстати, называется полуинвариантом.
В простейших случаях мы действительно легко можем оценить n, в нетривиальных случаях удобнее или даже необходимо прибегнуть к обобщению — сказать, что функция n возвращает не обычные натуральные числа, а натуральные числа с custom-ным отношением порядка, всё ещё обладающим тем свойством что любая нисходящая цепочка a < b < ··· < c обязана иметь конечную длину — это свойство называют фундированностью. Натуральные числа со специальным отношением порядка, удовлетворяющим этому свойству, называются счётно-бесконечными ординалами.
Метод доказательства завершимости, использующий в качестве семиинварианта ординал ɑ, называется трансфинитной индукцией порядка ɑ. Название проистекает из того, что этот метод в точности сводится к обыкновенной математической индукции, если в качестве ɑ использовать натуральные числа с обыкновенным порядком.
Тут я отмечу, что и в теории множеств, и в теории типов можно определять и вообще говоря несчётные ординалы. Про них мы тут говорить вообще не будем — это в некотором смысле совершенно другой мир, с другими совершенно другими областями применения.
§ Ординалы в логике
-------------------
В 1934 году Герхард Гентцен применил трансфинитную индукцию (точно как мы описали выше, как метод доказательства завершимости) для доказательства непротиворечивости арифметики первого порядка PA.
Доказательство состоит из следующих частей:
1. Формальное описание языка, на котором записываются все возможные формальные доказательства в рамках арифметики первого порядка;
2. Представление алгоритма “устранения сечений”, приводящего любое доказательство в некую “нормальную форму”, по построению исключающую возможность противоречия;
3. Доказательство, что этот алгоритм всегда успешно завершается — вот тут используется трансфинитная индукция порядка ε₀.
Более того, внутри арифметики первого порядка PA можно доказать трансфинитную индукцию любого порядка ниже ε₀, но не самого ε₀, так как это приводило бы к возможности доказать собственную непротиворечивость, что нарушало бы теорему Гёделя. Таким образом получается что трансфинитная индукция порядка ε₀ не только достаточна для доказательства непротиворечивости PA, но и имеет минимальный возможный порядок. В таком случае говорят что дедуктивная мощность арифметики первого порядка |PA| = ε₀.
С тех пор доказательство Гентцена было обобщено на огромное количество более сильных дедуктивных систем. Алгоритмы устранения сечений в дедуктивных системах уже почти век держат первенство в качестве самых медленных и ресурсоёмких алгоритмов, а величина используемых для демонстрации их завершимости ординалов умопомрачительна. Вникание в их устройство безмерно расширяет представления о том, насколько большими могут быть мыслемые объекты. И тем не менее, речь всё ещё идёт именно о счётно-бесконечных ординалах, более того их подмножестве — вычислимых ординалах, т.к. таких что существует алгоритм, позволяющий сравнить два их элемента между собой. ( Read more...Collapse )
|
|
(4 comments | comment on this)
|
| Friday, June 2nd, 2023
| |
7:03 pm - Вшивый о бане (монады всякие)
|
(Этот же текст с нормальным форматированием и хайлайтингом: https://gist.github.com/akuklev/53cf44920f1ad4b0edd7d56d7ce312da)
Вот кто о чём, а вшивый завсегда о бане. Вот начал я активно и очень много пользоваться Котлином — это язык программирования такой, если вдруг кто не знает. Его Андрей Бреслав сделал, а сейчас им кроме меня ещё больше 5 миллионов людей пользуется, хороший в общем язык. И главное синтаксически очень гармоничный, и поэтому сразу шаловливые мои ручки тянутся его развивать.
Одна из постоянных тем в программировании — corner case handling. Есть какой-то happy path, алгоритм или формула, которые работают в случае общего положения. При этом есть ситуации, которые нужно обработать отдельно. В математической формуле это скажем такие значения переменных, при которых случается деление на нуль. В пошаговом алгоритме — ситуации, когда какой-то компонент не готов/сломался или ещё какая-то ошибка. Часто логика предметной области или конкретной задачи требует особой обработки какого-то специфического случая.
И вот happy path чаще всего записывается удобно и лаконично, его описание удобно читать.
А вот corner cases имеют тенденцию к комбинаторному взрыву, т.к. могут зачастую встречаться в разных комбинациях, поэтому код обработки этих ситуаций имеет тенденцию быть уродливым, нечитаемым и подверженным ошибкам — не ошибкам кодинга, а ошибкой думинга. В смысле не «хотел чтобы программа работала так-то, но неправильно объяснил компьютеру», а «не продумал как следует, что в такой ситуации нужно делать, или вообще не подумал что такая ситуация может случиться». Это те самые ошибки, где зачастую оказываются бессильны формальные математические методы, и уж точно не поможет никакой ИИ. В лучшем случае, формальные методы помогут выявить такие ситуации, а ИИ придумать реалистичный сценарий, в котором они возникают. Но вот придумать что в этой ситуации делать — это часть постановки задачи, это работа программиста (программиста-аналитика), понимающего предметную область и идеологический смысл решаемой задачи.
Так вот, одна из главных задач дизайнеров языка программирования — сделать так, чтобы добавление обработки corner cases не превращала исходную реализацию happy path в нечитаемую стену текста по форме и клубок спагетти по содержанию.
Для этого крайне желательно иметь возможность обрабатывать corner cases как “на месте”, так и “в сноске” и иметь возможность свободно переключаться между этими подходами.
Вариант “в сноске” известен как обработка исключений, вариант “на месте” как null handling в императивных языках программирования, а в функциональных языках программирования — как работа внутри декартовой монады ResultOrFailure.
В Котлине синтаксически весьма приятно устроен null handling и предусмотрено удобное переключение между ним и обработкой исключений — `runCatching {code}` превращает исключения в null, а `expr!!` превращает null назад в исключение. Однако в той форме, как это реализовано сейчас, !! не является обратным к runCatching, т.е. преобразование исключения в null стирает всю информацию про исключение. Чтобы это исправить, необходимо и достаточно добавить в язык custom null objects: https://youtrack.jetbrains.com/issue/KT-59047
Таким образом мы под шумок расширяем удобный синтаксис для работы с nullable values на любые булевы декартовы монады. Ну раз такое дело, так давайте же уже сделаем из этого синтаксиса полноценную do-notation для таких монад, благо это предложение в пропозал строчек: https://youtrack.jetbrains.com/issue/KT-59046, причём идеально укладывающийся в логику синтаксиса языка.
С этим расширением мы можем взять формулу `arctan (a / b)`, не работающую для b = 0, и прям на месте обработать этот исключительный случай:
`arctan ?(a /? b) ?: 90°`
Тут `/?` это как деление, только в случае деления на ноль вернёт null. Вопрос перед скобкой сделает применение функции arctan пропускающим этот null насквозь, а оператор `?:` заменит этот null на 90°.
А обработка “в сноске” тут выглядит как
try {
arctan (a / b)
} catch (e: ArithmeticException) {
90°
}
А ещё в Котлине есть метки, использование которых позволило бы сделать ещё и вот так:
try {
180° - p1@{arctan (a / b)}
} catch@p1 (e: ArithmeticException) {
90°
}
Но это я даже не предлагал пока, больно уж радикально. К тому же тут для гладкости было приятно, если бы можно было опускать try, когда в него завёрнут весь метод целиком.
* * *
Но если уж соприкоснулся с монадами, то на обработке corner cases остановиться невозможно. Очень руки чешутся по аналогии с синтаксисом для обработки null'ов сделать полноценную do-notation, ведь она тоже очень красиво укладывается в логику языка: https://youtrack.jetbrains.com/issue/KT-59052
Это ожидаемо в Котлин не берут, потому что он не Скала (и слава богу, наверное).
А теперь смотрите внимательно. Выше мы видели двойственность — можно обрабатывать corner cases при помощи null-object handling а можно при помощи exception handling, и между ними можно переключаться. За этим математически вообще красивая штука стоит, называется сопряженная пара монады и комонады.
Так вот, do-notation в Котлин не пускают, а сопряженная с ним штука там цветёт и здравствует, и называется type-safe builder notation, и считается жемчужиной языка. Type-safe builder устроен так что мы вдоль всего кода тащим с собой один конкретный мутабельный объект и периодически дёргаем его методы. Например, мы можем вот так сгенерировать список:
val x = listOf('b', 'c')
val y = buildList() {
add('a')
add(*x)
repeat(3) {
add('d')
}
add('e')
}
println(y) // [a, b, c, d, d, d, e]
Внутри скоупа buildList() у нас к имеющимся операторам-с-побочными-эффектами (например, throw) добавляются ещё все методы специального мутабельного объекта под названием листбилдер. Ну и мы просто выполняем какой-то код, между делом потихоньку наполняем этот самый билдер, а когда блок закончится, на выходе у нас будет обычный (в идеале, иммутабельный) список.
Этот самый “избранный мутабельный объект, методы-мутаторы которого в текущем скоупе используются как операторы-с-побочными-эффектами” на математическом языке называется комонадой.
Раз объект-контекст type-safe builder'ов в Котлине мутабельный, то Type-safe builder'ы получаются последовательные (Sequential, или Serial), двойственные к do-нотации для монадических декораторов.
А что будет двойственным к do-нотации для аппликативно-функториальных декораторов? Интуитивно кажется, что это должен быть вариант type-safe builder'ов, где объект-контекст не неограниченно-мутабельный, а аккумулятивный. Типа как в примере с `buildList()`.
|
|
(13 comments | comment on this)
|
| Friday, April 21st, 2023
| |
4:06 am - Viva Starship!
|
Я поздравляю нас всех с невероятно успешным первым запуском космического корабля Starship. На слове “поздравляю” фейсбук показывает красивый фейерверк, что особенно подходит к случаю — фейерверк тоже был, на высоте 38 километров. Но дело не в фейерверке, а в том, что было до него — успешный старт и полёт Starship'а до самой стадии разделения ступеней.
Это штука огромная! По размеру это натурально летающий 35-этажный дом, на каждом этаже которого по квартире площадью 65 кв. метров. Эта штуковина в полтора раза тяжелее и крупнее, чем какая либо ракета за всю историю космонавтики, сегодня её двигатели развили совокупную тягу в два раза выше чем у Сатурна 5, летавшего на луну (прежнего рекордсмена по этому параметру). Falcon 9 в шутку вывел на орбиту машину Тесла, а эта штуковина способна вывести на орбиту советский чугунный тепловоз, и вернуться обратно — он целиком влезает в отсек для полезной нагрузки и проходит по массе, и ещё место останется.
Прежде тестировали только верхнюю ступень, и совсем чуть-чуть. Отдельного теста первой ступени ещё не было ни разу, и ещё ни разу не пытались запускать все её 33 двигателей одновременно на земле. Ни разу не пользовались стартовой площадкой, с которой её запускали. Соответственно, старт был обложен граблями просто со всех сторон.
Сегодня тестировали корабль в сборе, с совершенно нового стартового стола оригинальной конструкции. Я ожидал проблем до старта и остановку обратного отсчёта на последних секундах, ожидал что оно взорвётся на стартовом столе и разнесёт его к чертям. Если не взорвётся и не разнесёт, ожидал что либо не взлетит, либо полетит не туда или взорвётся на первых 30 секундах полёта.
Оно, на первый взгляд штатно, пролетело больше двух минут, успешно достигнув сверхзвуковой скорости и пройдя стадию максимального скоростного напора (Max Q, максимальная нагрузка на корпус корабля) не развалилось, и не взорвалось. На такой благополучный исход я даже не надеялся, я оценивал его вероятность ну максимум 5-10%. После такого результата можно быть совершенно уверенными, что новаторские двигатели Raptor (самые совершенные в истории космонавтики по многим параметрам) и корабль принципиально рабочие, и через несколько итераций доводки и тестов удастся добиться удачного выхода на орбиту.
Конечно же, остаётся открытым вопрос, удастся ли планируемым сейчас способом возвращать обе ступени на землю целыми и невредимыми, не откроются ли экономически непреодолимые грабли по части теплоизоляционной обшивки, как это было у шаттла (там надо было перебирать эту обшивку после каждого старта с такими сложностями, что многоразовость шаттла была по некоторым оценкам экономически убыточной). Конечно же, сделать Starship настолько же надёжным и многоразовым, как сейчас Falcon 9, займёт несколько лет доводки и сотни стартов. Но это уже вопрос рутинной обкатки и доводки, а не принципиальной реализуемости.
Уже несколько десятилетий человечество пребывало в жалком и постыдном положении: самый могучий, крупный и грузоподъёмный корабль построили наши деды, имея в распоряжении лишь очень примитивные по нынешним меркам инструменты. Он успешно стартовал первый раз 57 лет назад и последний раз 50 лет назад. С тех пор мы ни разу ничего такого не делали и постепенно растеряли даже способность просто воспроизвести результат без малого 60-летней давности.
Сегодня это недостойное положение дел было наконец исправлено. В космонавтике началась новая эра.
|
|
(15 comments | comment on this)
|
| Thursday, March 9th, 2023
| |
6:39 am - Умчи меня туда
|
Очень давно, примерно 2002-2003 ко мне попала нестандартная запись «Лесного оленя», она мне жутко понравилась аранжировкой, необычным подбором инструментом, соло-импровизациями в середине и в конце и голосом одной из двух исполнительниц, причём той из них которая в полный голос поёт только в припеве (отдельно его можно услышать, например на 121-123 секундах), который мне напоминал голос моей покойной мамы, которой на тот момент не было ещё всего несколько месяцев. Её обычный голос это, кстати, не напоминает, но на её певческий голос похоже, его знали немногие, потому что в присутствии каких-то посторонних людей или тем более публично она на моей памяти никогда не пела.
Запись я эту потерял вместе с каким-то из умерших жестких дисков лет пятнадцать назад, но у меня неплохая звуковая память, поэтому я нередко слушал её в голове по памяти, и даже как-то раз успешно подбирал на пианино кусочек соло. А сейчас подумал — почему бы не отыскать. И знаете, за полчаса отыскал, даже меньше. Оказалось это с альбома «Когда проснётся Бах» Фёдора Чистякова, и там весь альбом совершенно обалденный. Кстати, мне кажется, что я вспомнил, что мне её прислал Pavel Reich, надо будет по логам ICQ посмотреть, они должны были где-то сохраниться. Вокалисток, кстати, зовут Виктория и Светлана Знаменская, к сожалению не знаю кто из них кто, да и вообще никакой информации о них сходу разыскать не удалось.
https://youtu.be/9hWjugQsntI?t=120
|
|
(8 comments | comment on this)
|
| Saturday, October 9th, 2021
| |
7:57 pm - Towards Univalent Construction Calculus
|
Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning.
By “modern” let us mean MLTTs featuring the empty type 𝟘, the unit type 𝟙 inhabited solely by the symbol 𝟘, the type 𝔹 (bit or boolean type) inhabited by the symbols 𝟘 and 𝟙, and a cumulative hierarchy of univalent universes (types containing symbols for other types) closed under forming quotient inductive-inductive types (QIITs), dependent product types “∀(x : X) Y” and identity types “x = y”:
```
𝟘 ⊃ 𝟙 ⊃ 𝔹 ⊃ 𝓤 ⊃ 𝓤⁺ ⊃ 𝓤⁺⁺ ⊃ ···,
𝟘 : 𝟙 : 𝔹 : 𝓤 : 𝓤⁺ : 𝓤⁺⁺ : ···,
```
Such theories support a huge repertoire of value types, here's a list of some random examples:
– Natural numbers `ℕ`;
– Finite lists of integer Numbers (`List[ℤ]`);
– Sequences of rational numbers (`Seq[ℚ]`);
– Countable subsets of real numbers (`CSet[ℝ]`);
– Turing-complete computations yielding a complex number if they halt (`℧(ℂ)`).
Types `P` satisfying `∀(x y : P) x = y` are called propositional and enjoy propositional resizing, i.e. once it is proven that a type `P : 𝓤⁺ⁿ` is propositional, it is guaranteed to have an isomorphic copy in the smallest open universe U. Predicates and relations on value types can be represented propositional types and composed by conjunction, disjunction, implication, negation as well as quantifiers `∀(x : X) P(x)` (a special case of the dependent product) and `∃(x : X) P(x)` (can be defined as a QIIT) in a way faithfully representing higher-order intuitionistic logic with equality. Proofs and mathematical constructions can be represented as terms of the theory. Univalence allows transporting proofs and constructions along isomorphism and equivalences of mathematical structures and induces the natural extensional notion of identifiability (equality, isomorphy, equivalence, etc.) for propositions, functions, conductive types, and all sorts of mathematical structures such as groups, rings, categories, and topological spaces. Constructiveness means that proofs can be algorithmically verified and terms of closed inductive types like 𝔹 or ℕ can be algorithmically evaluated to a fixed bit value or numerical value respectively. [Footnote: Constructive type theories are thus abstruse programming languages capable to express both total and Turing-complete computations, without being able to specify their operational behavior and effectively control their computational complexity. It is possible to extend it to a genuine programming language by introducing linear types, but that's another story.]
What can we wish more? ( Read more...Collapse )
|
|
(4 comments | comment on this)
|
| Friday, July 9th, 2021
| |
11:16 pm
|
Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что так ведь так не с любой толпой...
TechCrowd, около миллиона людей, занятых в индустрии новейших технологий или восхищённых ими, съехавшиеся со всего света на огромнейшую выставку, которую просто невозможно физически обойти менее чем за два дня, выставку, где впервые в истории показывают кучу офигеннейших новинок (таких как например смартфоны или беспроводной интернет). Невероятно яркие цвета и запахи, невероятно выглядящие люди со всего света — японцы, корейцы, индусы, невероятные одежды и прически, манеры и языки.
Многие из вас родились уже в XXI веке, и контекст совершенно непонятен. Когда я был маленький, у нас дома не было телефона. Не мобильного телефона, а никакого телефона. Если кому-то, например, бабушке хотелось что-то срочно сообщить нам, то самым быстрым способом было сесть на автобус и через полчаса приехать, с риском не застать нас дома. Тогда можно было оставить записку и сунуть её в дверь. Договориться о приходе заранее было невозможно, как невозможно было и отменить заранее согласованную встречу. При хороших отношениях с имеющими телефон соседями, можно было позвонить куда-то от соседей, или в совсем-дико-экстренных случаях могли позвонить соседям и попросить что-то передать. Но это потом, когда к дому подвели телефон, в первые потора года во всем доме не было ни одного телефона.
Когда я был в детском лагере, самым быстрым способом что-то передать домой было послать телеграмму, на следующий день она гарантированно доходила. Телефон был, один на весь лагерь, по нему заведующая могла вызвать скорую помощь или там сообщить чьим-то родителям что кто-то сломал руку. Дело в том, что междугородные звонки стоили чудовищно дорого, кроме того просто взять и позвонить по телефону в другой город было невозможно, ну просто нет способа набрать номер, не находящийся в предалах того же населённого пункта. Чтобы позвонить в Омск из лагеря в области, нужно было _заказать_ междугородний звонок, и через полчаса-час телефон звонил, на том конце провода была телефонистка, которая соединяла. С родственниками и друзьями из других городов мы переписывались письмами (в зависимости от интенсивности общения от одного письма в месяц до парочки в год) и перезванивались примерно один раз в год. Кроме Омска, мелких городков и деревень Омской области, и Новосибирска я не бывал вообще нигде до 11 лет, на самолете ни разу не летал до 16 лет. До 11 лет я не видел ни моря, ни другой крупной реки, кроме той, что протекает в Омске, ни гор. На отдых ездили в леса и/или на речку в пределах автомобильной доступности, за один день езды по раздолбанным дорогам. Всякие там дома отдыха ведомственные ещё были в деревнях Омской области — Чернолучье, Красноярка. За всю жизнь до 6 лет я вживую общался может быть с пятью иностранцами, а видел в непосредственной близости может быть человек 15 максимум, не считая трудовых мигрантов из Китая и Вьетнама. Среди них ни одного японца, ни одного индуса или там южноамериканца. Ни одного негра, кстати. Все кого я видел были европейцы или североамериканцы, не сильно отличающиеся от жителей России внешним видом и в плане одежды, причёсок и всякого такого отличающиеся разве что тем, что одежда более дорогая, а люди чуть более ухожены. Ну и никаких культурных шоков, людей с розовыми волосами, английских лордов. Да что там, я ни одного живого вегитарианца на тот момент не встречал.
Напоминаю, мне не сто лет, мне сейчас всего 36. :-)
Так вот, чтобы понять, насколько на выставке в 1996 году меня поразил интернет (а ещё там был VR-шлем), нужно понимать именно этот контекст. В 2001 году я внезапно оказался в Ганновере, и через полгода попал на CeBIT – крупнейшую международную выставку IT, и это был конечно взрыв мозга. Сто новых технологий и устройств за три дня, какие-то невероятные японцы с синими волосами на самокатах. Это как будто оказываешься в фантастическом фильме, а вокруг инопланетяне. Ну и да, технологии про которые сложно сейчас поверить, что так было не всегда, в тот момент показывались просто впервые: от цветных экранов мобильных телефонов, видеозвонков через интернет и до интернет-банкинга и соцсетей – да-да, они всё это появилось в 2001ом, а до этого ничего этого не было вовсе. До этого эти штуки были в фантастических книгах и фильмах, а на выставке их можно было взять и попробовать. И вот это удивительное ощущение причастности к вот этой разноязыкой, но очень близкой по интересам и мировоззрениями толпе, объединённой вовлечённостью в эту невероятную технологическую революцию.
|
|
(27 comments | comment on this)
|
| Monday, May 10th, 2021
| |
12:47 pm - Прогресс
|
Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась назад на космодром. Это, на-минуточку, стальная болванка размером 55 метров в высоту и 9 в диаметре. То есть как 15-этажный дом, у которого на каждом этаже квартира площадью более 60 квадратный метров. Оно летает и садится. И в 2024 году полетит на луну, скорее всего.
Вторая новость менее свежа и менее зрелищна, но куда более монументальна. На тестовой установке C2-W (Норман) компании Tri-Alpha Energy (с инжекторами нейтралов из Новосибирского ИЯФа им. Будкера) научились стабильно держать хорошую плазму температуры 50-70 миллионов градусов по 5 миллисекунд, причём время ограничено только запасом энергии на прогрев плазмы и вопросами теплоотвода. На следующей тестовой установке они рассчитывают поднять температуру ещё в два с половиной раза и получить таким образом условия, достаточные для стабильной реакции синтеза дейтерия с тритием, таким образом обогнав ИТЭР.
Такой демонстратор у них скорее всего получится. Демонстратор, а не энергоустановка, дляпотому что там не будет предусмотрено устройств для съема произведённой энергии, и кучи-кучи-кучи невероятно сложны инженерно устройств охлаждения, радиационной защити и проч., позволяющей такой установке работать в непрерывном режиме.
Дело в том, что цель их в другом — цель добиться безнейтронной (не производящей радиоактивных отходов) реакции синтеза p-¹¹B, для чего нужно будет поднять температуру ещё в десять раз. Но это святой грааль энергетики и ракетостроения.
Во-первых, безнейтронная реакция это уже не “чайник топить”: в отличие от атомных реакторов и реакторов на дейтериево-тритиевом синтезе, которые просто греют теплоноситель, из которого энергию добывают при помощи паровых турбин, с безнейтронной реакции можно снимать электроэнергию напрямую, благодаря чему возможен несравнимо более высокий КПД.
Во-вторых, на безнейтронной реакции синтеза можно сделать прямоточный термоядерный ракетный двигатель, не убивающий радиацией всё живое на корабле. И одновременно, являющийся энергоустановкой для внутренних нужд корабля, не требующий недоступных в открытом космосе систем теплоотвода. И это единственный вид ракетных двигателей, дающий:
1) перспективу путешествий за пределы Солнечной Системы;
2) перспективу пилотируемых межпланетных путешествий дальше Марса.
Я совсем не уверен, что TAE успеют как они надеются к 2030-2040 году, но чёрт с ним, главное чтобы они вообще в принципе хоть когда-нибудь смогли, потому что если у них получится — то это новая эра в жизни человечества. Эра энергетической независимости (от ископаемых, стационарных и волатильных источников) и доступности межпланетных путешествий.
|
|
(50 comments | comment on this)
|
| Thursday, May 6th, 2021
| |
10:37 am - О водосбережении
|
Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она на какое-то время становится дефицитным ресурсом.
Я уже много раз об этом писал, но иногда не грех напомнить.
Эффективность использования воды в домохозяйствах развитых странах можно при двух параллельных канализаций — одной для так называемых практически чистой мыльной воды (“серый сток”), другой для всего остального (“чёрный сток”). Серые стоки — это вода из раковин, душа, ванной, стиральной и посудомоечной машины. Использование двух канализаций позволяет минимум вдвое сократить эффективный расход воды домохозяйствами, потому как серые стоки составляют от 50 до 60% канализации каждого жилого дома, и могут быть на 100% использованы повторно минимальными усилиями:
— Во-первых, серые стоки можно вообще без фильтрации использовать для смыва в туалете, таким образом понижая расход воды домохозяйствами на 30%.
— Во-вторых, после нейтрализации моющих средств, такая вода может сразу применяться для полива. Напомню, что для нейтрализации моющих средств не требуются химикаты и вообще расходные материалы, используются только долгоживущие катализаторы + ульрафиолет. И установка по обезмыливанию воды небольшая и спокойно влезает в подвале в техническое помещение.
Например в Германии в домах с разделением канализации (увы, это пока большая редкость) расход водопроводной воды составляет в среднем всего 60л на человека в день. В малоэтажных домах с участком (таких, где живёт максимум 2-3 семьи) очень часто есть ещё система сбора дождевой воды, которая используется для полива. В таких домах можно дополнительно озаботиться вторым водопроводом для “свежей дождевой воды”, чтобы мыться, стирать и мыть полы дождевой водой — так можно сократить расход до 20-30л в день на человека. К сожалению в многоэтажных домах эта система не работает — собираемой с многоэтажки дождевой воды хватает только для полива газона и насаждений на прилегающей территории. Важно, однако помнить, что в состоятельных засушливых приморских странах для всех тех же нужд очень хорошо применять опреснённую морскую воду. Таким образом, реальная потребность в питьевой водопроводной воде составляет лишь 20-30л на человека безо всякой экономии и с ежедневным душем щедрой струёй.
А теперь внимание: всё это не имеет никакого смысла, если воду не экономят в сельском хозяйстве и в индустрии. В развитых странах только
9-12% расхода воды приходится на домохозяйства,
50-75% на индустрию,
25-30% на сельское хозяйство.
За пределами развитых стран почти вся вода (ок. 80%) используется для нужд сельского хозяйства.
Почему же важно всё-таки говорить о методах снижения расхода воды в домохозяйствах? Потому что для нужд сельского хозяйства и индустрии полностью хватает опреснённой морской воды. Кроме того, существуют технологии (капельное орошение в сельском хозяйстве и куча всего в индустрии), позволяющие на порядок снизить расход воды.
|
|
(15 comments | comment on this)
|
| Sunday, May 2nd, 2021
| |
10:36 am - 36
|
|
| Saturday, March 13th, 2021
| |
4:34 am - Посудомойка моей мечты
|
Оказывается существует общее решение для двух кухонных проблем:
1) Как сделать посудомойку, чтобы от её загрузки не страдали люди с больной спиной?
2) Что делать с бессмысленным угловым пространством?
Решение (правда, на мой взгляд, чуть-чуть недодуманное) придумали 5 лет назад дизайнеры Mohsen Jafari Malek и Behzad Taheri, см. приложенное изображение. Как жалко, что никто пока не сделал такой посудомоечной машины!
А мои соображения такие:
1) Штырь посреди очень жрет пространство и мешает загрузке. Штырю лучше быть в дальнем углу, а от него уже пусть идут под центр каждого из ящиков горизонтальные опоры с поворотным шарниром. Поворотный шарнир (он предполагается и в оригинальном дизайне) — это чтобы ящики можно было поворачивать и таким образом иметь оптимальный доступ к дальнему краю. Для машины стоящей в глухом углу кухни это необходимость.
2) У ящиков не нужно срезать углы! Достаточно просто сделать поворотный шарнир выезжающим, т.е. когда начинаешь поворачивать ящик, он отъезжает по своей направляющей от штыря в углу так, чтобы углы ящика не тёрлись об стену и не мешали повороту.
3) Сверху над посудомоечной машиной могут висеть шкафчики, в которые вся эта выезжающая наверх конструкция может упираться, поэтому верхнюю крышку лучше сделать откидной для экономии места.
4) Отдельное горизонтальное отделение для столовых приборов (как во всех машинках Miele) не только очень удобная вещь, но и очень экономит полезный объем остальных ящиков. Мне оптимальный вариант видится так:
– Сверху откидная крышка;
– Под ней отделение для ложек-вилок-ножей, оно не поворотное, и откидывается как и крышка;
– После того, как всё это откинул, наверх выезжают собственно ящики с посудой.
Доступ к фильтрам, отделению с солью, отделению для запаса моющего средства (который нужно пополнять раз в месяц-другой, потому что автоматическая система дозирования) и, в экстренном случае, для прочистки и ремонта — через боковую стенку, через соседний нижний шкафчик. Как правило это будет шкафчик под раковиной.
|
|
(14 comments | comment on this)
|
| Wednesday, January 27th, 2021
| |
2:33 am - Языки программирования
|
Я тут понял удивительную вещь. Одно из тех открытий, когда вдруг понимаешь, что всю жизнь говорил прозой. Ну когда обнаруживаешь, что ты какую-то вещь считал естественной, считал что вообще все вокруг так думают, а оказывается, ровно наоборот: так не думает почти никто.
Итак, открытие: кажется, подавляющее большинство математиков и подавляющее большинство программистов думаю о языках программирования как об инструментах для “компьютерщиков”. Ну типа как какие-то там специальные отвертки с моторчиком или вроде того, чтобы где-то покрутить и компьютер начал делать то что нужно.
Для меня язык программирования это, разумеется, инструмент концептуализации и моделирования той или иной предметной области. В первую очередь математических построений, потому что любая другая предметная область пользуется математическими конструкциями (попробуйте сформулировать какую-нибудь бизнес-логику, не прибегая к понятиям пары, списка и числа). Естественно sine qua non для языка программирования в моей голове — возможность записывать на нём концептуально чисто и элегантно известные уже 2300 лет геометрические построения и алгоритм Эвклида.
Именно поэтому я столько лет не понимал, когда очень сильные программисты начинали тирады что в языках программирования не нужна поддержка замыканий и прочего FP, или наоборот ратовали только за pure FP без каких-либо выразительных средств для описания императивных алгоритмов. Ну как можно _хотеть_ работать на языке, на котором _невозможно сказать то, что ты имеешь в виду_? Как можно хотеть разговаривать на птичьем языке Эллочки-людоедки, в рамки которого просто не влезают _правильные_ концептуализации того, с чем мы работаем?
Именно поэтому я столько лет не понимал, когда знакомые математики отмахивались от HoTT со словами “ну, наверное программистам это полезно, но зачем это нужно в математике пока непонятно”. Как это может быть непонятно? Математика кишмя кишит построениями, от и до. Определение какиех-нибудь когомологий это описание того, как их строить. Теорема о неявной функции — это декларативное описание того, как строить функцию по её уравнению.
Мы можем конечно делать вид, что словесное описание с картинками (коим пользовался и Эвклид ещё ~2300 лет назад), это и есть идеальный способ описания построений. Но если бы это было так, не было бы затруднений несколькими умелыми штрихами превращать словесные описания в формализованные машинно-читаемые. Раз это далеко не так, значит в словесных описаниях лишь видимость conceputal clarity, а на самом деле что-то существенное замели под ковёр. Значит должно быть интересно, что именно замели под ковёр, и как этого избежать не теряя в элегантности описания построений. И тут природа как обычно даёт нам подсказку, что мы копаем в нужном месте — тем удивительным фактом, что на пути формализации построений откуда ни возьмись вдруг возникает нетривиальная современная математика.
|
|
(53 comments | comment on this)
|
| Monday, January 25th, 2021
| |
11:49 pm - Корневищный такой...
|
Задремал... проснулся от видения, точнее обоняния, вкуса и осязания. Мне привиделся креп-суп с нежно подкопчёнными полосками трески, нежными лисичками и кубиками обжаренной брюквы, а к этому был ароматный латгальский хлеб — ч0рный-пречёрный кисло-сладкий ржаной хлеб, и винегрет, как давеча был у  Юлия Ремпель — классический в общем-то русский винегрет, но такой, что можно есть тарелка за тарелкой и остановиться просто невозможно. И такие были текстуры во рту, и хрусткая квашеная капуста в винегрете, и лисички такие, даже не опишешь толком, и кубики брюквы — чуть-чуть надкусываешь, а потом можно уже размять языком, а там вкус такой насыщенный, посконный корневищный вместе с мягкостью жаренной картошки, а крем суп обволакивающий, но не однородный, с некоторым характером.
Я проснулся и никак не мог решить, чем же это запить, вроде бы и чёрный хлеб, но и такие разнообразные текстуры и вкусы во рту. Сошелся с собой на очень охлаждённом (градусов до 10) гевюрцтраминере, хоть и не очень он идёт ко всей этой еде, но вот как-то захотелось. Вообще суп этот прекрасный с брюквой в ресторане Kartoffelhaus у нас тут в брюквенный сезон делают, и подают к нему тёмное пиво — разливной чешский Staropramen, к брюкве он конечно больше подходит, но не к нежно подкопчённым полоскам трески, вот в чём загвостка.
А потом я совсем проснулся и понял, что мне это всё к сожалению только приснилось, и что-то обидно стало, по коей причине и решил я написать это текст и выставить его на публичное обозрение, чтобы и в вас тоже вселился ночной жор.
|
|
(5 comments | comment on this)
|
|
|
|
|
