tgoop.com/covalue/74
Last Update:
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
BY Covalue
Share with your friend now:
tgoop.com/covalue/74