Так как я теперь работаю с 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, который позволяет динамически запускать фрагменты отложенных вычислений в безопасных для этого контекстах.

Hewer, Hutton, [2024] "Quotient Haskell: lightweight quotient types for all"

Мой порт секций 2+3 на Cubical Agda: source

У субтипов есть дуальная редко используемая, но полезная конструкция - фактор-типы. Для субтипа мы доказываем выполнение предиката при конструировании, а для фактор-типа - при элиминации. Классический пример программистской фактор-конструкции - мультимножества (bags), т.е. списки, факторизованные по перестановке элементов. При работе с такой конструкцией для каждой функции, принимающей bag аргументом, нужно доказывать, что её результат не зависит от перестановок нижележащего списка. Эти пруф-обязательства можно автоматизировать, ограничив логику до SMT-разрешимой. Так мы получаем систему рефайнмент-типов, например автоматизация для субтипов широко используется в LiquidHaskell. Однако, автоматизация для фактор-типов менее изучена, каковой пробел и восполняет статья, вводя расширение LH - QuotientHaskell. Основная идея состоит в переводе эквациональных законов, требуемых функциями на фактор-типах, в предикаты refinement логики. Класс поддерживаемых фактор-типов - quotient inductive types (QIT), где конструкторы индуктивного типа определяются одновременно с уравнениями для данных. Первая часть статьи посвящена трем мотивирующим примерам.

Первый пример - "мобили", бинарные деревья с данными в нодах, факторизованные по зеркальному отражению ветвей (Node l a r == Node r a l). Для создания фактор-типа нужно добавить "высший" конструктор нужного равенства (в гомотопической терминологии - "пути"). В логике QH эти конструкторы становятся обычными равенствами; ключевой момент - терм в левой части уравения должен иметь каноническую (конструкторную) форму. Фактор-определения технически создают новый тип, а не являются рефайнментом старого.

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

Следующий пример - "бум-иерархия": деревья с (опциональными) данными в листьях -> списки -> (конечные) мультимножества -> множества.

* Чтобы получить списка из дерева, нужно факторизовать его по законам моноида (где "сложение" это конструктор ноды). Конкатенация такого фактор-списка имеет константную сложность, т.к. мы просто добавляем новую ноду, не пересчитывая нормальную форму списка - это может быть полезно, когда у нас много подобных операций, а линейное представление списка используется редко. На факторизованных списках работают древесные операции, сохраняющие структуру моноида - sum, map, filter.
* Мультимножества получаются повторной факторизацией по коммутативности "сложения", аналогично мобилям. Это отсекает функции, учитывающие порядок элементов, например, toList.
* Множества получаются окончательной факторизацией по идемпотентности, что запрещающает различать разные вхождения одного и того же элемента. Мы по-прежнему можем использовать функции типа contains, но уже не имеем права подсчитывать количество вхождений.

Последний классический пример фактор-конструкции это рациональные числа, получаемые факторизацией пар целых чисел по равенству перекрестных произведений числителя на знаменатель. Такой подход позволяет не скрывать внутреннюю структуру типа в целях сохранения инварианта. В определении также используется рефайнмент знаменателя до ненулевых чисел. Важно выбрать удобное определение спецификации для факторизации - вместо произведения можно использовать GCD, но тогда в доказательствах придется рассуждать о его свойствах, что потенциально менее автоматизируемо. Для извлечения числителя и знаменателя нужно сначала определить функцию reduce, вычисляющую нормальную форму дроби через всё тот же GCD. Авторы отмечают, что для корректной работы QH нужно включенное по умолчанию расширение PLE (алгоритм поиска доказательств из набора уравнений в контексте).

Ядром QH является λQ, лямбда-исчисление с паттернами (термами первого порядка, построенными из конструкторов и переменных) - расширение λL, ядра жидких типов. К контекстам добавляются факторы и guard-предикаты (высказывания, соответствующие истинным предположениям внутри if-веток). Фактор - это набор квантифицированных переменных и тройка из refinement предиката, паттерна (левая часть равенства) и терма общего вида (правая часть). Для факторов нужна подстановка, также факторы могут применяться одновременно, но должны быть попарно независимы. Для корректности необходимо вычислять most general unifiers (MGU) для паттернов. Стоит также отметить, что система не поддерживает расширение фактор-типов до GADT, т.наз. quotient inductive families. Наконец, показывается, что конгруэтность функций (a = b -> f a = f b) сохраняется для факторизованных равенств.

Также, для удобства пользователя, λQ вводит на фактор-типах порядок субтипизации, что позволяет напрямую использовать "менее" факторизованные типы в функциях на "более" факторизованных (т.е., контравариантность).

