标签: 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 …

有人请用简单的语言解释缩减语义和PLT Redex的用法.

谢谢.

每次我在 PLT redex 中定义一种语言时，我都需要手动定义一个（避免捕获）替换函数。例如，这个模型没有完成，因为subst没有定义：

#lang racket/base
(require redex/reduction-semantics)

(define-language ?
  [V ::= x (? x M)]
  [M ::= (M M) V]
  [C ::= hole (V C) (C M)]
  [x ::= variable-not-otherwise-mentioned])

(define -->?
  (reduction-relation ?
    [--> (in-hole C ((? x M) V))
         (in-hole C (subst M x V))]))

但定义subst是显而易见的。PLT redex 可以自动处理替换吗？