Category: животные

Category was added automatically. Read all entries about "животные".

ДР Цертуса 2011

(no subject)

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

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

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

У чёрного медведя

Ресторан «У чёрного медведя» открылся, когда Гёттинген ещё был членом Ганзейского союза (или только-только вышел из него), Иван Грозный был (первым) всероссийским государем, Елизавета I превращала Англию в великую морскую державу, а Шекспир писал свои основные произведения. И проработал до 2011 года. Я там был, мёд-пиво пил, и было очень вкусно. А потом закрылся он на масштабный ремонт.

Прежние его операторы, муж и жена Бутц, стали стары, и владелец — Айнбекская пивоварня — продал здание пожилому богатому инвестору, который планировал инвестировать миллионы евро и провести очень глубокий и качественный ремонт-реставрацию здания, в частности возвращение части помещений исторического вида, и переделку бесхозного сводчатого подвала XIV-го века в публичное помещение. А потом инвестор умер.

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

Грустьпечаль какая-то.
ДР Цертуса 2011

Обувное

Вангую, что сандали будущего будут состоять из одной подошвы, прилипающей к стопе электро-отключаемым механизмом по типу присосок геккона. Одна тонкая дышащая (потовпитывющая и поторассеивающая) подошва с маленькой кнопкой «отцепиться от ноги». В барефутерском варианте ещё и очень тонкая и гибкая, чтобы идеально чувствовать ногой поверхность — чисто защита ноги от грязи, уколов, порезов, мозолей и экстремальных температур. Очень приятный и безвредный тип обуви будет.
ДР Цертуса 2011

Ещё кухонное

А ещё в каком-то отдалённом будущем я таки хочу проапгредйдить раковину измельчителем мусора. Мне пока больше всего нравится (сертифицированный для Германии, что редкость) InSinkErator Evolution 200. Потому что тихий и мощный. Только дорогой, собака.

Кстати, гулял по их сайту, встретил их бестолковый кран с кипятком. И вспомнил, что где-то в другом месте мне встречался такой дополнительный кран в раковину с пятью кнопками: крутой кипяток, горячая вода для заваривания зелёного чая, охлаждённая вода, охлаждённая вода с газом, обычная вода с газом. Такая помесь проточного нагревателя с проточным охладителем и сифоном для газирования воды; только оно ещё и воду берёт из водопровода, по дороге убирая оттуда кальций и хлорирующие агенты. Сходу не нашёл.
ДР Цертуса 2011

Как же до меня медленно доходит!

Как до жирафа. Всего-то лет десять прошло. В общем я о том, что translucent modules это “виртуальный” uncurrying тайпклассов.

Давайте работать в терминах предикативного λωΠΣW-исчисления, без каких либо предположений о существовании вселенных. Т.е. у нас как термы, так и типы могут быть зависимы как от термов, так и от типов, однако мы не смешиваем термы и типы, как это принято в традиции MLTT, благодаря тому что там подразумевается, что вселенные у нас есть.

Если у нас есть обыкновенный зависимый тип навроде Fin[n : Nat], то функцию f типа
Π(n : Nat).Π(m : Fin[m]).R никто не мешает оформить как f : Π(x : BoundedNat).R, где BoundedNat := Σ(bound : Nat).Fin[bound].

Вот и когда у нас есть зависимый от типов тип навроде Order[T] и полиморфная функция f : ∀(T).Π(o : Order[T]).R, мы хотим иметь возможность эквивалентно написать f : Π(x : Ordered).R, где Ordered что-то вроде Σ(T).Order[T], при в терминах Σ-типов мы это выразить не можем, T не терм, а тип. В MLTT мы можем аппроксимировать этот тип через U-Ordered := Σ(T : U).Order[T], где U — какая-нибудь вселенная, однако в этом случае мы фиксируем вселенную перед определением функции, и таким образом теряем требование, чтобы функция была параметрически полиморфна по T.

Отметим, что в MLTT сигнатура Π(T : U).Π(o : Order[T]).R гарантирует параметрическую полиморфность благодаря тому, что т.е. вселенные в MLTT не имеют элиминаторов и синтаксически невозможно написать неполиморфную функцию такой сигнатуры; однако двойственная ей через uncurrying сигнатура Π(x : U-Ordered).R уже ничего такого не гарантирует.

Так вот translucent modules, они же “records with abstract type members” это такой синтаксический сахар, который позволяет нам жить и писать так, как будто бы uncurrying для ∀(X).Y[X] существовал, получается такой специальный “рекорд” (X : ∗, y : Y[X]), в котором поле X такое специальное, что честной проекции на него не существует, но мы тщательно делаем вид, что она существует при помощи path dependent types (т.е. записей вида o.X), только ведёт себя не как все нормальные отображения, а как-то особенно хитро, на самом деле в точности так, чтобы "λo : (X : ∗, y : Y[X]). blablabla o.X blablabla" всегда можно было desugar'нуть в “Λ(X : ∗).λ(y : Y[X]). blablabla X blablabla”.