Система вводит два класса равенств - пропозициональное равенство из рефайнмент логики, и расширенное judgemental равенство в системе типов, более слабое. Это второе равенство позволяет конструировать из системы факторов в контексте набор уравнений, который далее будет передан SMT-солверу. Правила для манипуляции расширенными равенствами выстроены таким образом, чтобы получить завершающийся тайпчекинг и соблюсти все хорошие свойства, ожидаемые от равенства. Потенциально проблематичным, однако, является наивный полный перебор всех комбинаций из n факторов в контексте, т.е. n! вариантов; авторы утверждают, что на практике это число достаточно мало.

QH построен как расширение LiquidHaskell, он вносит изменения в парсер (фактор-выражения и вспомогательные доказательства соблюдения фактор-равенств), AST, процесс генерации равенств и тайпчекинг для case-выражений. Используемый язык паттернов это урезанная версия хаскельных паттернов (нет wildcards, irrefutable patterns, as-patterns). Тайпчекинг фактор-типов включает в себя ряд этапов: проверка грамматической корректности, лифтинг равенств (генерация уравнений для солвера), проверка соблюдения фактор-условий при элиминации факторизованных данных (на этой фазе важно иметь термы в нормальной форме, из чего вытекает требование включения PLE по умолчанию), процедуру разрешимости для субтипизации фактортипов. Для быстродействия вычисленные отношения субтипизации кэшируются, и производятся оптимизации для тривиальных теорем.

В качестве схожих работ авторы приводят Cubical Agda (чьими фактор-типами они явно вдохновлялись), аксиоматизацию факторов в Lean, разрешимые факторы в Coq/Mathcomp, ряд реализаций в Isabelle и реализацию в NuPRL. Последние два пункта идеологически близки, поскольку предполагают сопутствующую автоматизацию, однако реализации в Isabelle имеют более низкий уровень автоматизации, а NuPRL требует принятия аксиомы выбора.

В конце статьи авторы обозревают свои достижения: интеграцию с SMT-автоматизированной системой субтипов, реализацию QITs, неявные преобразования между функциями на типах разной степени факторизованности. Кроме того, остался еще ряд примеров, которыми они спешат поделиться: реализация модульной арифметики, факторизованная система полярных координат, лямбда-исчисление со вшитым eta-равенством. В качестве ограничений называются: отсутствие function extensionality, GADTs/QIFs и неинтуитивные сообщения об ошибках. Работу над этими моментами, а также над автоматическим выводом фактор-типов авторы оставляют на будущее.

Во вторник, 9 апреля, снова читал доклад про отложенную рекурсию, на этот раз постарался сделать его более "программистским", добавив больше примеров использования.

Набор постов от William Bowman по понятиям ТЯП (реализуемость, логические отношения, синтаксис, модель):

https://www.williamjbowman.com/blog/2022/10/05/what-is-realizability/
https://www.williamjbowman.com/blog/2023/03/24/what-is-logical-relations/
https://www.williamjbowman.com/blog/2023/06/07/what-is-syntax/
https://www.williamjbowman.com/blog/2023/06/15/what-is-a-model/

И еще одна слегка расширенная версия доклада про отложенную рекурсию: добавил немного примеров с доказательствами.

Bertot, [2008] "Structural abstract interpretation, A formal study using Coq"

+ порт на Агду

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

Идея абстрактной интерпретации заключается в вычислении приближенных значений для некоторых аспектов поведения программы - обычно анализ делается по графу потока управления программы, но в статье анализируется напрямую синтаксическое дерево. Такую аппроксимацию, как правило, можно получить значительно быстрее, нежели исполнять саму программу, при этом на её основании можно проводить компиляторные оптимизации и делать выводы о корректности. Стандартным примером приближенного анализа является огрубление точных значений числовых переменных до бита четности или интервала значений. Классически при этом выводится аппроксимация "сверху" (overapproximation), т.е. мы хотим гарантировать отсутствие ложноотрицательных результатов за счет возможных ложноположительных (стандартный компромисс статического анализа). Формально отношения между точными (конкретными) и приближенными (абстрактными) множествами значений описываются в теории АИ через соответствия Галуа (пара функции абстракции α и функции конкретизации γ, необходимы для транспорта отношений порядка), в статье используется ad-hoc форма этой конструкции. Также требуется, чтобы домен абстрактных значений имел структуры полугруппы (т.к. моделируются числовые значения) и ограниченной (полу)решетки.

