Category: мода

Category was added automatically. Read all entries about "мода".

ДР Цертуса 2011

(no subject)

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

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

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

Plug-in гибриды не в моде?

Аргументировали мне тут, что нынче plug-in (точнее говоря, я имею в виду series-)гибриды не в моде, лучше мол только электричество.

Мои представления о прекрасном таковы, что ездить оптимально было бы именно на электромобилях с компактным range extender'ом на обыкновенном топливе, т.е. том, что называется series hybrid.

От мотора, выполняющего функции range extender'а не требуется ни умения работать в широком диапазоне оборотов (он будет работать вообще на фиксированных оборотах, где работает оптимально), ни иметь запас мощности и крутящего момента для обгона/езды в горку. Кроме того, он никогда не заглохнет и у него никогда не будет холодных стартов. Всё это позволяет в качестве такового взять какой-нибудь компактный мотор (CREEV Wankel engine или вот LiquidPiston) с воздушным охлаждением и мощностью этак на 30-50kW*.

Мазда так уже пробовала в своём демонстраторе в 2013-м, и у них весь range extender на 30kW вместе с топливным баком, системой подачи топлива, и системой очистки выхлопа, влез в 100 кг, и поместился под задним сиденьем, там где обычно топливный бак бывает — а вместо нормального топливного бака они взяли десятилитровый. У LiquidPiston есть прототип X-4 (дизельный), который даёт 37kW, весит 20 кг, влезает в куб со стороной 28 см и имеет КПД 45%. Такой КПД — это очень круто для мотора легкового автомобиля, больше бывает только у дизелей, которые весят как минимум под тонну. Но, правда, он таки с жидкостным охлаждением. И, ессно, одному богу известно какой там выхлоп и насколько затратно его будет почистить.

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

Как вы думаете, что экономичнее и экологичнее — иметь гигантский аккумулятор (сплошь из драгоценного сырья и с токсичными отходами внутре) и вообще без мотора, или иметь аккумулятор которого хватает на повседневные поездки (более 200 дней в году), а когда не хватает (8-80 дней в год), начинать жечь топливо на трассе?

____
* 30 kW позволяет ехать нашему довольно крупному VW Touran'у со скоростью 130 по плоскости на столько, на сколько хватит бака. При КПД 45% это будет 4.22 литра дизелю на сотню.
50 kW позволяет ехать сколько влезет со скоростью 160, и при указанном КПД потребляться будет 7.04 литра дизеля на сотню.
ДР Цертуса 2011

Очень зависимые типы

Николай Краус и коллеги недавно высказали гипотезу, что HoTT можно дополнить ещё одним полезным в хозяйства конструктором зависимых типов данных, впервые упомянутым в 1996 году под названием "очень зависимая функция". Этот конструктор является одновременным обобщением зависимой суммы и зависимого произведения, из-за чего он крайне симпатичен.

Смотрите, это тип пары двух натуральных чисел:
(Nat, Nat)

А вот это тип пары двух натуральных чисел, таких что второе не больше
первого:
(n : Nat, Fin(n))

А вот это тип натуральнозначной функции на натуральных числах:
Nat -> Nat

А вот это более рестриктивный тип, он требует чтобы значение было не больше аргумента:
(n : Nat) -> Fin(n)

Существует совершенно фундаментальная эквивалентность между кортежами (парами, тройками и т.д.) и списками конечной длинны. Для однородных списков это вообще тривиально, (Nat, Nat, Nat) == (Fin(3) -> Nat), для кодирования гетерогенных списков справа потребуются уже зависимые функции:
(A, B, C) == (selector : Fin(3)) -> selector |>
  0 => A
  1 => B
  2 => C


