ДР Цертуса 2011

(no subject)

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

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

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

Глушители шума для квадрокоптеров и турбин

Хотите пример технологии с богатейшим потенциалом? Смотрите: https://4everscience.com/2020/09/08/uchyonye-sproektirovali-material-kotoryj-blokiruet-94-zvukov/

(там есть видео)

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

Я практически уверен, что можно добиться ещё больших результатов, комбинируя это с активным шумоподавлением.

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

А если совсем фантазировать, то это шаг на пути к летающим машинам. :-)
ДР Цертуса 2011

Запланированное устаревание

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

Задумался, сколько в Германии жилья старше 70 лет, оказалось 25% всех жилых зданий. А 14% всех жилых зданий старше ста лет! Более чем половина зданий старше 70 лет — дорогое, качественное жильё, с запасом удовлетворяющее современным требованиям по планировке и метражу, много превосходящее даже большую часть новостроек по вентиляции и освещённости и лишь немного уступающее современному жилью по теплоизоляции.

Самое смешное, что среди того что построено даже за последние 10 лет, столь добротного жилья примерно те же 50%. А вот с войны до 1970 года практически ничего добротного не строили, не до того было, почти всю застройку этого периода в принципе не жалко, ну не считая некоторой культурно-исторической ценности, тоже ведь важный период истории был, который именно эта архитектура отражает.
ДР Цертуса 2011

Водный транспорт

А сейчас производят какие-нибудь скоростные речные трамваи, вроде «Ракет» на подводных крыльях?
Помню в детстве были все эти Ракеты, Кометы, Метеоры, Восходы 50х-60ых годов изготовления с неплохой для такого вида транспорта крейсерской скоростью 60-65 км/ч («Восходы» были 70ых, но ТТХ почти такие же). А потом это всё как-то не развивалось, хотя казалось бы, хорошая вещь.

Ещё помню был французский проект BGV (Bateau à Grande Vitesse), который появился в 80ые, потом его пытались воскресить из мёртвых то в 90ые годы, то в 2000ные. Это должны были быть трёхточечные глиссеры-паромы, и они должны были развивать на воде скорость аж 120 км/ч...
ДР Цертуса 2011

Embracing Largeness and Taming it

What's missing to Intuitionistic Type Theories (ITTs) is the ability to talk about, say, all groups: you can talk only about `U`-small groups for a given universe `U` there. It is not the case in case of Construction Calculi (common generalisation to ITTs and second-order lambda calculus System F).

In a particular Construction Calculus variant we're developing (Cedille Core with Reflective Univalent Universes), it is possible to define the type classes like `Group[T : *] : *` supplying a group structure on the type `T`. In general, carrier is not limited to be a single type, it can be a pair of types, a type former (say, `Endofunctor[F : * -> *] : *`), a sequence of types (say, `Spectrum[Ts : Nat -> T] : *`) or even something dependent, say `Category[Ob : *, Hom : Ob -> Ob -> *] : *` that supplies a type with a and a type and a type twice indexed by the first type by the structure of a category.

You can actually provide proofs and constructions for _all_ groups, say `DirectProduct[A B : *](G : Group[A], H : Group[B]) : Group[A × B]`. Functors between categories and natural transformations between functors are definable too: their carriers are complicated, but feasible to work with.

Furthermore, there you actually do have a notion of locally-small category of structured objects. It takes a typeclass on * (like Grp) as the first parameter:
```
LSCategory[Str : * -> *, Hom : (X Y : *) -> Str[X] -> Str[Y] -> *]
```

