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: |

The Channel name and bio must be no more than 255 characters long During a meeting with the president of the Supreme Electoral Court (TSE) on June 6, Telegram's Vice President Ilya Perekopsky announced the initiatives. According to the executive, Brazil is the first country in the world where Telegram is introducing the features, which could be expanded to other countries facing threats to democracy through the dissemination of false content. A few years ago, you had to use a special bot to run a poll on Telegram. Now you can easily do that yourself in two clicks. Hit the Menu icon and select “Create Poll.” Write your question and add up to 10 options. Running polls is a powerful strategy for getting feedback from your audience. If you’re considering the possibility of modifying your channel in any way, be sure to ask your subscribers’ opinions first. Judge Hui described Ng as inciting others to “commit a massacre” with three posts teaching people to make “toxic chlorine gas bombs,” target police stations, police quarters and the city’s metro stations. This offence was “rather serious,” the court said. 1What is Telegram Channels?
from us


Telegram PLComp
FROM American