tgoop.com/plcomp/87
Last Update:
https://arxiv.org/abs/2001.10490
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
Большинство систем интерактивного доказательства теорем разрабатываются с прицелом на формализацию математики. Включая возможность использования специфической математической нотации, разработанной для некоторой теории. Такой как 𝛴, 𝛱 или ∫, которые используются не только в математическом анализе, но и в теории категорий, например. Характерная особенность приведённых обозначений, как и многих других — "захват переменных" аналогично тому, как переменные захватываются кванторами в логике и лямбда-абстракцией в лямбда-исчислении. При этом, поскольку системы интерактивного доказательства строятся поверх того или иного варианта лямбда-исчисления, математическую нотацию придётся выражать именно через лямбды, и как-то с ними взаимодействовать.
В этот момент возникает вопрос "гигиены": мы не хотим, чтобы переменные перепутались и были связаны с неправильной лямбда-абстракцией, ообенно "невидимой" лямбдой, которая была автоматически сгенерирована в процессе трансляции другой нотации. Вопрос дополнительно осложняется естественным "инженерным" требованием: поскольку многие обозначения используют одинаковый синтаксис связывания переменных, мы хотели бы описать этот синтаксис и его семантику один раз, и просто переиспользовать во всех подходящих случаях. Примерами переиспользования синтаксиса связывания переменных могут служить те же нотации для сумм и произведений: 𝛴 и 𝛱.
Статья демонстрирует как можно решить эту задачу при помощи типизированной системы макросов и несложного алгоритма, обеспечивающего гигиену. Само собой, за простоту приходится чем-то заплатить. В данном случае — ограниченной применимостью, поскольку алгоритм полагается на определённые свойства языка программирования. Наиболее существенное из них: выполнение программы осуществляется "построчно", по одному выражению верхнего уровня за раз, в порядке их записи в файле. Новую нотацию (на самом деле, любой макрос) могут использовать только выражения, записанные ниже определения макроса. И некоторые другие упрощающие предположения. Такое поведение часто встречается в системах интерактивного доказательства теорем, но сильно ограничивает применимость в языках программирования общего назначения. Для таких языков придётся пользоваться намного более сложным алгоритмом гигиены, как, например, в Racket.
Кроме того, в статье рассматриваются вопросы интеграции макро-системы и систем "уточнения" (elaboration) и type-driven expansion, плюс реализация тактик в виде гигиенических макросов, чего до сих пор не встречалось в системах интерактивных доказательств.
В итоге, несмотря на очевидную направленность на системы интерактивного доказательства, статья является отличным введением в проблематику, связанную с макросами, обеспечением гигиены, типизацией макросов, декларативным и императивным заданием макросов. Рекомендую всем читателям, ещё не знакомым, но интересующимся вопросами создания макро-систем в языках программирования.
#macros #lean #elaboration #proofassistants
BY PLComp
Share with your friend now:
tgoop.com/plcomp/87