ДР Цертуса 2011

(no subject)

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

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

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

Счетные и вычислимые ординалы

§ Зачем нужны ординалы?
-----------------------

Ординалы — не просто математический курьёз. У счётных ординалов есть важнейшее практическое применение.

Одна из моих основных областей интересов, которыми я занимаюсь профессионально вот уже почти десять лет — формальное доказательство корректности компьютерных программ. Самая базовая задача — продемонстрировать, что тот или иной рекурсивный алгоритм всегда успешно завершается, т.е. ни при каких входных данных не входит в бесконечную рекурсию. Как подступиться к такой задаче?

Ну вот допустим у нас есть функция 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| = ε₀.

С тех пор доказательство Гентцена было обобщено на огромное количество более сильных дедуктивных систем. Алгоритмы устранения сечений в дедуктивных системах уже почти век держат первенство в качестве самых медленных и ресурсоёмких алгоритмов, а величина используемых для демонстрации их завершимости ординалов умопомрачительна. Вникание в их устройство безмерно расширяет представления о том, насколько большими могут быть мыслемые объекты. И тем не менее, речь всё ещё идёт именно о счётно-бесконечных ординалах, более того их подмножестве — вычислимых ординалах, т.к. таких что существует алгоритм, позволяющий сравнить два их элемента между собой. Collapse )
ДР Цертуса 2011

Вшивый о бане (монады всякие)