Для задания семантики анализируемого языка используется исчисление предусловий, состоящее из (1) бескванторных логических формул (предусловий/assertions) и аннотированных ими программ, (2) функции вычисления наислабейшего предусловия (формулы, которой должны удовлетворять переменные в начале исполнения) по аннотированной программе и (3) функции для генерации условий проверки (набор импликаций, которые, будучи валидными, гарантируют что любое исполнение программы, стартующее из удовлетворяющего предусловию состояния, будет удовлетворять всем последующим формулам). Для while-циклов также добавляются явные инварианты. Нужно заметить, что в самой статье полноценная аксиоматическая семантика c пред- и постусловиями не вводится, но это проделано в предыдущей статье автора, откуда я взял соответствующий кусок с доказательствами корректности аксиоматической семантики относительно операционной и корректности генератора условий. Ключевым же свойством генератора условий для корректности абстрактного интерпретатора является монотонность, т.е. валидность условий, построенных из некой формулы влечет валидность условий, построенных из её ослабления. Задача абстрактного интерпретатора - по исходной программе и абстрактному начальному состоянию одновременно вывести аннотированную программу и абстрактное конечное состояние.

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

Первый интерпретатор просто использует эти функции напрямую для рекурсивного аннотирования программы, не пытаясь вывести инварианты циклов (подставляя вместо них тривиально истинные формулы). Его корректность сводится к трем свойствам: (1) наислабейшее предусловие, полученное из вычисленного конечного состояния, действительно слабее предусловия, полученного из начального состояния, (2) все условия проверки, полученные из вычисленной аннотированной программы и конечного состояния, являются валидными и (3) вычисленная аннотированная программа идентична исходной программе после стирания аннотаций. Пример работы этого интерпретатора проиллюстрирован на домене битов четности со свободно добавленным верхним элементом (кодирующим отсутствие информации).

Второй интерпретатор более серьезно подходит к работе с циклами, используя информацию о том, что тест цикла всегда истинен внутри его тела и ложен на выходе. Незавершимость кодируется обертыванием конечного состояния в опциональный тип в выдаче интерпретатора. К параметрам добавляются две новые функции, которые вычисляют уточнения абстрактного состояния в зависимости от успешно и неуспешно пройденного теста цикла соответственно; именно эти функции берут на себя основную сложность задачи, в частности, они пытаются выводить информацию о незавершимости, и эта же информация позволяет пометить мертвый код тривиально ложными аннотациями. Схема процесса вывода инварианта цикла (в общем случае эта задача неразрешима!) выглядит так: (1) несколько абстрактных прогонов тела цикла (их количество контролируется эвристикой) с нарастающим расширением множества значений переменных - если процесс стабилизировался, инвариант найден; (2) если инвариант не найден, запускаем процесс 1 еще раз с переаппроксимацией для значений некоторых переменных - это позволяет ускорить процесс схождения (количество этих повторов также контролируется отдельной эвристикой); (3) если инвариант всё еще не найден, выбрать гарантированный инвариант (первый интерпретатор сразу же делает это, используя тривиальную истину); (4) сужение переаппроксимированных инвариантов повторным запуском интерпретатора (наличие этого шага приводит к определению интерпретатора через вложенную рекурсию).

Реализация этих шагов требует введения ряда вспомогательных функций-параметров, например, для сравнения количества информации в двух абстрактных значениях. Для доказательства корректности второго интерпретатора (состоящего из тех же трёх частей, что и в первом случае) также требуются 14 новых условий, описывающих все эти новые функции и их взаимодействие. Обе реализации интерпретаторов и их доказательства упакованы в модули, параметризующие их по абстрактному домену. Первый интерпретатор уже был ранее инстанцирован доменом чётности, а для второго описано кодирование домена числовых интервалов с потенциально бесконечными границами, где роль верхнего элемента играет интервал (-∞,+∞), а переаппроксимация заключается в замене одной из границ на -/+∞.

В заключение автор отмечает, что статью не следует рассматривать как полноценное введение в теорию АИ, а реализованные интерпретаторы являются моделями, т.к. оставляют желать лучшего в плане производительности - например, при вычислении аннотаций повторяется работа, уже проделанная ранее при поиске инварианта цикла. Кроме того, статический анализ может быть эффективнее, если рассматривать не отдельные переменные, а отношения между несколькими переменными.

#automatedreasoning

Возможно, кому-то будет интересно поучаствовать в данном проекте. Ребята занимаются поиском и оптимизацией путей на графах Кэли - это такая комбинаторная кодировка группы, где элементы группы становятся вершинами, а ребра связывают те элементы, что получаются друг из друга умножениями на один из генераторов группы. Это позволяет изучать структуру групп с помощью методов теории графов; в частности, искать подходы к решению word problem для разных групп (т.е. сравнению структур по модулю правил перезаписи, разновидностями этого класса задач являются нормализация и унификация в ТЯП). Также любопытно, что графы Кэли являются примером Para-конструкции из прикладного теорката.

