Это проблема, которая время от времени наталкивается на меня, и мне интересно, может ли кто-нибудь здесь помочь.PLT Redex: параметрирование определения языка
У меня есть модель PLT Redex языка, называемая lambdaLVar, которая является более или менее разновидным лямбда-исчислением садовых разновидностей, но дополняется хранилищем, содержащим «переменные решетки» или LVars. LVar - это переменная, значение которой может только увеличиваться со временем, когда значение «увеличения» задается частично упорядоченным множеством (ака решетки), которое указывает пользователь языка. Поэтому lambdaLVar - это действительно семейство языков - создайте его с помощью одной решетки, и вы получите один язык; с другой решеткой, и вы получите другую. Вы можете посмотреть код here; важный материал находится в lambdaLVar.rkt.
В определении lambdaLVar на бумаге определение языка параметризуется этой заданной пользователем решеткой. В течение долгого времени я хотел сделать такую же параметризацию в модели Redex, но до сих пор я не мог понять, как это сделать. Частично проблема заключается в том, что грамматика языка зависит от того, как пользователь создает экземпляр решетки: элементы решетки становятся терминалами в грамматике. Я не знаю, как выразить грамматику в Redex, которая является абстрактной по решетке.
Тем временем я попытался сделать lambdaLVar.rkt настолько модульным, насколько мог. Язык, определенный в этом файле, специализирован для конкретной решетки: натуральные числа с max как операция наименьшей верхней границы (lub). (Или, что то же самое, натуральные числа, упорядоченные по <=. Это очень скучная решетка.) Единственными частями кода, характерными для этой решетки, являются строка (define lub-op max), расположенная вверху, и natural, появляющиеся в грамматике. (Там в lub metafunction, который определен в терминах заданного пользователя lub-op функции. Последнее является лишь функцией Ракетки, поэтому lub должно бежать, чтобы ракетка позвонить lub-op.)
Запрещая способность фактически указать lambdaLVar таким образом, который является абстрактным по выбору решетки, кажется, что я должен был бы написать версию lambdaLVar с самыми голыми решетками - просто элементы Bot и Top, где Bot < = Top - и затем используйте define-extended-language, чтобы добавить больше материала. Например, я мог бы определить язык, называемый lambdaLVar-Nats, который специализируется на натуралов решетки я описал:
;; Grammar for elements of a lattice of natural numbers.
(define-extended-language lambdaLVar-nats
lambdaLVar
(StoreVal .... ;; Extend the original language
natural))
;; All we have to specify is the lub operation; leq is implicitly <=
(define-metafunction/extension lub lambdaLVar-nats
lub-nats : d d -> d
[(lub-nats d_1 d_2) ,(max (term d_1) (term d_2))])
Затем, чтобы заменить два отношения сокращения slow-rr и fast-rr, что я имел для lambdaLVar, я могла бы определить пар оберток:
(define nats-slow-rr
(extend-reduction-relation slow-rr
lambdaLVar-nats))
(define nats-fast-rr
(extend-reduction-relation fast-rr
lambdaLVar-nats))
Мое понимание из документации на extend-reduction-relation является то, что она должна переосмыслить правила slow-rr и fast-rr, но с использованием lambdaLVar-Nats. Положив все это вместе, я попытался запустить тестовый пакет, который я имел с одним из новых, расширенных отношений сокращения:
> (program-test-suite nats-slow-rr)
Первое, что я получаю это нарушение контракта жалоба: small-step-base: input (((l 3)) new) at position 1 does not match its contract. Контрактная линия малой ступени основывается только на #:contract (small-step-base Config Config), где Config - это нетерминал грамматики, который имеет новое значение, если он интерпретируется под lambdaLVar-nats, чем при lambdaLVar, из-за специфического материала решетки. В качестве эксперимента я избавился от контрактов на small-step-base и small-step-slow.
Тогда я смог фактически запустить 19 тестовых программ, но 10 из них потерпят неудачу. Возможно, неудивительно, что все те, которые терпят неудачу, - это программы, которые каким-то образом используют LVAR с натуральным числом. (Остальные - «чистые» программы, которые вообще не взаимодействуют с магазином LVars.) Таким образом, тесты, которые терпят неудачу, являются именно теми, которые используют расширенную грамматику.
Итак, я продолжал следить за кроличьей дырой, и, похоже, Redex хочет, чтобы я расширил все существующие формы суждений и метафрукты, связанные с lambdaLVar-nats, а не lambdaLVar. Это имеет смысл, и, кажется, это нормально работает для суждений, насколько я могу судить, но с метафайлами у меня возникают проблемы: я хочу, чтобы новый метафорум перегрузил старое одноименное имя (потому что существующие формы суждения используют его), и, похоже, нет способа сделать это. Если мне нужно переименовать метафунты, это победит цель, потому что мне все равно придется писать все новые суждения. Я полагаю, что то, что я хочу, - это своего рода поздняя привязка вызовов метафурнов!
Мой вопрос в двух словах: Есть ли способ в Redex спараметрировать определение языка так, как я хочу, или расширить определение языка таким образом, что будет делать то, что я хочу? Смогу ли я просто написать макросы, генерирующие Redex?
Спасибо за чтение!