Семантически транслюсцентный модуль (рекорд с одним или несколькими абстрактными полями) следует понимать как типозависимый тип (тайпкласс) R[T1 T2 .. Tn : ∗], просто представленный синтаксически нетривиальным образом. В языках с развитой системой модулей, абстрактные поля могут иметь не только тип Type, но и тип иного транслюсцентного модуля, скажем M := (O : Ordered, x : X[O.Carrier],..), всё спокойно это дешугарится в вышеописанную схему, просто M[T : ∗] := (order : Order[T], x : X[T],..), в процессе, правда, возникнут higher kinded parameters, если тип абстрактного поля сам был параметризован. Функции, возвращающие translucent module после дешугаринга возвращают просто параметризованный одним или несколькими типами рекорд, т.е. f : X -> (∀(T).M[T]), функции, принимающие translucent module дешугарятся в полиморфные: f : (l : List) -> List.Item превращается в f : ∀(T). List[T] -> T. После такого дешугаринга можно заменить все ∀(T) на Π(T : U) без потери строгости, вот и всё. (Насколько я понимаю, higher kinded ∀'s тоже заменяются на Π's без потери строгости, хотя это совсем не элементарный результат.) Вот и ответ на мой вопрос про семантику сложных структур из прошлого поста.

А, да, про системы модулей в языках с отношением subtyping'а: указание верхних и нижних границ можно рассматривать на уровне семантики как дополнительные поля рекорда, обеспечивающие конверсию в/из абстрактного параметра T из/в указанной границы. И всё работает.
ДР Цертуса 2011

Теоретико-множественные основания теорката

На протяжении 20-го века основным языком классической математики была система NBG (von Neumann-Gödel-Bernays). Теоретико-множественная часть системы NBG называется теорией множеств Цермело-Френкеля с аксиомой выбора (ZFC), разница между ними в том, что на языке ZFC можно говорить только о множествах, и нету грамматического оборота, позволяющего сказать, например, "для всех групп G". А вот NBG это система, где можно определять классы, например всех множеств Set, всех групп Grp, всех колец Rng, при этом она является консервативным расширением ZFC, т.е. все вещи, которые в ней можно доказать "для всех групп Grp" это в точности те же вещи, которые можно доказать про группы в ZFC. Конечно же на языке NBG можно говорить и о таких алгебраических структурах как категории, о классе Cat множеств со структурой категории.

Однако в Cat не входит "категория всех групп", т.к. Grp не множество, я в Cat входят только множества со структурой категории. Зато мы можем отдельно рассматривать два разных понятия,
1) конкретные категории: Классы со структурой категории: Grp, Rng,..
2) малые категории: элементы Cat

На практике от этого получается большая беда, для малых категорий мы можем доказывать общие результаты, скажем "для всякой категории С верно то-то" и производить общие построения, "для всякой категории C мы можем построить Скелет C, Нерв C" и т.д. Но применить эти результаты к большим конкретным категориям навроде Grp мы вообще говоря не можем.

