PLCOMP Telegram 87
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



tgoop.com/plcomp/87
Create:
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

View MORE
Open in Telegram


Telegram News

Date: |

Deputy District Judge Peter Hui sentenced computer technician Ng Man-ho on Thursday, a month after the 27-year-old, who ran a Telegram group called SUCK Channel, was found guilty of seven charges of conspiring to incite others to commit illegal acts during the 2019 extradition bill protests and subsequent months. Administrators Ng was convicted in April for conspiracy to incite a riot, public nuisance, arson, criminal damage, manufacturing of explosives, administering poison and wounding with intent to do grievous bodily harm between October 2019 and June 2020. A vandalised bank during the 2019 protest. File photo: May James/HKFP. On June 7, Perekopsky met with Brazilian President Jair Bolsonaro, an avid user of the platform. According to the firm's VP, the main subject of the meeting was "freedom of expression."
from us


Telegram PLComp
FROM American