Похоже, злая рыба осетрина меня таки во мраке догнала, в смысле началась сезонная аллергия в Испании. Глядя на календарь и во двор (добрые застройщики насажали под окнами десяток берез), это скорее тимофеевка. На антигистаминах обычно указывают побочным эффектом сонливость, но таков же и эффект самого поллиноза.
Всегда удивляло словосочетание animal husbandry, чудились в нем некие нотки хтонических культов скотоложества. Утверждают, что husband ранее означало главного домообитателя, который уже в свою очередь имел в своем распоряжении жену, скот и прочую утварь. Видимо, если до этого слова еще не добрались политкорректоры, то это вопрос времени.
Придумал название для кулинарного шоу про низы общества: "Деглясированный элемент"
Martín Hötzel Escardó (21:49)
I don't agree that set theory is assembly. Assembly has a well defined semantics (telling you what each instruction does). Set theory is more like bit-streams. Everything is a bit-stream in the computer. But the semantics of bit-streams is outside the realm of bit-streams (this bit stream is a program, this bit stream is a jpg file encoding an image, this bit stream is somehow coding a complex number). Similarly, the "semantics" of sets (this is the set encoding the number 17, this is the set encoding the sine function, this is the set encoding the free group on one generator, this is the set encoding the monster group, this is the class encoding the category of groups) is completely outside set theory. You can't answer the question "what is the free group on one generator" by pointing to a particular set. You also have to explain (outside set theory) how everything is encoded. In type theory there is much less encoding. In particular, the definition of "the" type of natural numbers is closer to a universal property than to any accidental encoding as the ones one encounters in (the practice of) set theory. And the same goes for functions, for pairs, and much more. Set theory is less than assembly.
Новость о смерти Крылова залетела нехорошей мухой в голову с утра, сбивала с толку целый день, а под вечер окончательно испортила настроение. Кажется, будто дурное межвременье доедает остатки молодости.
Придумал загадку: что общего между сепарационной логикой и 3D-играми? Присылайте ваши ответы в редакцию.
Forwarded from Alex Gryzlov
в общем моя интуиция заключается в том что для завтипов по ряду причин (тотальность, индексы) ленивость слишком крупнозернистый инструмент, нужно ее разбирать на составляющие - кодату, линейность и тд
Chirimar, Gunter, Riecke, "Reference Counting as a Computational Interpretation of Linear Logic"
Analogs to the
Analogs to the
store and fetch operations are the delay and force operations that appear in any functional programming languages. In such languages, the delay primitive postpones the evaluation of a term until it is supplied to the force primitive as an argument. When this happens, the value of the delayed term is computed, returned, and memoized for any other applications of force. Abramsky has argued that this is a natural way to view the operational semantics of the store and fetch operations of LL; we will follow this approach as well.https://www.epatters.org/assets/thesis.pdf Patterson, "The algebra and machine representation of statistical models"
Сегодня ночью допилил на идрисе майкбрайдовский ко-де-Брёйн в интерпретации Dan Doel (ссылки в ридми): https://github.com/clayrat/PRSA/tree/master/src/Somewhere
Суть идеи - натянуть линейное обращение с переменными назад на интуиционистскую лямбду. Т.е., отталкиваемся от того факта, что в линейной логике стартовый секвент это
Профит от этой штуки не совсем понятен, но например hereditary substitution становится структурно-рекурсивным, что для тотальных языков всегда вин. В целом МакБрайд намекает на более эффективные и удобные тайпчекеры для пруверов.
Суть идеи - натянуть линейное обращение с переменными назад на интуиционистскую лямбду. Т.е., отталкиваемся от того факта, что в линейной логике стартовый секвент это
A ⊢ A: конструкторы переменных не несут никакой дополнительной структурной информации, а только сигнализируют о том, что у нас в контексте единственная формула, которую мы и берем. Тогда нам нужно размазать weakening/contraction по остальным правилам, т.е., каждая лямбда должна сразу знать, используется ли её аргумент или нет, и каждая аппликация должна говорить, как распределены переменные между функцией и аргументом. По ходу дела оказывается, что мы попадаем в волшебный мир топосов Шануэля aka Клейсли-категорию свободных алгебр над монадкой включений. Все эти страшные слова означают тот факт, что мы по сути везде таскаем связку, показывающую как ослабить контекст до требуемого.Профит от этой штуки не совсем понятен, но например hereditary substitution становится структурно-рекурсивным, что для тотальных языков всегда вин. В целом МакБрайд намекает на более эффективные и удобные тайпчекеры для пруверов.
GitHub
PRSA/src/Somewhere at master · clayrat/PRSA
Proof-relevant separation algebras from Rouvoet et al - clayrat/PRSA
Покатался на велосипеде первый раз за три месяца. На улице приятно, жара схлынула, везде куча народу - бегуны, велосипедисты, дети, старички. Многие зачем-то в масках.
TIL что старый анекдот про котлы в аду на самом деле про крабов: https://ru.wikipedia.org/wiki/%D0%9C%D0%B5%D0%BD%D1%82%D0%B0%D0%BB%D0%B8%D1%82%D0%B5%D1%82_%D0%BA%D1%80%D0%B0%D0%B1%D0%B0
Wikipedia
Менталитет краба
разновидность эгоистичного поведения
Если кому-то интересно, как выглядит каррирование и кокаррирование на секвенциях, то вот https://gist.github.com/clayrat/f5a49ee9976eb361868523ed3fed2ff5
Gist
system L with subtractions
system L with subtractions. GitHub Gist: instantly share code, notes, and snippets.
https://core.ac.uk/download/pdf/82119988.pdf van Glabbeek, "On the expressiveness of higher dimensional automata"