Bornat, [2009] "Separation logic and concurrency"

Программирование это комбинация механических вычислений и формальной логики. Как правило, каждый новый формализм используется программистами для увеличения объема выразимых программ, а не корректности (насчет баланса между выразительностью и непротиворечивостью см также например https://twitter.com/aspiwack/status/1394012829464866819). Многопоточные вычисления - самая сложная разновидность программирования, и тут, как всегда, теория информатики одновременно и плетется за практикой, и обгоняет её.

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

Конкурентная сепарационная логика (CSL) классически занимается safety, т.е. частичной корректностью многопоточной программы относительно спецификации и модели консистентности. Её предшественник это в первую очередь метод Owicki-Gries 70х - расширение аксиоматической логики Хоара на программы с примитивами параллельной композиции и синхронизации, основанное на доказательствах non-interference. Метод OG популяризировал идеи ресурсных инвариантов и вспомогательных (ghost) переменных. В 80х Cliff Jones доработал метод OG до rely-guarantee, добавив два одноименных условия к пред- и постусловиям. Одно из слабых мест обоих методов - работа с алиасингом, т.е. тем фактом, что одна ячейка памяти может индексироваться разными символьными выражениями. Для решения этой проблемы и была придумана сепарационная логика - параллельная ветка развития логики Хоара, где под "сепарацией" понимается двухместный предикат над ячейками, гарантирующий неравенство их адресов. Это позволяет иметь т.н. frame-правило (терминология, кстати, заимствована из ИИ), позволяющее отбрасывать "нерелевантные" логические условия, т.е. работать только с тем состоянием, которое напрямую затрагивается рассматриваемой частью программы.

Как и метод OG, CSL добавляет примитивы параллельной композиции и критических секций вида with r when B do C (для которых подразумевается наличие более низкоуровневой имплементации). r - так называемый ресурс, для каждого из которых в логике вводится свой инвариант (также идея OG). Статья показывает пример доказательств для программ с семафорами, далее переходит к механизму permissions, нужному для отслеживания read-only вспомогательных переменных (существуют альтернативы этому механизму - subjective auxiliary state в FCSL и ghost objects/higher-order ghost code в Iris). Далее демонстрируется доказательство для readers-writer lock (запрет на гонку между чтением и записью) на семафорах, с использованием ghost ticket трюка.

Последняя секция посвящена доказательству для неблокирующего алгоритма 4-slot авторства Hugo Simpson - алгоритм реализует wait-free single-reader single-writer atomic register. Доказательство выполнено "а-ля моделчекинг", с явным перечислением состояний в инварианте. Было бы неплохо иметь алгоритмическую теорию ресурсов, которую мы могли бы использовать в компиляторах, говорит нам статья, и завершается оптимизмом насчет грядущей инкоропорации идей rely-guarantee и темпоральной логики в CSL.

#concurrency

https://github.com/thery/FlocqLecture

Упражнения на работу с действительными числами и плавучкой в Coq с библиотекой Flocq - неравенства, режимы округления, форматы, лемма Стербенца, IEEE754.

#realnumbers

Известная в узких кругах take lemma для конечных списков через обобщенный take_take:

Lemma take_take_min {T} i j (s : seq T) : take i (take j s) = take (minn i j) s.
Proof. by elim: s i j => //= a l IH [|i] [|j] //=; rewrite minnSS IH. Qed.

Lemma take_lemma {T} (p r : seq T) : (forall i, take i p = take i r) <-> p = r.
Proof.
split; last by move=>->.
move=>H; move: (H (size p)) (H (size r)); rewrite !take_size=>{H} Hp Hr.
by rewrite Hp -Hr {2 3}Hp !take_take_min minnAC minnn minnC.
Qed.

https://serokell.io/blog/dependent-types-with-david-christiansen

In this month’s episode of Functional Futures, our guest is David Christiansen, the Executive Director of the Haskell Foundation, a contributor to a number of dependently typed languages, and a dependent type advocate that has managed to introduce many people to the topic today through his work, talks, and texts.

We cover topics such as dependent types, theorem proving, metaprogramming, and many more. We also discuss the book he co-authored with Daniel P. Friedman, The Little Typer, and his current work in progress: Functional Programming in Lean.

Семантика {P}c{Q}:

Хоарова логика:
P s, s -(c)-> s' => Q s'

Сепарационная логика:
P s, safe c s /\ s-(c)->s' => Q s'

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

Исследование представленно в статье в журнале Metaphilosophy.

Также оно кратко освещёно в заметке в Daily Nous.

В этот раз исследователи подвергли кластерному анализу программы подготовки PhD из базы данных The Academic Philosophy Data and Analysis Project, которая ведётся с 2011 года. Всего рассмотрено 129 разных программ (актуальных на лето 2021 года), из которых, к сожалению, лишь 27 реализуются за пределами США. Кластеры составлялись на основе (1) области специализации и (2) ключевых слов, характеризующих образовательную программу. В итоге (для кого-то вполне ожидаемо) получилось, что разделение на аналитическую философию и философию континентальную имеет место, но представляет собой скорее упрощение действительного положения дел. Кластерный анализ даёт наилучшие результаты при выделении 3 кластеров: аналитическая философия (синий цвет на диаграммах, 72 программы), философия науки (фиолетовый цвет, 15 программ) и континентальная философия (жёлтый цвет, 40 программ). Хотя кластер философии науки находится как бы на границе между аналитической философией и философией континентальной, он более тяготеет именно к аналитической философии, и при выделении 2 кластеров сливается с последней.

Кроме того, авторы проанализировали выделение 6 кластеров, что не даёт достаточно хорошего результата при используемом количестве исходных данных. Однако это позволяет выделить в рамках аналитической философии дополнительно к философии науки и собственно аналитической философии (58 программ) кластер (из 14 программ) философии сознания и когнитивных наук, к которым (неожиданно!) примешиваются эстетика и философия религии, что можно считать погрешностью из-за недостаточности исходных данных, а в рамках континентальной философии — собственно континентальную традицию (15 программ), историко-философский и философско-религиозный кластер (17 программ), а также кластер (из 8 программ), связанный с этикой, политической философией и гендерными исследованиями.

Не спрашивайте, почему 72+15+40=127, если заявлено, что исходные данные содержат информацию о 129 программах. Ответ найдёте в разделе 3.1 статьи.

https://arxiv.org/abs/2209.07427 Boruch-Gruszecki, Wasko, Xu, Parreaux, [2022] "A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning"

https://github.com/Linyxus/cdot-calculus

крайняя версия формализации скального DOT calculus на Coq

Davenport, England, Griggio, Sturm, Tinelli, [2020] "Symbolic computation and satisfiability checking"

Небольшое введение в (относительно) современное состояние дел во взаимодействии SAT/SMT-солверов и систем компьютерной алгебры.

https://youtu.be/AaE1mV27XxA

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

Manuell, [2023] "Pointfree topology and constructive mathematics"

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

Так как я теперь работаю с automated reasoning, взялся покопать теорию классических разрешающих процедур. Начать решил с апдейта конструктивного доказательства полноты алгоритма резолюции для классической логики высказываний: https://github.com/clayrat/resolution-ssr/

Спортировал пруфперл Свирстры 2009 года про конструирование Хоаровой монадки на ссрефлект: https://gist.github.com/clayrat/3cab897057ce6a637d87f58950fbea62

Продолжая исследования классических алгоритмов для работы с логиками, портировал пропозициональную интерполяцию с Isabelle на SSReflect: https://github.com/clayrat/resolution-ssr/blob/main/theories/craig_interp.v

Свойство интерполяции было введено Уильямом Крэгом в 1957 году - логическая система обладает им, если для любых двух формул A и B, таких что валидность второй вытекает из валидности первой, можно найти “промежуточную” формулу I, чья валидность вытекает из валидности A и влечет валидность B; при этом все переменные в ней встречаются в обоих исходных формулах (т.е. в качестве I нельзя в общем случае просто взять A или B). Свойство это в дальнейшем было показано для многих логик - пропозициональной, первого порядка, ряда модальных, многосортных и т.д, зачастую конструктивными методами, что и позволяет реализовать процедуру нахождения I в виде алгоритма. Позже также получили ряд результатов для сложности процедуры интерполяции, в частности связь с проблемой P=NP. В 2000х МакМиллан предложил использовать интерполяцию для быстрого приблизительного вывода инвариантов в модел-чекерах, основанных на SAT-солвинге. Подробнее см. слайды D’Silva, [2016] “Interpolation: Theory and Applications”.

Barwick, [2017] "The future of homotopy theory"

Призыв к гомотопистам перестать считать себя топологами, и рассматривать теорию гомотопий как науку о структурных равенствах математических объектов.

Chen, [2022] "A Hoare logic style refinement types formalisation"

Спортировал в этот раз на Идрис, довольно близко к Агде, не считая того факта, что эта-законы для туплов в Идрисе отказываются работать.

Рефайнмент типы, понимаемые как подмножества, т.е. пары (сигмы) из типа и предиката на нем {t ∶ T ∣ P t}, популярны в системах автоматизированных доказательств, но требуют от метатеории телескопических сигнатур функций и механизма для работы с сабтайпингом (ослабление-усиление-преобразование рефайнмента под нужный контекст). Статья рассматривает формализованное на Agda соответствие реф. типов логикам Флойда-Хоара, отображая пред- и постусловия на входные и выходные типы функций. Рассматривается упрощенный вариант лямбда-исчисления с примитивными булями, числами и функциями только первого порядка. Контекст в такой системе распадается на список типизированных переменных и индексированный им список предикатов (соответствующий предусловию); тайпчекинг же соответствует выводу наислабейшего предусловия.

Использование Хоаровского стиля избавляет от телескопических правил и упрощает формализацию системы. Работа с предикатами в статье ручная, через интерпретацию базовых типов в типы Агды, т.е. перед нами эдакий полу-shallow энкодинг. Отделение предикатов от контекста также помогает работать с дополнительными уравнениями, возникающими по ходу разбора программы и не зависящими от ее переменных.

Формализация состоит из четырёх исчислений - 𝜆B (лямбда с функциями первого порядка), 𝜆R (рефайнменты), 𝜆А и 𝜆С. Ключевой момент в 𝜆R - правило для сабтайпинга (усиления постусловия) требующие показать соответствующие импликации (приблизительный аналог consequence правил в логике Хоара). Симметричное правило ослабления предусловия оказывается выводимо внутри системы. Здесь также лежит причина отсутствия функций высшего порядка в статье - для кодирования предикатов на них пришлось бы моделировать полноценную теорию множеств, в духе подхода semantic subtyping (интересно, можно ли обойтись гомотопическими множествами?). Также стоит отметить, что 𝜆R кодируется индуктивно-рекурсивно, через комбинацию правил и функции стирания до 𝜆B, убирающей предикаты и ноды сабтайпинга.

Здравость и полнота 𝜆R доказываются семантически. Тайпчекер (по сути вывод предикатов) для него формулируется через вычисления наислабейшего предусловия, подстановкой интерпретации терма в постусловие. Проблема с таким тайпчекером в том, что он не работает с функциями. Для исправления этого вводится новая пара исчислений 𝜆А (отличается от 𝜆B только требованием рефайнмент сигнатур для функций) и 𝜆С (соответствующие рефайнменты), где изменены правила для LET и APP; также блокируется редукция для предикатов на функциях. В таком исчислении тайпчекинг уже не исчерпывается подстановкой, вычисление наислабейшего предусловия распадается на вычисление предусловий для всего кроме функций, и валидации аннотаций функций. Для доказательств здравости и полноты тут требуются еще монотонности по предикатам.

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

#refinementtypes

Hewer, Hutton, [2022] "Subtyping Without Reduction"

https://github.com/brandonhewer/Subtyping

Продолжаем тему субтипизации. Статья выстроена вокруг двух факторизованных кодировок субтипов - 1) сигмы с пропозиционально обрезанным индуктивным семейством и 2) индуктивно-рекурсивной с ограничением на инъективность одновременно определяемой функции; обе кодировки формализованы на кубической Агде. Мотивация - операции на субтипах как правило перевычисляют вшитый предикат, что может сильно замедлять тайпчекинг. В первой половине статьи в качестве рабочего примера берется подтип чётных натуральных чисел и операция сложения на нём.