Even more generally, for any theory T presented in intuitionistic first order logic with dependent sorts (FOLDS) one can define a respective locally-small n-category of models. Any theory `T` has a fixed dependency depth `n` and fixed carrier kind `ϰ` the definition of respective n-Categories starts like
```
LSᵀCategory[Str : ϰ -> *, Hom : (X Y : ϰ) -> Str[X] -> Str[Y] -> *, Hom₂ : ···, Homₙ : ···]`.
```

In particular, one can define a locally-small 2-category of small categories and so on, with their respective functors, natural transformations etc.

It is not possible to abstract on kinds `ϰ` and thus also theories `T`, but it seems undesirable. We strive to develop a calculus with strong reflection properties (large objects behave exactly like `U`-small ones), so that we can derive a metatheoretical result that one can actually always work with U-small ᵀCategories, on which level abstracting on `T` is surely possible.
ДР Цертуса 2011

Упражнения по энергетике

Давно, кстати, хотел проделать мысленное упражнение про эффективный дизельный генератор для частного дома. Поразмышлять я, правда, хотел чисто об эффективности на этапе использования, оставив в стороне вопросы жизненного цикла, т.е. цены, долговечности, издержек производства и утилизации.

Вот допустим есть частный дом, и его хозяева хотят быть независимыми от внешних поставщиков энергии, но одновременно свободно пользоваться энергией. Разница между базовым и пиковым потреблением электроэнергии огромна — они различаются в 20-30 раз. Никакой генератор не может эффективно работать на 1/20-ой своей максимальной мощности, поэтому какая-то эффективность возможна только с использованием большой батарейки, благо у лучших образцов нынче потери энергии на цикле зарядки-разрядки меньше 1%. Тогда от дизельного генератора требуется обеспечивать пиковую нагрузку совместно с батарейкой (стало быть потребная пиковая мощность генератора может быть гораздо ниже), и включаясь то и дела фоново в своём оптимальном по КПД режиме подзаряжать батарейку время от времени. Разумеется, подразумевается, что если он будет работать в этом самом оптимальном по КПД режиме всё время (либо всё время с перерывами на охлаждение, необходимыми конструктивно), то за сутки он суточное потребление электроэнергии домохозяйством уж точно вырабатывает с запасом.

Дневное потребление электроэнергии (горячую воду, отопление и кондиционирование сперва оставим в стороне) частного дома на одну семью составляет в зависимости от количества людей и их привычек где-то от 5 до 16 кВт-ч. При этом средняя базовая потребляемая мощность меньше 1 кВт даже для большой семьи, а в качестве пиковой мощности обычно закладывают 15 кВт, и это без запаса на то, что в доме делают ремонт или что там живёт любитель помастерить электросварочным аппаратом (мощностью до 7 кВт).

Большая батарейка как раз под такое использование — Tesla Powerwall 2, там общая ёмкость 13.5кВт-ч, то есть в общем как раз на сутки. Выдавать она умеет до 2 кВт непрерывно и до 7 кВт пиково. То есть нам понадобится ещё дизельный генератор, способный пиково выдавать ещё 10кВт, ну чтоб с запасом.

Самые эффективные на сегодняшний день экспериментальные двигатели (дающие в оптимальном режиме КПД 55%) имеют отношение оптимальной и пиковой мощности 1:3. В предположении, что эти двигатели можно отмасштабировать, в фоновом режиме такой двигатель сможет полностью зарядить Powerwall 2 за 4 часа, потратив всего 2 литра дизеля*, и будет он иметь рабочий объём всего порядка 0.35л!

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

_______
* Кстати побочно он за эти самые 4 часа будет производить как раз достаточно тепла, чтобы обеспечивать дом горячей водой для мытья рук + чуть более 1 часа душа в сутки.
ДР Цертуса 2011

Выжать до капли

Несколько месяцев назад, в феврале 2020-го впервые была показана работающая на природном газе газотурбинная установка на вращающейся детонационной волне, то есть там происходит не объемное сжигание топлива, а детонация во фронте волны, бегущей кругами по кольцевой камере: “Operability of a Natural Gas–Air Rotating Detonation Engine”, Walters et al., doi:10.2514/1.B37735.

Кроме того, что это попросту очень сложно сделать технологически, были большие сомнения, что это вообще удастся сделать именно не для чистого метана, а для природного газа, т.е. метана с примесями. Но предложенная схема мало того что работает — она, вероятно, сработает и для биогаза — возобновляемого топлива, обильно добываемого на городских очистных сооружениях, а также на комбинатах по переработке сельскохозяйственных отходов и пищевого мусора, химически представляющего из себя природный газ не самой чистой пробы, к которому домешано 20-30% CO₂.

Детонация в волновом фронте — это, по видимому, предельно совершенный способ извлечения энергии из горючих материалов*, круче уже некуда. Когда технология доберётся до индустриального использования, она сулит нам электростанции на природном и биогазе с электрической эффективностью свыше 70%, причём даже для некрупных газотурбинных установок общей мощностью порядка 100 МВт, использующихся в небольших теплоэлектростанциях. А именно небольшие теплоэлектростанции (обеспечивающие один завод или некрупный район города) часто удаётся использовать максимально эффективно, то есть организовать для них разумное использование оставшейся тепловой мощности — для теплоснабжения предприятий или для отопления и снабжения горячей водой близлежащих домов.

На сегодняшний день рекорд эффективности принадлежит парогазовым установкам General Electrics 7HA.03 общей мощностью порядка 1000 МВт. Их электрическая мощность составляет 640 МВт, и у них 64%-ная эффективность преобразования в электроэнергию топливной энергии, заключённой в природном газе. Это блоки для крупных теплоэлектростанций, для которых редко удаётся организовать очень уж эффективное использование остаточного тепла: только если рядом есть крупнейшее тёплоёмкое производство, либо электростанция стоит при крупном городе в регионе с суровыми зимами. И то, при теплоснабжении крупного города из одной точки получается не настолько эффективно — много тепла теряется по дороге, слишком уж длинный путь от станции до конечного потребителя в среднем выходит.

Барьер в 60% электрической эффективности преодолели всего десять лет назад, а через пару лет производители рассчитывают выйти на 65%. Так что 70⁺%, хотелось бы надеяться, не за горами. Но миниатюризация высокоэффективных парогазовых установок — это ещё следующий шаг, сейчас в отношении теплоэлектростанций районного масштаба всё не так уж радужно — там рекорд электрической эффективности на сегодняшний день едва выше 50%.

_______
* Исключая водород и, в теории, другие щелочные металлы, для которых возможны топливные элементы мембранного типа, обеспечивающие конверсию в электроэнергию всей энергии Гиббса.
ДР Цертуса 2011

Равенство Лейбница как кодирование Чёрча и Cedille

А вот все говорят, что равенство Лейбница это импредикативное кодирование равенство Мартин-Лёфа.

А вот Cedille получается кодировать индуктивные типы через зависимые пересечения соответствующего им типа импредикативного кодирования, и принципа индукции. Разберём на примере натуральных чисел.

Вот тип алгебр над сигнатурой натуральных чисел:
```
NatAlg := ∀[T : ∗], (succ : T -> T, zero : T)
```

Сами натуральные числа Nat — алгебра, свободно порождённая succ и nat, её можно также охарактеризовать как инициальную среди всех таких алгебр, т.е. из неё существует уникальный гомоморфизм в любую такую алгебру: т.е. в частности это означает, что берём элемент `n : Nat`, берём алгебру `A : NatAlg`, замешиваем их и получаем некий элемент A.T. Можно попробовать сказать, что элементы `Nat` это и есть такие “черные ящики”, превращающие всякую Nat-алгебру в её элемент:
```
Nat-ish := ∀[T : ∗], (T -> T) -> T -> T
```

Это и есть нумералы Чёрча, несложно показать что этот тип имеют выражения следующего вида:
```
zero := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ n
one := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(n)
two := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(f(n))
three := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(f(f(n)))
...
```

А следующая функция превращает нумерал в следующий нумерал:
```
succ(m : Nat-ish) := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ (m(f))(f(n))
```

Все синтаксически-выразимые объекты типа Nat-ish суть натуральные числа. Но, ежели у подлежащей теории есть теоретикомножественные модели, то в этих моделях тип Nat-ish неизбежно будут населять ещё и бестии, невыразимые синтаксически. Однако можно ведь попытаться выделить среди них “настоящие”, т.е. те, для которых работает математическая индукция. Давайте запишем тип, выражающий математическую индукцию, т.е. позволяющий доказать предикат P(n : Nat) для всех n, обладая доказательствами базы индукции P(0) и шага индукции P(n) -> P(succ(n)):

Nat-ly := (n : Nat-ish) ↦ ∀[P : Nat-ish -> ∗], (step : ∀[n : Nat-ish], P(n) -> P(succ n)) -> (base : P(zero)) -> P(n)

В Cedille есть способ выделить среди типа Nat-ish элементы, которые сами себе доказательство индукции (термы n, которые могут быть типизированны одновременно как элементы Nat-ish и как элементы Nat-ly(n) для самого себя):
```
Nat := (n : Nat-ish, n : Nat-ly(n))
```

Вот для этого типа в Cedille можно показать, что это в самом деле тип натуральных чисел.

* * *

Теперь давайте попробуем проделать то же самое для типа равенства. Равенство-лейбница термов `x y : T` записывается как тип
```
Id-ish[T : ∗](x y : T) := ∀[P : T -> ∗], P(x) -> P(y)
```

Запишем также терм
```
refl[T : ∗](x : T) : ∀(P : T -> ∗), (\p : P(x)) ↦ p
```
и обратим внимание, что `refl[T](x) : Id-ish[T](x, x)`.

Теперь давайте вспомним как устроена индукция для равенства Мартин-Лёфа:
```
Id-ly[T : ∗](x y : T) := (p : Id-ish[T](x, y)) ↦ (∀[P : Id[T] -> ∗], P(refl)) -> P(p)
```

Кто-нибудь уже изучал тип `Id-ish[T : ∗](x y : T) := (p : Id-ish[T](x, y), p : Id-ly[T](x, y)(p))` в Cedille?
ДР Цертуса 2011

A Framework for Complex Symbolic Languages and Structured Categories

A Framework for Complex Symbolic Languages and Structured Categories
====================================================================

ABSTRACT: We develop two extensions to the formalism of algebraic theories of successively increasing strength to provide a formalism for symbolic languages including proposition and proof languages for standard logical systems and internal languages for plethora of structured categories.
The first one, IIR-EAT, can be understood as stratified version of essentially algebraic theories with slightly refined semantics following the natural model approach of [Awo16]: it allows for more models, yields a more flexible notion of isomorphism and makes IIR-EATs into a superset of Cartmell's Generalised Algebraic Theories without equations on sorts[Car81]. This formalism is sufficient for symbolic languages of first order logical systems, categories with simple algebraic structure (e.g. monoidal categories) and most notably also weak ⍵-categories[Fin17]. We present explicit IIR-EATs of symbolic languages for the single-sorted equational logic and first order logic with dependent sorts[Makkai]. Axiomatic theories are then free algebras for logic systems they are defined upon.
The second one, XAT (extended algebraic theories), goes even further and incorporate a staging mechanism known as bidirectional typing that allows well-controlled circular type dependencies. XATs can represent symbolic languages of higher order logics and internal languages of (quasi)categories with arbitrary properties that can be expressed as essentially unique algebraic structures (existence of products, limits, internal homs, subobject and object classifiers). XATs have natural functorial semantics in the doctrine of recently developed fibrant weak model categories [Hen20], and the category of models for each theory carries a structure of fibrant weak model category itself. XATs facilitate exact formulations of syntax-semantics duality and Baez-Dolan microcosm principle.


§ Introduction: Symbolic Languages
==================================

The idea of symbolic languages traces back to Leibniz. He conceived symbolic languages for knowledge representation, logical arguments, specification of devices and systems, and even legislation. Symbolic languages were to be strictly unambiguous, have a precise well-defined grammar, a carry an intrinsic notion of sentence identity, i.e. it should be clear what details of how a sentence is being written down (or spoken out, or represented in any other way) are insignificant).

{Sidenote: There is a related notion of formal languages in computer science. There, sentences are assumed to be represented as finite sequences of characters of predefined alphabet. This notion differs from the notion of symbolic language by prescribing the representation and lacking unambiguity. In applications, formal languages are usually to be parsed: processed into an unambiguous abstract syntax tree, or rather abstract syntax representation, because plain trees are in general not enough to represent languages with binders like the first order logic (the quantifiers are operators with binders). Symbolic languages are formal languages modulo parsing: they're about abstract syntax representations.}

Statements, proofs and constructions in mathematics are mostly written using natural languages (e.g. English) as a matter of fact. But at least since Frege(cf. https://en.wikipedia.org/wiki/Begriffsschrift, 1879) it is universally assumed that it's possible to use well-defined symbolic language instead. Mathematicians keep writing up their results using natural languages because they are way more human-readable and much better at expressing subtleties and the thought process which lead to the result: ultimately a goal of a paper is not just establishing a mathematical fact but also instructing the reader how to carry out such or a similar proof themselves. Yet mathematicians strive to keep relevant parts trivially translatable into the respective symbolic language.

While mentally using a symbolic language or two (the first order logic and its proof language, known as natural deduction) for these purposes, generic pure mathematicians have had little interest in symbolic languages as subject of study. The area was predominantly studied by computer scientists driven by applications: symbolic languages are used computer-aided knowledge representation, software development (declarative programming languages are precisely the symbolic languages for specification of algorithms, interactive systems and distributed systems) and computer-verifiable proofs. Being application-driven, the area relied on a patchwork of ad-hoc formalisms of varying mathematical elegance and no strong connections to other areas of mathematics.

In recent decades, a solid theory of symbolic languages has begun to emerge, uncovering a multitude of connections to category theory, abstract homotopy theory and algebraic geometry.

§ Exposition: Symbolic Languages and Algebraic Theories
=======================================================

Mathematical facts (theorems) are stated and proven inside of a respective axiomatic theory, e.g. Euclidean Geometry. For sake of reusability and composability of mathematical results, generic mathematicians[^1] usually work inside of a common environment: an axiomatic theory of vast generality known as Zermelo–Fraenkel set theory, into which more specialised axiomatic theories (like theory of groups) are submerged. However, it makes a lot of sense to study specialised axiomatic theories in their own right.

An axiomatic theory is defined upon a chosen underlying logic (usually, classical first order logic unless stated otherwise) and is given by
– a language in which propositions of the theory are stated (the language of the underlying logic extended by theory-specific syntax), and
– a finite or recursively generated set of axioms in this language, i.e. propositions assumed to be true a priori in this particular theory.

A logic consists of an extendible common language base for axiomatic theories stated upon this logic, and a language for proofs specific to this logic. These symbolic languages can be described in terms of formation rules (also called “inference rules” in proof languages) generating a set of well-formed (by construction) propositions and a set of correct (by construction) proofs respectively.

Fig. 1: Examples of formation and inference rules.
```
 A : Prop   B : Prop       A : Prop   B : Prop   x : Pf[A]    y : Pf[A => B]
