Covalue

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

www.tgoop.com/covalue/81

1.3K viewsFeb 10 at 09:01

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

BY Covalue