PLT Redex: 参数化语言定义

Question

这是个问题困扰我有一段时间了，想知道这里是否有人能帮忙。

我有一个名为lambdaLVar的语言的PLT Redex模型，它更或多或少是一个普通的无类型lambda演算，但扩展了一个包含"格变量"（或LVars）的存储。 LVar是一个只能随着时间增加而增加其值的变量，其中“增加”的含义由用户指定的偏序集（又称格）给出。因此，lambdaLVar实际上是一系列语言-将其实例化为一个格，您将获得一种语言;带有不同格子，您将获得另一种语言。您可以在此处查看代码；重要的内容在lambdaLVar.rkt。 在lambdaLVar的纸上定义中，语言定义是由用户指定的格参数化的。很长一段时间以来，我一直想在Redex模型中进行相同类型的参数化，但到目前为止，我还没有找到方法。部分麻烦在于，语言的语法取决于用户如何实例化格：格的元素成为语法中的终结符号。我不知道如何在Redex中表达一个抽象的语法来覆盖格。

同时，我尽量让lambdaLVar.rkt尽可能模块化。在该文件中定义的语言专用于特定的格：最小上界（lub）操作为max的自然数。（或者，等价地，通过<=排序的自然数。这是一个非常无聊的格。）代码中仅与该格有关的部分是靠近顶部的行（define lub-op max）和在语法中出现的natural。（有一个lub元函数是用用户指定的lub-op函数定义的。后者只是一个Racket函数，因此lub必须跳出到Racket以调用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))])

接着，为了替换我在lambdaLVar中使用的两个缩减关系slow-rr和fast-rr，我可以定义一对包装器：

(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。 small-step-base的合同行只是#:contract (small-step-base Config Config)，其中Config是一个语法非终结符，在lambdaLVar-nats下重新解释后具有新的含义，而不是在lambdaLVar下，因为涉及到特定的格子问题。作为实验，我删除了small-step-base和small-step-slow上的合同。

然后我就能够运行我的19个测试程序，但其中10个失败了。也许并不奇怪的是，所有失败的都是以某种方式使用自然数值LVars的程序。(其余的是"纯粹"的程序，根本不与LVars存储交互。)所以失败的测试恰好是使用扩展语法的那些测试。

所以我继续沿着兔子洞走，似乎Redex希望我将所有现有的判断形式和元函数扩展，使它们与lambdaLVar-nats相关联，而不是与lambdaLVar相关联。这很有道理，据我所知，对于判断形式来说，它似乎可以正常工作，但在元函数中，我遇到了麻烦：我希望新的元函数重载同名的旧函数(因为现有的判断形式正在使用它)，但似乎没有办法做到这一点。如果我必须重命名元函数，那就失去了意义，因为我还必须编写全新的判断形式。我想我需要的是元函数调用的一种后期绑定！

简而言之，我的问题是：在Redex中是否有任何方式可以按照我想要的方式对语言定义进行参数化，或者以能够实现我的要求的方式扩展语言定义？还是最终只能编写生成Redex的宏？

谢谢阅读！

- Lindsey Kuper

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 尽快支持模块化，但在此期间，这种方法似乎能够很好地工作。

- Lindsey Kuper