Category: история

Category was added automatically. Read all entries about "история".

ДР Цертуса 2011

(no subject)

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

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

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

Поликатегории, *-автономные категории, симметричные моноиадльно-замкнутые категории

Упоминавшаяся вчера статья Майка Шульмана, кстати, огонь! (https://arxiv.org/pdf/2004.08487.pdf)

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

С стороны логики месседж такой: мультипликативно-аддитивная (т.е. без экспоненциальных модальностей) линейная логика без 0 и ⊤ консервативна над аналогичной интуиционистской линейной логикой без 0.

Есть такой очень естественный с категорной и вычислительной (теоретико-типовой) точки зрения фрагмент линейной логики — интуиционистская линейная логика: _⊗_, 1, _⊸_, _&_, _⊕_. Вот обычная интуиционистская логика моделируется в декартово-замкнутой категории (где требуется наличие конечных сопроизведений, чтоб была дизъюнкция), а что будет если взять симметричную моноидально-замкнутую категорию? Вот в ней как раз интуиционистская линейная логика живёт. Естественный вопрос — насколько она слабее “классической” линейной логики, где всё симметричненько? Ну и вот ответ, что если без 0, то нинасколько. А если с 0, то слабее, потому как наличие нуля это в точности то, что позволяет закодировать оператор «не», который ведёт себя в классической и в интуиционистской логике по-разному, это известный результат Шеллинкса 1991 года.
ДР Цертуса 2011

Карри-Говард для FOL

Как все тут знают, по соответствию Карри-Говарда интуиционистской логике высказываний (логике нулевого порядка) соотведствует просто-типизированное лямбда-исчисление с произведениями STLC.

Утверждениям в логике соответствуют типы в STLC, доказательствам утверждений — термы соответствующих типов. У STLC с произведениями есть прекрасная категорная семантика — декартово-замкнутые категории.

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

То есть тут у нас есть такие сущности:
– Типы элементов (например, скаляров и векторов), они образуют категорию с конечными (декартовыми) произведениями. Среди них выделенный тип “1” — нейтральный элемент произведений. Назовём эту категорию T, и в ней особо выделим проекции X ↠ Y (морфизмы, которые выделяют из произведения A × B ×···× D подпроизведение, скажем, B × C, и, опционально, меняют порядок аргументов).
– Типы предикатов P(x : T), где T какой-то тип элементов. Отношения суть предикаты на произведении нескольких элементарных типов отношений, например Id(p : T × T), а обыкновенные высказывания суть предикаты на 1. Если мы хотим чтобы у нас была логика первого порядка с равенством, то как раз постулируется что для каждого типа элементов автоматически есть предикат Id(x : T, y : T).
– Мы хотим, чтобы совокупность предикатов над одним и тем же типом была реализацией логики высказываний (т.е. категория предикатов над T была декартово замкнутой)
– Мы хотим, чтобы каждая проекция в категории элементов X ↠ Y порождала контравариантный функтор между категориями предикатов над Y и предиктов над X (это значит мы можем менять местами переменные у предикатов и добавлять переменные, которые никак не используются), сохраняющий структуру декартовой замкнутости.
— Далее мы хотим, чтобы у нас были кванторы — функторы сопряженные с вложениями слева и справа, соответственно предикаты P(x : X, y : Y) в предикаты (∀x,P)(y : Y) и (∃y,P)(y : Y). То есть мы уменьшаем количество переменных (можем уменьшить и до нуля, тогда получатся предикаты над единицей, то есть высказывания), замыкая убираемые переменные квантором всеобщности или существования.

Вот собственно и вся категорная семантика FOL, называются такие штуковины гипердоктринами (или, соответственно гипердоктринами с равенством, если требуются id-типы). Привожу определение по Pierre Clairambault, “From Categories with Families to Locally Cartesian Closed Categories”:

Screen Shot 2019-07-30 at 15.03.07

А вообще это классика, R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für math. Logik und Grundlagen der Math., Band 29, 505-542 (1983).
ДР Цертуса 2011

Литобзор

Математикам и сочувствующим рекомендую прекрасную обзорную статью Даниэля Грейсона на 28 страниц и приблизительно час чтения: «An introduction to univalent foundations for mathematicians» (arXiv:1711.01477).

Сразу после этой статьи, чтобы разобраться с тем, что как же именно устроена аксиома унивалентности, очень рекомендую ещё и совсем короткую (9 страниц, полчаса вдумчивого чтения) статью Мартина Эскардо «A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom».


Пара критических замечаний:
– В статье про унивалентность не хватает, на мой взгляд, упоминания того факта, что унивалентность следует из короткого (5 штук) набора “технических” свойств структурного равенства типов, см. статью «Axioms for univalence» (Ian Orton and Andrew Pitts).
– В статье Грейсона вместо типа утверждений возникает иерархия типов утверждений Propi, а вместо типа Group всех групп возникает на самом деле иерархия типов Groupi, и это как-то коробит. В этом месте нехило бы рассказать про то, что существует непротиворечивое расширение MLTT (Predicative Calculus of Cumulative Inductive Constructions), в котором вместо Propi имеется “настоящий” тип всех утверждений Prop (в котором живут типы-утвержения изо всех вселенных сразу) и можно определить полиморфный тип Group всех групп, причём любое доказательство, которое делается для конкретного Groupi, но нигде не использует i, доказывает утверждение для всего типа Group в целом.
ДР Цертуса 2011

Вопрос

Меня вот уже который раз спрашивают: что бы почитать такого по истории современного Израиля (с 1881 и особенно 1919 до наших дней), чтобы не совсем сухо и не совсем пропаганда (и совсем не антипропаганда)? В идеале, по-английски, но можно и по-русски. Какую-нибудь книжку или несколько книжек хороших никто не может посоветовать?
ДР Цертуса 2011

Cedille: Полиморфное лямбда-исчисление с выводимой индукцией

Некоторое время назад Aaron Stump сотоварищи предложил интересный вариант полиморфного лямбда-исчисления, где существуют кодировки широчайшего класса индуктивных типов данных, для которых выводима индукция. В этом посте я хотел обрисовать идеи его подхода.Collapse )
ДР Цертуса 2011

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

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

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

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

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

