Covalue

Следующая лекция по теориям типов (STLC и System T) пройдет в среду 5 августа, в то же время (19:00 CEST/UTC+2 / 20:00 MSK).

Первая лекция через час, зум-ссылка в календаре.

Онлайн-курс «Современные теории типов»

В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с летними пропусками). Начнём с обзора формальных языков и алгебраических теорий и пойдём до самого фронтира синтетических и направленных теорий типов. Примерная программа:

1. Вводная лекция
2. Языки и алгебраические теории
3. STLC и System T
4. PCF
5. System F и Fω
6. Зависимо-типизированные языки
7. Индукция
8. Рефайнмент- и фактор-типы
9. Эффекты в типах
10. HoTT
11. OTT/CuTT
12. □-полиморфизм
13. Модальные типы
14. Охраняемая рекурсия
15. Когезивные модальности
16. Направленные и симплициальные теории

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

Ссылка на гугл-календарь, где будем публиковать даты лекций:
https://calendar.google.com/calendar/u/0?cid=YzdkMGI0MTdlZjFiMTg1OGVmNzUyYjFkZjBjYjYwZjBhYTI0MGExNjlhMWVhZGY5OTcyOGYwOTM4OTVlMDliM0Bncm91cC5jYWxlbmRhci5nb29nbGUuY29t

Начинаем

Сегодня в 12:30 UTC (через ~2 часа) планирую постримить формализацию понятия рефлексивных графов.

Начинаем

Сегодня в 12:45 UTC (через ~2.5 часа) планирую постримить на ютюб-канале формализацию Symmetry Book на кубических типах.

Формализация краткого вывода закона исключенного третьего из аксиомы выбора (узнал от Валерия Исаева):

https://gist.github.com/clayrat/80f2e048831e6829a49d5cb3843b2c7d

Начинаем

Сегодня в 12:00 UTC (через ~1.5 часа) планирую постримить разбор PoC компилятора в пучки.

Начинаем

Сегодня в 12:00 UTC (через 2.5 часа) планирую постримить разбор статьи о программировании на полиномиальных функторах.

Начали

Сегодня в 12:30 UTC (через 1.5 часа) планирую постримить на ютюб-канале разбор диалоговой семантики и вайб-кодинг солвера на её основе. Подключайтесь, кому интересно!

Grandury, Nanevski, Gryzlov, [2025] "Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach"

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

В теории типов наиболее общим представлением ориентированного графа обычно полагается функция A → A → U, где A — тип вершин графа, а U — вселенная («тип типов»), то есть гомогенный бинарный предикат. Используя классическую эквивалентность (см. например HoTT book, 4.8.3) ∑[T:U] (T → A) ≃ (A → U), мы можем трансформировать определение графа в пару { edge : A → U, adj : (from : A) → edge from → A }, то есть в представление в виде adjacency map, которое сопоставляет исходным вершинам рёберные конструкции и умеет по ним извлекать конечную вершину. Специализируя эту конструкцию под конечные графы и структуры данных, мы получаем из неё классические представления adjacency matrix/list.

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

В классической сепарационной логике рассматривается в первую очередь PCM куч (heaps). Как только у нас появился второй PCM, мы можем рассмотреть отображения (морфизмы) между ними, а также эндоморфизмы над самими графами. Морфизм в данном случае это функция, сохраняющая моноидальную операцию, f(γ₁∙γ₂) = fγ₁∙fγ₂. Это позволяет распространить концепцию фрейминга (framing) на графы - в статье мы называем это "контекстной локализацией" (contextual localization). Другими словами, морфизмы позволяют вычленить кусок графа, произвести над ним некоторое действие, и затем автоматически склеить его с незатронутой оставшейся частью, что сильно упрощает ряд доказательств. Морфизмами, в частности, являются высокоуровневые комбинаторы над кодировкой графов как конечных отображений - map, filter, а также более ad-hoc функции вроде взятия множеств конечных вершин sinks. Достижимость (reachability) в графе сама по себе морфизмом не является, но удобно взаимодействует с морфизмом filter, что позволяет "вырезать" фрагменты из достижимых компонент.