Суть первой идеи - кодирование предиката, определяющего вхождение в субтип индуктивным типом, с добавлением дорогостоящих операций, замкнутых по предикату (т.е., вышеупомянутого сложения) как "неканонических" конструкторов. Такое добавление выбрасывает семейство из класса prop (т.к. доказательство одного факта теперь можно получить разными термами, например, сложением с нулем), но можно исправить это т.н. prop-обрезанием, т.е. постулированием равенства всех доказательств одного типа высшим конструктором. Для удобства работы можно построить изоморфизм между "каноническим" предикатом четности и факторизованным. Элиминировать из такого предиката назад в natы можно через введение промежуточного сигма-пропа или рекурсией по числам-индексам.

Вторая идея - использовать высшее индуктивно-рекурсивное определение для всего субтипа сразу. Т.е. строим сразу структурно чётные числа со вшитым сложением, одновременно определяя функцию toN для проекции в наты и добавляем высший конструктор для инъективности toN. Тут на словах обрисовывают построение изоморфизма с предыдущим определением, однако доступного кода нет. Пришлось реконструировать его самому на основе последующих разделов (поверх библиотеки cubical-mini): https://gist.github.com/clayrat/7e7e33d72fa2cf19dfe855c90981a41f

Фактически обе техники сводятся к построению DSL для операций на субтипах - блокирование редукции за счет кодирования функций данными и ускоряет тайпчекинг. Далее авторы решают перейти к примеру с конечными упорядоченными множествами Fin, кодируют их как сигму из ната и индуктивного неравенства (с конструкторами 0 < S _ и x < y -> S x < S y), благополучно забывают про первичную мотивацию и дальше работают только с самим типом неравенства - зашивают в него конструкторы для транзитивности и разницы-на-единицу (плюс проп-обрезание), подчеркивают что пруфы над расширенным вариантом сохраняют новые конструкторы, а не "нормализуют" их до двух канонических. Также обещают показать высшеиндуктивно-рекурсивный вариант в коде - но его там тоже нет.

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

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