В поисках решения этого вопроса Гротендик придумал понятие иерархии вселенных. Вселенная (Гротендика) это такое множество U, очень похожее на класс всех множеств Set (похожесть выражается в замкнутости относительно базовых тайп-формеров, см. http://en.wikipedia.org/wiki/Grothendieck_universe), но без требования что все другие множества в него входят, в частности U ∉ U. Вместо этого требуется, чтобы для каждого множества s ∈ Set существовала какая-нибудь вселенная U ∋ с. В частности, это означает, что для начиная с любой вселенной U можно построить иерархию U ∈ U' ∈ U'' ∈ ···.
Дальше вместо того чтобы что-то доказывать для (больших) конкретных категорий Grp, Rng и т.п., проводят доказательства для их "усечённых до U" подкатегорий GrpU, RngU. Жить так безусловно можно. Но таскать за собой индексы U в каждой формуле, а впереди каждого высказывания писать "для любой достаточно большой вселенной U" муторно и неэлегантно. (Хотя в Agda так сейчас и живут!)

Решение этого вопроса предлагает теория множеств (strong) ZFC/s Соломона Фефермана: это обычная ZFC/NBG, дополненная постулатом о существовании как минимум одной вселенной Гротендика и схемой генерализации: если мы доказали высказывание pU усечённое до той или иной вселенной U, причём U входит в высказывание только на уровне типов (т.е. связывает свободные переменные), но не термов (это называется proof irrelevance), то автоматически вернен неусечённый вариант p. Отметим, что отдельно постулировать иерархию вселенных не нужно, из определения вселенной и схемы генерализации автоматически следует, что для каждого s ∈ Set существует какая-нибудь вселенная U ∋ с.

Не смотря на то, что сам Феферман недоволен результатом и последние сорок лет периодически возвращается к вопросу о том, как бы вообще обойтись без понятия вселенной при формализации теорката, сами категорные теоретики вполне довольны этим подходом, см. https://golem.ph.utexas.edu/category/2009/11/feferman_set_theory.html, а вопрос детальной работы со вселенными Гротендика, как выяснилось, имеет полезные прикладные стороны как в логике (в отросли интуиционистских теорий типов), так и за её пределами (inter-universal Teichmüller Theory).

Мне же этот вопрос интересен в смысле того, как обращаться со вселенными в функциональных языках программирования и Theorem Prover'ах на базе теорий типов. Думается мне, что будущее за подходом Фефермана, а не за постулированием иерархий вселенных в явном виде.
ДР Цертуса 2011

Принтерное

Размышлял над тем, не завести ли всё-таки домой принтер. Хочется конечно аппарат со сканером, цветной, лазерный, чтоб минимум 1200 dpi в каждом направлении, со стоимостью расходников в пределах 10 центов за страницу и толерантностью к многомесячному простою. Плюс чтоб печатал на любой бумаге (и самой дешевой рецайклинговой и толстой мелованой для грамот) По этим ограничениям находится примерно вот такой аппарат: EPSON ACULASER™ CX17NF. Это лазерный LED-принтер (мало движущихся частей, жить должен почти вечно), честные 1200х2400 dpi, отличные чёткие буквы, отличная цветная печать. И бонус в виде дуплекса. Стоимость расходников от 7 до 10 центов на страницу.
Весьма компактных размеров для МФУ с дуплексом: 41см × 40см × 35см
Стоит 350 евро.

Но что-ж они собаки такие фигуристые? Пылесборник же страшный. Отчего нельзя делать МФУ-принтеры в формфакторе закрытого кирпича как Сanon PIXMA (MG3220 и др. модели) или Brother J4510DW


В обоих под крышкой сканер, во втором в крышку ещё встроен проточный сканер, и дуплекс во втором тоже имеется. Кстати, рекордсмен по компактности среди дуплексных МФУ Brother J470DW: 41см × 37см × 18см, ума не приложу как они всё туда засунули.

(Пост проапдейчен в соответствии с комментариями, tnx eta_ta.)
ДР Цертуса 2011

Очень-очень интересно!

В предикативных типизированных исчислениях построений встречаются много разных способов определять типы, самый универсальный предикативный (т.е. избегающей неразрешимой рекурсии) известный на сегодня способ определять типы — расслоенные индуктивно-рекурсивные определения, таким образом можно определять не только индексированные контейнеры (эквивалентно: индуктивные семейства типов), их зависимые суммы и произведения, но и вселенные (типы типов), замкнутые относительно построения в них индексированных контейнеров, зависимых сумм и произведений. В общем это такой зверь, которого достаточно для всех известных применений, не считая высших типов. Именно индуктивно-рекурсивно (и заведомо только так) можно построить модель зависимо-типизированного языка в нём самом, т.е. пару из зависимого типа Expr[T] (валидное выражение языка типа T) и функции execute: Expr[T] => T.

Ничего нормального для высших типов на эту тему ещё не изобрели, в частности в HoTT стоит адова проблема построения симплициалных типов (это важно потому что показано, что если в HoTT можно смоделировать её саму, то с необходимостью можно сэмулировать и симплициальные типы). С другой стороны, с колокольни HoTT вообще непонятно, как могут строиться в одномерной теории вселенные типов, доказано что уважающая унивалентность вселенная n-типов в HoTT неизбежно имеет h-уровень больше n. То есть понятно, что индукция-рекурсия очень поверхностно совместима с HoTT, унивалентных вселенных так не построишь, да и другие интересности получаются неэквивариантными.

В недавней статье Neil Ghani et al. вводят очень интересную (красивую с категорной точки зрения) положительную индукцию-рекурсию: https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/papers/positive_calco2013.pdf.
Крайне интересным образом, вселенная, замкнутая относительно построения П-типов, методами IR+ не получишь, однако можно получить группоид, обладающий нужными свойствами, это как раз то что в HoTT должно получиться. Наверняка за этим делом скрывается обобщение – некая высшая положительная индукция-рекурсия HIR+, методами которой можно как раз получать всякие там симплициальные типы.
ДР Цертуса 2011

«Кто подобен зверю сему? И кто может сразиться с ним?»

Понравилась метафора у Лемуры, http://lemura.livejournal.com/209580.html:
Самая страшная для меня книга — это учебник социальной психологии.
А самая страшная нечисть — это безголовая курица.

Потому что дракона можно убить, в упыря вогнать серебряную пулю или осиновый кол, назгула сообразить на двоих с полуросликом — но что ты сделаешь с безголовой курицей, когда она несется на тебя с добрыми намерениями и воплем: “Ааааа бежать, спасать, гуманитарку слать — там голодают от рака дети!”
И не проверит такая курица ни кому она помогает, ни правда ли там дети, ни как распределяется эта гуманитарка...