(Этот же текст с нормальным форматированием и хайлайтингом: 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()`.
ДР Цертуса 2011

Viva Starship!

Я поздравляю нас всех с невероятно успешным первым запуском космического корабля Starship. На слове “поздравляю” фейсбук показывает красивый фейерверк, что особенно подходит к случаю — фейерверк тоже был, на высоте 38 километров. Но дело не в фейерверке, а в том, что было до него — успешный старт и полёт Starship'а до самой стадии разделения ступеней.

Это штука огромная! По размеру это натурально летающий 35-этажный дом, на каждом этаже которого по квартире площадью 65 кв. метров. Эта штуковина в полтора раза тяжелее и крупнее, чем какая либо ракета за всю историю космонавтики, сегодня её двигатели развили совокупную тягу в два раза выше чем у Сатурна 5, летавшего на луну (прежнего рекордсмена по этому параметру). Falcon 9 в шутку вывел на орбиту машину Тесла, а эта штуковина способна вывести на орбиту советский чугунный тепловоз, и вернуться обратно — он целиком влезает в отсек для полезной нагрузки и проходит по массе, и ещё место останется.

Прежде тестировали только верхнюю ступень, и совсем чуть-чуть. Отдельного теста первой ступени ещё не было ни разу, и ещё ни разу не пытались запускать все её 33 двигателей одновременно на земле. Ни разу не пользовались стартовой площадкой, с которой её запускали. Соответственно, старт был обложен граблями просто со всех сторон.

Сегодня тестировали корабль в сборе, с совершенно нового стартового стола оригинальной конструкции. Я ожидал проблем до старта и остановку обратного отсчёта на последних секундах, ожидал что оно взорвётся на стартовом столе и разнесёт его к чертям. Если не взорвётся и не разнесёт, ожидал что либо не взлетит, либо полетит не туда или взорвётся на первых 30 секундах полёта.

Оно, на первый взгляд штатно, пролетело больше двух минут, успешно достигнув сверхзвуковой скорости и пройдя стадию максимального скоростного напора (Max Q, максимальная нагрузка на корпус корабля) не развалилось, и не взорвалось. На такой благополучный исход я даже не надеялся, я оценивал его вероятность ну максимум 5-10%. После такого результата можно быть совершенно уверенными, что новаторские двигатели Raptor (самые совершенные в истории космонавтики по многим параметрам) и корабль принципиально рабочие, и через несколько итераций доводки и тестов удастся добиться удачного выхода на орбиту.

Конечно же, остаётся открытым вопрос, удастся ли планируемым сейчас способом возвращать обе ступени на землю целыми и невредимыми, не откроются ли экономически непреодолимые грабли по части теплоизоляционной обшивки, как это было у шаттла (там надо было перебирать эту обшивку после каждого старта с такими сложностями, что многоразовость шаттла была по некоторым оценкам экономически убыточной). Конечно же, сделать Starship настолько же надёжным и многоразовым, как сейчас Falcon 9, займёт несколько лет доводки и сотни стартов. Но это уже вопрос рутинной обкатки и доводки, а не принципиальной реализуемости.

Уже несколько десятилетий человечество пребывало в жалком и постыдном положении: самый могучий, крупный и грузоподъёмный корабль построили наши деды, имея в распоряжении лишь очень примитивные по нынешним меркам инструменты. Он успешно стартовал первый раз 57 лет назад и последний раз 50 лет назад. С тех пор мы ни разу ничего такого не делали и постепенно растеряли даже способность просто воспроизвести результат без малого 60-летней давности.

Сегодня это недостойное положение дел было наконец исправлено. В космонавтике началась новая эра.
ДР Цертуса 2011

Умчи меня туда

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

Запись я эту потерял вместе с каким-то из умерших жестких дисков лет пятнадцать назад, но у меня неплохая звуковая память, поэтому я нередко слушал её в голове по памяти, и даже как-то раз успешно подбирал на пианино кусочек соло. А сейчас подумал — почему бы не отыскать. И знаете, за полчаса отыскал, даже меньше. Оказалось это с альбома «Когда проснётся Бах» Фёдора Чистякова, и там весь альбом совершенно обалденный. Кстати, мне кажется, что я вспомнил, что мне её прислал Pavel Reich, надо будет по логам ICQ посмотреть, они должны были где-то сохраниться. Вокалисток, кстати, зовут Виктория и Светлана Знаменская, к сожалению не знаю кто из них кто, да и вообще никакой информации о них сходу разыскать не удалось.

https://youtu.be/9hWjugQsntI?t=120
ДР Цертуса 2011

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? Collapse )
ДР Цертуса 2011

(no subject)

Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что так ведь так не с любой толпой...

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

Многие из вас родились уже в XXI веке, и контекст совершенно непонятен. Когда я был маленький, у нас дома не было телефона. Не мобильного телефона, а никакого телефона. Если кому-то, например, бабушке хотелось что-то срочно сообщить нам, то самым быстрым способом было сесть на автобус и через полчаса приехать, с риском не застать нас дома. Тогда можно было оставить записку и сунуть её в дверь. Договориться о приходе заранее было невозможно, как невозможно было и отменить заранее согласованную встречу. При хороших отношениях с имеющими телефон соседями, можно было позвонить куда-то от соседей, или в совсем-дико-экстренных случаях могли позвонить соседям и попросить что-то передать. Но это потом, когда к дому подвели телефон, в первые потора года во всем доме не было ни одного телефона.

Когда я был в детском лагере, самым быстрым способом что-то передать домой было послать телеграмму, на следующий день она гарантированно доходила. Телефон был, один на весь лагерь, по нему заведующая могла вызвать скорую помощь или там сообщить чьим-то родителям что кто-то сломал руку. Дело в том, что междугородные звонки стоили чудовищно дорого, кроме того просто взять и позвонить по телефону в другой город было невозможно, ну просто нет способа набрать номер, не находящийся в предалах того же населённого пункта. Чтобы позвонить в Омск из лагеря в области, нужно было _заказать_ междугородний звонок, и через полчаса-час телефон звонил, на том конце провода была телефонистка, которая соединяла. С родственниками и друзьями из других городов мы переписывались письмами (в зависимости от интенсивности общения от одного письма в месяц до парочки в год) и перезванивались примерно один раз в год. Кроме Омска, мелких городков и деревень Омской области, и Новосибирска я не бывал вообще нигде до 11 лет, на самолете ни разу не летал до 16 лет. До 11 лет я не видел ни моря, ни другой крупной реки, кроме той, что протекает в Омске, ни гор. На отдых ездили в леса и/или на речку в пределах автомобильной доступности, за один день езды по раздолбанным дорогам. Всякие там дома отдыха ведомственные ещё были в деревнях Омской области — Чернолучье, Красноярка. За всю жизнь до 6 лет я вживую общался может быть с пятью иностранцами, а видел в непосредственной близости может быть человек 15 максимум, не считая трудовых мигрантов из Китая и Вьетнама. Среди них ни одного японца, ни одного индуса или там южноамериканца. Ни одного негра, кстати. Все кого я видел были европейцы или североамериканцы, не сильно отличающиеся от жителей России внешним видом и в плане одежды, причёсок и всякого такого отличающиеся разве что тем, что одежда более дорогая, а люди чуть более ухожены. Ну и никаких культурных шоков, людей с розовыми волосами, английских лордов. Да что там, я ни одного живого вегитарианца на тот момент не встречал.
Напоминаю, мне не сто лет, мне сейчас всего 36. :-)

Так вот, чтобы понять, насколько на выставке в 1996 году меня поразил интернет (а ещё там был VR-шлем), нужно понимать именно этот контекст. В 2001 году я внезапно оказался в Ганновере, и через полгода попал на CeBIT – крупнейшую международную выставку IT, и это был конечно взрыв мозга. Сто новых технологий и устройств за три дня, какие-то невероятные японцы с синими волосами на самокатах. Это как будто оказываешься в фантастическом фильме, а вокруг инопланетяне. Ну и да, технологии про которые сложно сейчас поверить, что так было не всегда, в тот момент показывались просто впервые: от цветных экранов мобильных телефонов, видеозвонков через интернет и до интернет-банкинга и соцсетей – да-да, они всё это появилось в 2001ом, а до этого ничего этого не было вовсе. До этого эти штуки были в фантастических книгах и фильмах, а на выставке их можно было взять и попробовать. И вот это удивительное ощущение причастности к вот этой разноязыкой, но очень близкой по интересам и мировоззрениями толпе, объединённой вовлечённостью в эту невероятную технологическую революцию.
ДР Цертуса 2011

Прогресс

Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась назад на космодром. Это, на-минуточку, стальная болванка размером 55 метров в высоту и 9 в диаметре. То есть как 15-этажный дом, у которого на каждом этаже квартира площадью более 60 квадратный метров. Оно летает и садится. И в 2024 году полетит на луну, скорее всего.

Вторая новость менее свежа и менее зрелищна, но куда более монументальна. На тестовой установке C2-W (Норман) компании Tri-Alpha Energy (с инжекторами нейтралов из Новосибирского ИЯФа им. Будкера) научились стабильно держать хорошую плазму температуры 50-70 миллионов градусов по 5 миллисекунд, причём время ограничено только запасом энергии на прогрев плазмы и вопросами теплоотвода. На следующей тестовой установке они рассчитывают поднять температуру ещё в два с половиной раза и получить таким образом условия, достаточные для стабильной реакции синтеза дейтерия с тритием, таким образом обогнав ИТЭР.

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

Дело в том, что цель их в другом — цель добиться безнейтронной (не производящей радиоактивных отходов) реакции синтеза p-¹¹B, для чего нужно будет поднять температуру ещё в десять раз. Но это святой грааль энергетики и ракетостроения.
Во-первых, безнейтронная реакция это уже не “чайник топить”: в отличие от атомных реакторов и реакторов на дейтериево-тритиевом синтезе, которые просто греют теплоноситель, из которого энергию добывают при помощи паровых турбин, с безнейтронной реакции можно снимать электроэнергию напрямую, благодаря чему возможен несравнимо более высокий КПД.
Во-вторых, на безнейтронной реакции синтеза можно сделать прямоточный термоядерный ракетный двигатель, не убивающий радиацией всё живое на корабле. И одновременно, являющийся энергоустановкой для внутренних нужд корабля, не требующий недоступных в открытом космосе систем теплоотвода. И это единственный вид ракетных двигателей, дающий:
1) перспективу путешествий за пределы Солнечной Системы;
2) перспективу пилотируемых межпланетных путешествий дальше Марса.

Я совсем не уверен, что TAE успеют как они надеются к 2030-2040 году, но чёрт с ним, главное чтобы они вообще в принципе хоть когда-нибудь смогли, потому что если у них получится — то это новая эра в жизни человечества. Эра энергетической независимости (от ископаемых, стационарных и волатильных источников) и доступности межпланетных путешествий.
ДР Цертуса 2011

О водосбережении

Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она на какое-то время становится дефицитным ресурсом.

Я уже много раз об этом писал, но иногда не грех напомнить.

Эффективность использования воды в домохозяйствах развитых странах можно при двух параллельных канализаций — одной для так называемых практически чистой мыльной воды (“серый сток”), другой для всего остального (“чёрный сток”). Серые стоки — это вода из раковин, душа, ванной, стиральной и посудомоечной машины. Использование двух канализаций позволяет минимум вдвое сократить эффективный расход воды домохозяйствами, потому как серые стоки составляют от 50 до 60% канализации каждого жилого дома, и могут быть на 100% использованы повторно минимальными усилиями:
— Во-первых, серые стоки можно вообще без фильтрации использовать для смыва в туалете, таким образом понижая расход воды домохозяйствами на 30%.
— Во-вторых, после нейтрализации моющих средств, такая вода может сразу применяться для полива. Напомню, что для нейтрализации моющих средств не требуются химикаты и вообще расходные материалы, используются только долгоживущие катализаторы + ульрафиолет. И установка по обезмыливанию воды небольшая и спокойно влезает в подвале в техническое помещение.

Например в Германии в домах с разделением канализации (увы, это пока большая редкость) расход водопроводной воды составляет в среднем всего 60л на человека в день. В малоэтажных домах с участком (таких, где живёт максимум 2-3 семьи) очень часто есть ещё система сбора дождевой воды, которая используется для полива. В таких домах можно дополнительно озаботиться вторым водопроводом для “свежей дождевой воды”, чтобы мыться, стирать и мыть полы дождевой водой — так можно сократить расход до 20-30л в день на человека. К сожалению в многоэтажных домах эта система не работает — собираемой с многоэтажки дождевой воды хватает только для полива газона и насаждений на прилегающей территории. Важно, однако помнить, что в состоятельных засушливых приморских странах для всех тех же нужд очень хорошо применять опреснённую морскую воду. Таким образом, реальная потребность в питьевой водопроводной воде составляет лишь 20-30л на человека безо всякой экономии и с ежедневным душем щедрой струёй.

А теперь внимание: всё это не имеет никакого смысла, если воду не экономят в сельском хозяйстве и в индустрии. В развитых странах только
9-12% расхода воды приходится на домохозяйства,
50-75% на индустрию,
25-30% на сельское хозяйство.

За пределами развитых стран почти вся вода (ок. 80%) используется для нужд сельского хозяйства.

Почему же важно всё-таки говорить о методах снижения расхода воды в домохозяйствах? Потому что для нужд сельского хозяйства и индустрии полностью хватает опреснённой морской воды. Кроме того, существуют технологии (капельное орошение в сельском хозяйстве и куча всего в индустрии), позволяющие на порядок снизить расход воды.
ДР Цертуса 2011

36

Традиционный деньрожденный пост.
Год выдался необычный. :)