В качестве родственных подходов статья называет SProp, аннотации стираемости и абстрактные определения. Проблема у первых двух - недостаточная композициональность; у последних - необходимость в дополнительных доказательствах. Как направление для будущей работы указывается задание произвольных равенств между операциями, выработка языка комбинаторов для субтипов и поиск более удобных элиминаторов.

#hott

3 ноября выступил с докладом на семинаре PSSV'23 по теме, которой интенсивно занимаюсь последние пару месяцев - guarded recursion (склоняюсь к переводу "отложенная рекурсия"). Сделаю тут небольшой конспект, более подробную информацию можно найти на слайдах и в github-репе.

Вкратце, идею отложенной рекурсии можно охарактеризовать как исчисление "задумок" (thunks), восходит она к модальным логикам доказуемости (система Гёделя-Лёба и подобные ей). В guarded системе типов отложенное вычисление, возвращающее A, обозначается как ▷A. Этот конструктор типов оснащен структурой аппликативного функтора, т.е., в качестве базовых операций мы можем отложить вычисление на один шаг (next : A → ▷A) и применить на следующем шаге функцию к аргументу (ap : ▷(A → B) → ▷A → ▷B). Основная же рабочая конструкция - это оператор (уникальной) отложенной неподвижной точки fix : (▷A → A) → A. С программистской точки зрения он ведет себя как рекурсия, возвращающая после каждой итерации контроль вызывающей стороне, что позволяет записывать тотальные алгоритмы в продуктивном виде, т.е., как потенциально бесконечную серию завершающихся вычислений, которая может быть прервана после каждого шага. Потенциально незавершающиеся вычисления на практике встречаются повсеместно - это всевозможные серверные программы и потоковые преобразования данных.

