13

这是一个困扰我一段时间的问题，我想知道这里是否有人可以提供帮助。

我有一个名为 lambdaLVar 的语言的 PLT Redex 模型，它或多或少是一种普通的无类型 lambda 演算，但扩展了包含“晶格变量”或 LVars 的存储。LVar 是一个变量，其值只能随时间增加，其中“增加”的含义由语言用户指定的部分有序集合（又名格）给出。因此 lambdaLVar 实际上是一个语言家族——用一个格子实例化它，你就会得到一种语言；用不同的格子，你得到另一个。你可以看看这里的代码；重要的东西在lambdaLVar.rkt中。

在 lambdaLVar 的纸上定义中，语言定义由用户指定的格参数化。很长一段时间以来，我都想在 Redex 模型中做同样的参数化，但到目前为止，我还没有弄清楚如何做。部分麻烦在于语言的语法取决于用户如何实例化格：格的元素成为语法中的终结符。我不知道如何在 Redex 中表达一个在格上抽象的语法。

同时，我尝试使 lambdaLVar.rkt 尽可能模块化。该文件中定义的语言专门用于特定的格：自然数max作为最小上界（lub）操作。（或者，等效地，按 . 排序的自然数<=。这是一个非常无聊的格子。）特定于该格子的代码的唯一部分是(define lub-op max)靠近顶部的行，并natural出现在语法中。（有一个lub根据用户指定的函数定义的元lub-op函数。后者只是一个 Racket 函数，因此lub必须转义到 Racket 才能调用lub-op。）

除非能够以一种对晶格选择抽象的方式实际指定 lambdaLVar，否则我似乎应该能够编写一个具有最简单晶格的 lambdaLVar 版本——只有 Bot 和 Top 元素，其中Bot <= Top -- 然后define-extended-language用来添加更多东西。例如，我可以定义一种名为 lambdaLVar-nats 的语言，它专门用于我描述的 naturals lattice：

;; 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是，它应该重新解释 and 中的规则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 的契约线是 just #:contract (small-step-base Config Config)，其中Config是一个语法非终结符，如果在 lambdaLVar-nats 下重新解释比在 lambdaLVar 下重新解释，它具有新的含义，因为特定的格子的东西。作为一个实验，我摆脱了 和 的small-step-base合同small-step-slow。

然后我能够实际运行我的 19 个测试程序，但其中有 10 个失败了。也许不足为奇的是，所有失败的程序都是以某种方式使用自然数值 LVar 的程序。（其余的是完全不与 LVar 存储交互的“纯”程序。）因此，失败的测试正是使用扩展语法的测试。

所以我一直在跟踪兔子洞，似乎 Redex 想要我扩展所有现有的判断形式和元函数，以与 lambdaLVar-nats 而不是 lambdaLVar 相关联。这是有道理的，据我所知，它似乎对判断形式有效，但是对于元函数我遇到了麻烦：我希望新的元函数重载同名的旧元函数（因为现有的判断形式正在使用它) 并且似乎没有办法做到这一点。如果我必须重命名元函数，那就达不到目的了，因为无论如何我都必须编写全新的判断形式。我想我想要的是一种元函数调用的后期绑定！

简而言之，我的问题是： Redex 中是否有任何方法可以以我想要的方式参数化语言的定义，或者以某种方式扩展语言的定义，从而满足我的需求？我最终只需要编写生成 Redex 的宏吗？

谢谢阅读！

4

1 回答 1

5

我询问了 Racket 用户的邮件列表；线程从这里开始。总结一下由此产生的讨论：在今天的 Redex 中，答案是否定的，没有办法以我想要的方式参数化语言定义。但是，在带有模块系统的未来版本的 Redex 中应该是可能的，目前正在开发中。

define-extended-language以我在这里尝试的方式尝试使用 Redex 的现有扩展形式（ 、等）也不起作用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 能尽快获得模块，但与此同时，这似乎运作良好。

于 2013-04-06T18:58:09.713 回答