🚀 Уважаемые коллеги, тех, кому интересна математика и машинное обучение, приглашаем Вас принять в неформальном проекте.

Минимальное требование - Вы знакомы с Питоном, и у Вас есть несколько часов свободного времени в неделю. (Альтернативно - можно не знать Питон, но хорошо знать теорию групп (в идеале GAP,SAGE).) Задача проекта - применить машинное обучение к теории групп. Целью проекта является написание статьи в хорошем журнале, участники - соавторы. Другим бонусом будет являться - приобретение навыков по современным методам нейронных сетей, Reinforcement Learning и т.д.

Если Вам интересно участие - напишите @alexander_v_c (Александр Червов, к.ф.-м.н. мехмат МГУ, 25 лет math&DS, Kaggle, Scholar, Linkedin).
Чат для обсуждений: тут .
Вводный доклад тут.
Пояснения по RL части тут.

Краткая суть задачи может быть описана несколькими способами - нахождение пути на графе от вершины А до вершины Б, но размер графа 10^20-10^50 - обычные методы не применимы. Решение пазла типа Кубика Рубика. Задача близка к прошедшему конкурсу Каггл Санта 2023. Математически - разложение элемента группы по образующим. Математические пакеты, которые частично могут решать эту задачу - GAP,SAGE.

Достигнутые результаты - уже сейчас мы можем за минуты делать то, что авторы работы DeepCube делали за 40 часов на многих GPU.

Пару недель назад выпустил в открытое плавание (переведя под крыло Coq community) проект, над которым эпизодически работаю c 2021 года: FDSA in SSReflect.

Идея банальна - переписать код из открытой книги Nipkow et al, "Functional Data Structures and Algorithms" (в начале работы книга называлась "Functional Algorithms, Verified") с Isabelle/HOL на полностью типотеоретический язык. Для портирования я выбрал Coq + фреймворк Mathcomp/SSReflect + плагин Equations для компактной записи паттерн-матчинга и доказательств завершимости.

В Isabelle/HOL для ризонинга используется классическая логика, но для работы с корректностью вычислительных структур данных разница с конструктивной логикой невелика, поскольку почти всегда предполагается, что элементы этих структур как минимум дискретны (то есть снабжены разрешимой проверкой на равенство, что соответствует "локальному" исключенному третьему). Основное отличие, пожалуй, только в одном месте - вместо использования равенств на мультимножествах из Isabelle я использую списки и отношение перестановки (perm_eq) на них. Кроме того, в Isabellе функции не обязаны быть тотальными, что влечет за собой необходимость слегка менять определения - дополняя их для всей области определения и давая доказательства завершимости во всех случаях (а не только в избранных, как в книге).

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

Книга устроена следующим образом:

0. Вводная глава с основными понятиями.
1. Раздел, посвященный алгоритмам сортировки и выбора: mergesort/quicksort/quickselect. На мой взгляд, глава про алгоритм выбора делает ощутимый скачок в сложности, т.к. для quickselect доказательства завершимости (из-за использования вложенной рекурсии) и комплексити (упрощенный вариант теоремы Акра-Баззи) на порядок (а то и два) замысловатее таковых для сортировок.
2. Крупный раздел об алгоритмах на деревьях - тут и популярные красно-черные/AVL-деревья, и менее известные деревья Брауна, и специализированные квадродеревья.
3. Идеологическое продолжение предыдущего раздела о нескольких способах реализации очередей с приоритетом.
4. Раздел о продвинутых алгоритмических методах, включающий динамическое программирование, амортизационный анализ и косые деревья. До этого раздела я пока еще не добрался, остановился на адаптации поисковых деревьев из предыдущих глав в поисковую таблицу для кэширования результатов в динамическом программировании.
5. Раздел "разное": на текущий момент там есть строковый алгоритм Кнута-Морриса-Пратта, алгоритм сжатия Хаффмана и поисковый алгоритм αβ-отсечения. Тут я пока реализовал только алгоритм Хаффмана.

В целом, книга довольно неплохо объясняет классические иммутабельные алгоритмы (хотя местами слишком сжато, особенно в 4м разделе), этакий пруф-инженерный вариант известной работы Okasaki, [1998] "Purely functional data structures". В книге много упражнений, большинство из которых я прорешал, но в публичном репозитории заменил соответствующие места скелетами определений и теорем, чтобы не спойлить решения для потенциальных студентов.

#datastructures

https://cs.nyu.edu/media/publications/pavlinovic_zvonimir.pdf Pavlinovic, [2019] "Leveraging Program Analysis for Type Inference"