PLT Redex: параметризация определения языка

Question

Это проблема, которая беспокоит меня в течение некоторого времени, и мне интересно, может ли кто-нибудь здесь помочь.

У меня есть модель 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?

Спасибо за прочтение!

Answer 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 скоро получит модули, но пока что это работает хорошо.