PLT Redex: параметризация определения языка
Это проблема, которая беспокоит меня в течение некоторого времени, и мне интересно, может ли кто-нибудь здесь помочь.
У меня есть модель PLT Redex для языка, называемого lambdaLVar, который является более или менее нетипизированным лямбда-исчислением садового сорта, но дополнен хранилищем, содержащим "переменные решетки", или LVars. LVar - это переменная, значение которой может только увеличиваться с течением времени, где значение "увеличения" задается частично упорядоченным набором (иначе говоря, решеткой), который задает пользователь языка. Поэтому lambdaLVar - это действительно семейство языков - создайте его с одной решеткой, и вы получите один язык; с другой решеткой, и вы получите другую. Вы можете посмотреть код здесь; важные вещи есть в lambdaLVar.rkt.
В определении lambdaLVar на бумаге определение языка параметризовано этой пользовательской решеткой. В течение долгого времени я хотел сделать такую же параметризацию в модели Redex, но до сих пор я не смог понять, как это сделать. Отчасти проблема в том, что грамматика языка зависит от того, как пользователь создает экземпляр решетки: элементы решетки становятся терминалами в грамматике. Я не знаю, как выразить грамматику в Redex, которая абстрактна по решетке.
Тем временем я попытался сделать lambdaLVar.rkt как можно более модульным. Язык, определенный в этом файле, специализирован для конкретной решетки: натуральные числа с max
как операция с наименьшей верхней границей (lub). (Или, что то же самое, натуральные числа, упорядоченные <=
, Это очень скучная решетка.) Единственными частями кода, которые являются специфическими для этой решетки, являются строки (define lub-op max)
около вершины, и natural
появляются в грамматике. (Есть lub
метафункция, которая определяется в терминах указанного пользователем 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.) Итак, неудачные тесты - это именно те, которые используют расширенную грамматику.
Поэтому я продолжал следить за кроличьей ношей, и похоже, что Редекс хочет, чтобы я расширил все существующие формы суждений и метафункции, чтобы они были связаны с lambdaLVar-nats, а не с lambdaLVar. Это имеет смысл, и, насколько я могу судить, это работает нормально для форм суждений, но с метафункциями у меня возникают проблемы: я хочу, чтобы новая метафункция перегружала старую с тем же именем (потому что существующие формы суждений используют ее) и, кажется, нет способа сделать это. Если мне придется переименовать метафункции, это противоречит цели, потому что в любом случае мне придется писать совершенно новые формы суждений. Я полагаю, что я хочу что-то вроде поздней привязки вызовов метафункций!
Вкратцемой вопрос: есть ли в Redex какой-либо способ параметризовать определение языка так, как я хочу, или расширить определение языка так, чтобы он делал то, что я хочу? Буду ли я в итоге писать макросы, генерирующие Redex?
Спасибо за прочтение!
1 ответ
Я спросил список рассылки пользователей Racket; нить начинается здесь. Подводя итоги обсуждения: в Redex в его нынешнем виде ответ - нет, нет способа параметризовать определение языка так, как я хочу. Однако это должно быть возможно в будущей версии Redex с модульной системой, которая сейчас находится в разработке.
Это также не работает, чтобы попытаться использовать существующие формы расширения Redex (define-extended-language
, extend-reduction-relation
и т. д.), как я пытался сделать здесь, потому что, как я обнаружил, оригинальные метафункции не интерпретируются транзитивно для использования расширенных языков. Но модульная система, по-видимому, тоже поможет в этом, потому что она позволит вам собирать вместе метафункции, суждения и редукционные отношения и одновременно расширять их (см. Обсуждение здесь).
Итак, на данный момент ответ, действительно, написать макрос, генерирующий Redex. Примерно так работает:
(define-syntax-rule (define-lambdaLVar-language name lub-op lattice-values ...)
(begin
;; Entire original Redex model goes here, with `natural` replaced with
;; `lattice-values ...`, and instances of `...` replaced with `(... ...)`
))
И тогда вы можете создать конкретные решетки, например:
(define-lambdaLVar-language lambdaLVar-nat max natural)
Я надеюсь, что Redex скоро получит модули, но пока что это работает хорошо.