问题标签 [plt-redex]

有人请用更简单的语言解释归约语义和 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 的语言，它专门用于我描述的 naturals lattice：

然后，为了替换两个归约关系slow-rr以及fast-rr我为 lambdaLVar 所拥有的关系，我可以定义几个包装器：

我对文档的理解extend-reduction-relation是，它应该重新解释 and 中的规则slow-rr，fast-rr但使用 lambdaLVar-nats。将所有这些放在一起，我尝试使用新的扩展缩减关系之一运行我拥有的测试套件：

我收到的第一件事是违反合同的投诉：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 的宏吗？

谢谢阅读！

刚开始学习PLT-Redex... 出现两个问题：

1. 我们可以使用 PLT-Redex 来模拟​​副作用吗？例如：简单的增量构造i++？
2. 怎么样thread？到目前为止介绍的所有构造都不涉及创建线程之类的东西？线程同步？它在 PLT-Redex 中可行吗（语法和缩减规则？

提前致谢，

Is there a module in Java to define a language and make the reduction of expressions as PLT/Redex module of Racket?

我正在尝试为一种语言准备语义。一些推导可能会导致“卡住”状态。我想进行测试，某些术语不能简化为“卡住”状态。是否有可能使用类似的东西来表示它test-->E？

我正在努力在 Redex 中构建一个类型系统的模型，该类型系统也具有规范实现。我想使用 redex-check 来对我的模型与实际实现进行模糊测试。

实现（带有适配器）可以采用我的抽象语法，所以我需要一种将模糊器生成的术语传递给实现的方法。有没有办法做到这一点？

我正在使用 redex-check 来验证一个模型与另一个模型，并希望查看中间（成功）结果以进行调试。最明显的方法是让 property-expr 打印给定的术语作为副作用，但这是不优雅的。还有其他方法可以查看中间的 redex-check 尝试吗？

我正在尝试定义一个 Redex 元函数，它将对列表转换为单个数字列表，如下所示：

但是，add-up不接受最后一个定义 - Redex 抱怨e_1并e_2要求省略号，尽管它们已经低于一个省略号。有没有办法将球拍取消引用应用于 Redex 中省略号的每个成员？

我相信我对等递归和等递归类型都非常了解。因此，我一直在尝试在 PLT Redex 中为 ISWIM 实现具有等递归类型的类型检查器。但是，对于我的一生，我无法弄清楚如何使类型等效起作用。其他一切都很好。

这是我的语言：

类型检查器是一种判断形式（我认为“App”的情况是错误的）：

类型等价是另一种判断形式（我把所有的责任都归咎于这段代码）：

这是我的元功能：

任何帮助将不胜感激。

我正在定义一种具有强制转换和子类型的语言，如下所示：

然后我对它定义如下判断形式：

现在，在我的归约关系中，我想写一些类似的东西

我们假设(typeof v)返回值的类型v。据我所知，Redex 库中没有类似where-judgment-holds的东西，虽然我可以通过取消引用来解决它，但如果 R​​edex 中内置了一些东西会很好。