Классические структуры, которые можно определить с помощью отложенной рекурсии это:
* бесконечные потоки (streams)
* ко-списки (т.е., последовательности, могущие быть как конечными, так и бесконечными)
* расширенные числа Пеано (где есть терм для ∞)
* partiality monad (монада частичности, т.е., некоторое значение, получение которого отложено на неопределенное количество шагов, от 0 до ∞)

Применения отложенной рекурсии можно концептуально разделить на два класса: работа с бесконечными структурами напрямую и кодирование нестрогопозитивных рекурсивных типов. В качестве представителя первого класса можно привести определение и верификацию алгоритма Бёрда replaceMin, и его дальнейшие обобщения до MonadFix / value recursion. Нестрогопозитивные же определения можно продемонстрировать на примере алгоритма Хофманна для обхода дерева в ширину, вообще, такие конструкции (+ упомянутая монада частичности) часто всплывают при работе с моделями ЯП методом логических отношений и построении денотационных семантик. На этих идеях основано молодое направление ТЯП под названием (synthetic) guarded domain theory, где любой тип одновременно является доменом - это позволяет значительно упростить работу, избавившись от многочисленных доказательств "доменности".

Стоит заметить, что использование только guarded-модальности довольно жестко ограничивает возможность манипуляции задумками. С одной стороны, такой вездесущий контроль со стороны типов удобен. Классические подходы к работе с бесконечными структурами в пруф-ассистентах, вроде коиндуктивных механизмов, страдают от отсутствия композиционности - поскольку проверка на продуктивность в них работает синтактически, это регулярно приводит к ситуации, когда пруф-инженер получает ошибку о нарушении тотальности лишь после завершения трудоемкого доказательства, что, конечно, изрядно деморализует. С другой стороны, коиндуктивный ризонинг на guard-ах целиком не воспроизводится - интуитивно, при работе с отложенным вычислением мы можем только сохранять или увеличивать степень его "отложенности"; другими словами, задумки никогда нельзя "схлопывать" на этапе проектирования. Это ограничение можно обойти, расширив систему особыми переменными-часами, квантификацией по ним (частным случаем этой идеи является так называемая "константная" модальность) и примитивом force, который позволяет динамически запускать фрагменты отложенных вычислений в безопасных для этого контекстах.