Lin*_*per 12 formal-semantics racket plt-redex
这是一个一直困扰着我的问题,我想知道这里是否有人可以提供帮助.
我有一个名为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的语言,它专门用于我描述的自然格点:
;; 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个失败了.也许不出所料,所有失败的程序都是以某种方式使用自然数值LVars的程序.(其余的是"纯"程序,根本不与LVars存储交互.)因此,失败的测试正是使用扩展语法的测试.
所以我一直跟着兔子洞,似乎Redex希望我将所有现有的判断形式和元函数扩展为与lambdaLVar-nats而不是lambdaLVar相关联.这是有道理的,据我所知,它似乎对于判断形式是可行的,但是对于元函数我遇到了麻烦:我希望新的元函数重载同名的旧元函数(因为现有的判断形式正在使用它)似乎没有办法做到这一点.如果我必须重命名元函数,它就会失败,因为无论如何我都要编写全新的判断形式.我想我想要的是一种元函数调用的后期绑定!
我的问题简而言之: Redex中是否有任何方式以我想要的方式参数化语言的定义,或者以一种能够满足我想要的方式扩展语言的定义？我最终只需要编写生成Redex的宏吗？
谢谢阅读!
我询问了 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 能尽快获得模块，但与此同时，这似乎运行良好。