Отца не стало

Отца не стало. Полчаса назад. Мы были рядом.

Он два года боролся с раком лёгких.

Куклев Евгений Иванович, 31.12.1961 – 17.04.2017 (55 лет).
ДР Цертуса 2011

Занимательный препринт

Эрик Финстер сотоварищи охарактеризовали слабые ω-категории в терминах их внутреннего языка. Очень симпатичный препринт «A Type-Theoretical Definition of Weak ω-Categories (Eric Finster, Samuel Mimram)», и не менее симпатичная онлайн-имплементация языка.

Препринт быстро и легко читается (12 страниц).
Красиво описана конструкция внутреннего языка многомерного обобщения направленных графов (глобулярной теории типов), показано что синтаксическая модель этой теории типов суть категория конечных глобулярных множеств, объяснено почему теоретико-множественная модель суть категория глобулярных множеств.
На базе этого подхода уже строится алгебраическое определение ω-группоидов (аналогичное подходу Брунери) и ω-категорий (идейно эквивалентное определению Гротендика-Малтсиниотиса).
Работа не вполне закончена в том смысле, что доказательство эквивалентности определению Малтсиниотиса пока не приведено.
ДР Цертуса 2011

Сужение мира

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

В самом начале 19-го века, в 1803 году совершил первое плаванье параход Charlotte Dundas, первое в мире применимое на практике транспортное средство на механической тяге. В мае 1952 года реактивные авиалайнеры начали на ежедневной основе доставлять пассажиров через Атлантику. Дорога между двумя любыми населёнными пунктами сократилась приблизительно до суток.

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