Наша цель в том, чтобы можно было и зависимый кортеж вида
(a : A, b : B(a), c : C(a, b),..)
представить в виде функции. Для этого нам понадобится, чтобы тип значения функции на более старших аргументах мог зависеть от значений этой же самой фукнции на более младших аргументах.
(a : A, b : B(a), c : C(a, b),..) == (sel : Fin(3) -> (\fs => sel |>
  0 => A
  1 => B(fs(0)
  2 => C(fs(1))
))


Именно эта конструкция называется "очень зависимым типом". Она обобщает понятие "зависимого кортежа" на случай кортежей бесконечной длины, индексированных индуктивным семейством типов. Такой конструктор типов позволяет формулировать алгебраические структуры, которые не могут быть конечно аксиоматизированы, и, предположительно, пучки над категорями Риди, в том числе семи-симплициальные и симплициальные типы, слабые омега-группоиды (симплициальные типы Кана), Г-пространства. На данный момент конструкция проработана только для обратных категорий, т.е. случая семи-симплициальных, семи-кубических и т.д. типов.

Указанный выше синтаксис позволяет в теле выражения после -> применять f к любым аргументам, т.е. мы лишены синтаксической защиты от циркулярных определений. При определении конкретной функции f вместе с её типом такую защиту легко организовать. Для начала рассмотрим случай, когда каждый последующий тип кортежа T(n) зависит только от предыдущего значения (а не от всех предыдущих):
mutual
  f: (s : Fin(3)) -> t(s)
    ...

  t: Fin(3) -> Type
    0 => T(0)
    succ(n) => T(n) (f(n))


Тип Fin(3), разумеется, можно заменить на любой другой индуктивный тип, добавив в тело t разбор всех его конструкторов. Тут видно, что как только мы заполним многоточие телом функции f, функция f и её тип будут корректно определены взаимно рекурсивно-индуктивно. Мы без особого труда можем расширить зависимость на ситуацию, когди тип T(n) элемента кортежа зависит от всех предыдущих значений:
mutual
  f: (s : Fin(3)) -> t(s)
    ...

  t: Fin(3) -> Type
    0 => T(0)
    succ(n) => T(n) (fs(n))

  ts: Fin(3) -> Type
    0 => t(0)
    succ(n) => ts(n) × t(n + 1)

  fs: (s: Fin(3)) -> ts(s)
    0 => f(0)
    succ(n) => (fs(n), f(n + 1))


Как и выше, Fin(3) легко обобщается до произвольного индуктивного семейства типов. Как мы видим, синтаксическое определение очень зависимого типа совместно с конкретным представителем такого типа не представляет проблем. Как сформулировать синтаксическое определение очень зависимого типа в отрыве от конкретного представителя? Выше приведён способ развязать этот узел примитивно -- раз тип очень зависимых функций из W определяется функцией t(s: W, fs: subterm(s) -> ...): Type, то и будем писать в качестве формера (s : W) -> (\fs => well-formed type expression), однако возникают вопросы, нет ли более элегантного способа развязать этот узел в духе контейнеров.
ДР Цертуса 2011

Раз уж заговорили об ООП

Совсем недавно Андреас Россберг показал, как надо было делать SML, см. http://www.mpi-sws.org/~rossberg/1ml/1ml.pdf. В MLях традиционно (т.е. во всех ML без зависимых типов) существует два независимых уровня языка: языковое ядро и язык описания модулей/функторов. Андреас Россберг, показал как обойтись без такого расслоения, сделать модули first class citizens, и при этом не выйти за рамки System Fω, не потерять разрешимости тайп-чекинга и весьма сильного автовыведения типов, не смотря на довольно сильный сабтайпинг. Конечно знать бы заранее, SML надо было бы основывать именно на этом подходе, он во сто крат элегантнее.

С другой стороны, подход к прозрачности/инкапсуляции в модулях тут ad hoc'овый, в то время как Конор МакБрайд (https://pigworker.wordpress.com/2015/01/05/linear-dependent-types/) показал, как надо. Просто в модулях (они же контексты) поля надо аннотировать элементами моноида {0, 1, *}, 0 это proof-irrelevant-поля, это те самые opaque-поля, значение которых мы не можем смотреть в рантайме, программа относительно них таким образом заведомо параметрично-полиморфна. Элемент * означает, что значение поля можно использовать сколько угодно раз, это как обычно. А вот значение 1, означает что элемент можно использовать ровно один раз, это позволяет представлять resources/entities.

Польза "ООП" в рамках функциональных языков программирования сводится именно к поддержке вот такого синтаксического сахара (не выходяшего за рамки подлежащего исчисления, напр. System Fω), позволяющего удобно описывать тайпклассы и алгебраические структуры более общего вида. Единственное, из соображений того самого удобства, хочется поддержки наследования (не дублировать определения кольца в определении поля) и номинального сабтайпинга (язык должен понимать, что поле это тоже кольцо, раз мы одно от другого унаследовали). Особенно их хочется, когда начинаешь пользоваться орнаментами...
ДР Цертуса 2011

(no subject)

Реакт в мильон раз элегантнее, но angular ui содержит столько готовых компонентов, что просто невозможно соскочить с этой иглы. :(
Свечка и валокардин

Только в Гёттингене

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


P.S. Тут и в Швейцарии я уже встречал слинги самых разных стилей — строгие, гламурные, хипповые, хипстерские, нердские.. Проф. П. носила дитя в слинге строгой окраски, подходившем к костюму, постдок Р. в слинге с уравнениями из своей области и xkcd 55. Но вот чОрная ткань с черепом и костями — это что-то новенькое.
ДР Цертуса 2011

Ссылочное

Случайно встретил очень элегантное рекуррентное доказательство иррациональности числа π, оно занимает девять строк, читается за две минуты и доступно для понимания увлечённого математикой девятиклассника — там в одном месте интегрируется по частям несложное тригонометрическое выражение, а всё остальное вообще элементарно.

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

http://arxiv.org/pdf/0911.1933v1.pdf
ДР Цертуса 2011

UK

Прибыл. Великобритания уникально сочетает элегантность с кондовостью, по стилю и уровню благоустроенности на первый вгляд очень похожа на Швейцарию. Только машины неправильно ездять, что несколько дизориентирует по-началу. В автобусе из Стенстеда (аэропорта) на Liverpool street есть WLAN, что очень приятно.
ДР Цертуса 2011

Свежие зарисовки

Он: Мускулист, нагеленная прическа, открытое лицо. На крутом красном горном велосипеде, сверкающем дисковыми тормозами. Аккуратнен, выбрит, летняя рубашка, не застёгнутая на две верхних пуговицы, длинные шорты. Лет 20.

Она: Темно-синие чуть расклешенные джинсы, элегантные туфли на небольшом каблуке, светлая блузка, черный жакет очень идущий к джинсам. Чуть ниже среднего роста, смуглая кожа, зелёные глаза, сочные каштановые волосы. Резные черты лица, прямой, благородно выдающийся вперёд нос. Лицо по-детски свежее. Лет 19.

Их разделяет две полосы дороги. Светофор красный.

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

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

А у меня в плеере играет La Danza Neapolitana. :-)
Я бы на их месте сделал то же самое. А Вы?
ДР Цертуса 2011

Пример кода на Dyi.


###
# Это пример кода на  языке программирования, 
# разработкой которого я  занимаюсь последние
# несколько лет. Особое спасибо Саше Темереву
# (lj user=Sorhed) за помощь в создании 
# прозрачного и элегантного синтаксиса.
#
# Очень прошу всех,  читающих  этот текст, 
# оценить, насколько он понятен, насколько
# легко или трудно читается,  сказать, что
# бы Вы хотели тут изменить!
#
#    С уважением, Александр Куклев.
...

# Предпологается, что где-то выше определены 
# точки а, b и p, стиль basestyle и 
# дискриптор сервера погоды weatherServer .

# Определим прямую через точки a и b .

[ l := прямая-через: Точку a :и: Точку b. ]

Collapse )