Весь этот аппарат мы используем для создания библиотеки работы с графами в Hoare Type Theory, и построения двух формальных доказательств для императивных алгоритмов Шорра-Уэйта (разметка бинарного графа, где стек обхода хранится в самом графе через инверсию рёбер, без выделения отдельной памяти) и union-find (построение непересекающихся классов эквивалентности). Доказательства получились достаточно компактными (110 строк для Шорра-Уэйта, 49 для union-find).

Ограничение описанной техники вытекает из исходной идеи - она естественна для алгоритмов, исследующих граф, следуя по ребрам. Для алгоритмов, работающих с ребрами более "глобально" (например, алгоритм Краскала), скорее всего, потребуются другие представления.

#paper #separationlogic

Выложили запись доклада: https://www.youtube.com/watch?v=IkTimIZUCgg

Piecha, [2013] "Three Lectures on Dialogues"

Три лекции по диалоговой семантике интуиционистской логики. Диалоговая семантика - это интерпретация логических формул, придуманная Паулем Лоренценом и его учеником Куно Лоренцем в 1950х годах. Она основана на идее игры между игроком и оппонентом, где валидность формулы определяется как наличие у игрока выигрышной стратегии при любом поведении оппонента. Фактически, это предшественник игровой семантики.

Лекции устроены так:

1. Введение в диалоги Лоренцена для пропозициональной логики: формулы, атаки/защиты, позиции, D-диалоги, стратегии, полнота, классические обобщения.
2. Расширение пропозициональной логики на Хорновские дизъюнкты в стиле логического программирования: E-диалоги, прологовский дефинициональный ризонинг (резолюция + унификация)
3. Альтернативная трактовка импликации и соответствующая ей новая форма E-диалогов, вносящая дополнительную ассиметрию между допустимыми ходами игрока и оппонента.

Нашел качественную диссертацию с обзором состояния дел в model checking на 2010й год:

Weißenbacher, [2010] "Program Analysis with Interpolants"

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

Концептуально этот подход описывается теорией моделей (одним из двух основных разделов логики, второй - это теория доказательств, на которой основана теория типов и proof assistants). Интересно, что в моделчекинге примерно раз в декаду сменяется доминирующая парадигма, в целом его таймлайн выглядит примерно так:

* 1980е - зарождение самой идеи MC из работ Эдмунда Кларка по вычислению неподвижных точек для систем доказательств в предикат-трансформерах, использование BDD для компактификации состояний
* 1990е - дальнейшее ужатие состояний через partial order reduction, появление предикат-абстракции и CEGAR - методов автоматического конструирования моделей из набора assertions о программе
* 2000е - SAT/SMT-революция и уход от BDD, быстрая аппроксимация через интерполяцию Крейга
* 2010е - Аарон Брэдли изобретает семейство алгоритмов PDR (property directed reachability), где процесс построения инварианта чередуется и взаимодействует с построением контрпримера, взаимно усекая соответствующие пространства поиска
* 2020е - ажиотаж вокруг техник из машинного обучения

Первые три декады и основные их идеи расписаны в первых двух с половиной главах диссертации (вторая половина третьей и четвертая главы более технические).

#automatedreasoning

Ссылки с последнего слайда:

* B. Stroustrup: 21st century C++ Blog@CACM January 2025
* C++ Core Guidelines
* Profiles
** B. Stroustrup: Safety Profiles: Type-and-resource Safe programming in ISO Standard C++
** B. Stroustrup: Profiles syntax
** B. Stroustrup: Profile invalidation eliminating dangling pointers
** Herb Sutter: Lifetime safety: Preventing common dangling
* Khalil Estell: C++ Exceptions for Smaller Firmware. CppCon 2024
* Daniela Engert: Contemporary C++ in Action. CppCon 2022 a client server application for displaying video frames with timing constraints
* B. Stroustrup: A Tour of C++ (3rd Edition). Addison-Wesley. 2022.
* B. Stroustrup: Programming: Principles and Practice using C++.
* B. Stroustrup's HOPL papers
** A History of C++: 1979-1991. March 1993
** Evolving a language in and for the real world: C++ 1991-2006. June 2007
** Thriving in a Crowded and Changing World: C++ 2006-2020. June 2020