—————————————————————     ———————————————————————————————————————————————————Modus Ponens
    A => B : Prop                           MP(x,y) : Pf[B]

```

Collapse )
ДР Цертуса 2011

Пожалуйтесь на бога в вышестоящую инстанцию

(из частной переписки)

Сама идея, что физическая реальность не является вопросом компромисса, как-то не укладывается в головах.

Политики, журналисты, колумнисты, общественные деятели привыкли, что всякий, кто что-либо заявил публично по какому-то вопросу, в дальнейшем интересуется не содержательной стороной вопроса, а отстаиванием своей правоты.
Диалог с добросовестным учёным вызывает у них чудовищное недоумение. Учёный то меняет мнение “как флюгер”, как только выяснятся новые обстоятельства, то оказывается упрямым как террорист, и не идёт ни на какие на переговоры — нет чтобы как современные гибкие люди, сдать немножечко своей позиции, ну хотя бы чтобы показать цивилизованность и договороспособность, согласиться хотя бы для приличия, что 2 + 2 не 4, а хотя бы ну может быть 3,8 или 4,1. От большого уважения к бесноватому гению они готовы предложить аж 3,95, но “варвары” от науки просто с цепи сорвались со своим невероятно раздутым эго, продолжают настаивать на том, что 2 + 2 = 4.
То ли дело вирусолог Х, — сетует условный колумнист Фокуса, — вот тот, как только раскритиковали его пресс-релиз, что 2 + 3 = 6, сразу пошёл на встречу и согласился на пять с половиной. Вот цивилизованный человек!

Но ладно бы только это, ведь они же массово пытаются торговаться со стихией, как будто можно ставить ей условия или хитрить с ней путём подгонки фактов. “Мы готовы закрыть школы, но только по средам и пятницам.” Ну молодцы что готовы. Природе/богу похер что вы готовы, а что нет. Обидно, что бессердечная стихия не оценила и без того титанические старания? You feel offended? Ну не знаю, пожалуйтесь на бога в вышестоящую инстанцию, или назло маме отморозьте уши. Только нас в это не втягивайте.