问题标签 [plt-redex]

定义语义的常用方法是（例如）：

例如，考虑

然后我们可以定义归约关系

这是执行此操作的自然方式，因为它避免了必须为 3 个失败案例（数字字符串、字符串编号、字符串字符串）中的每一个编写单独的匹配器。但是，它会产生像这样运行它的问题：

（正确地）显示它可以让你减少到错误或数字 4。有没有办法制作一个“例外”模式来避免必须检查所有组成案例？

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

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

完全可以在不使用评估上下文的情况下为我的语言编写评估规则。我的语义完全是按值调用，并且不允许在 lambdas 中向前推进该术语。尽管如此，我看到的所有资源都以某种方式使用缩减上下文。是否有充分的理由使用我缺少的上下文？

我正在关注 Redex 的amb 教程，同时为类型化算术表达式构建模型，如 Pierce 的类型和编程语言中所见。

我已经为这种小语言定义了语法和类型系统，但是我很难定义它的小步语义。在我解决这些问题之前，让我先介绍一下我目前得到的定义。

首先，我定义了语言的语法。

接下来，我毫无问题地定义了类型系统。

据我了解，我们需要使用评估上下文来定义语义。所以我的下一步是为语言定义这样的上下文和价值观。

非终结C符代表上下文、NV数值、BV布尔值和V值。使用值的定义，我定义了一个用于测试表达式是否为值的函数。

使用这个设置，我尝试为这种语言定义操作语义。在 Pierce 的书中，这样的语义（没有评估上下文）如下：

为了使用评估上下文来表达这样的语义，我删除了 rules E-suc、和 ，E-pred并定义了一个在表达式上下文中步进的规则：E-izeroE-if

据我了解，我们不需要在 redex 中表示这样的上下文规则。因此，我将这种语言的语义定义为：

现在，我们遇到了问题：当我试图执行

Racket 返回以下错误信息：

当然，我在做一些愚蠢的事情，但我不知道是什么。有人可以帮我解决这个问题吗？

我是球拍新手，我对使用 redex 特别感兴趣。我已经为 Pierce 的类型和编程语言书中找到的类型化算术表达式做了一个小模型。代码位于以下要点：https ://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0

当我尝试测试进度和保存等属性时，我想检查测试覆盖了多少代码，因此我运行了以下命令，如 amb 教程中所示：

但是，它返回

这意味着永远不会执行任何语义规则，对吗？我认为问题在于球拍正在生成不一定正确输入的随机术语。

我的问题：有没有办法指定如何只生成类型良好的术语？

编写一个程序来销毁我的访问控制模型中的对象并模拟每种情况。这是我的代码。

这是测试代码。

当我想销毁 st1 中的一个对象时，我测试如下：

我不断收到此错误：

“矩阵”是我要销毁包括“Obj”在内的任何列表的矩阵。“Obj”可以是 o1 或 o2。我将“M_1”放入矩阵。我想把 "st1" 的 "m1" 放入 "M_1" "m1" 已经定义好了。它不应该是空的。那么为什么会发生这个错误呢？非常感谢！！

我想形式化一个基于 PLT Redex 和 Scheme 的简单中国墙模型。但是当我使用“步进器”工具来可视化每个不同的状态时。错误发生了，我以前从未见过。

我没有理想的做什么。这部分似乎有问题。

但是，当我删除有关“访问读取”的部分时，它会起作用。这很奇怪，因为“read”和“write”部分的唯一区别是拼写的不同。它们的子程序都返回“#true”或“#false”。所以就我而言，这个错误与子程序无关。所以我很困惑，不知道为什么。甚至之前没有见过这个错误，也没有理想。

附上我的代码。

也许这是一个愚蠢的错误。但我需要一些帮助。非常感谢！

我有一种用 PLT-Redex 定义的语言，它具有（动态）mixin 类型。表达式如下所示：

语言的评估是通过评估上下文和归约关系来完成的。

我的归约关系目前仅针对字段访问（lkp）定义，它将对 mixin 的查找归约到其值。

我对我的元函数 ( fvalue) 进行了测试，以验证它们是否有效。然而，redex 告诉我，我的归约关系以许多不同的方式映射到一个洞。我是否评论不同版本的评估上下文无关紧要new C ...。错误来自这个地方。

如何调试（或修复）问题？通常，我使用 Emacs 和 Racket 模式进行开发，或者使用 DrRacket。问题是当使用宏步进器时，错误会从一个步骤抛出到另一个步骤。如果我能看到它捕获的孔甚至了解它失败的地方，那就太好了。所以我也许明白为什么它完全失败了。

我最近开始使用 PLT-Redex，我想知道是否有人可以给我一些关于如何在 Racket 中实现 let* 表达式的指示。

现在我可以像这样写简单的 let 表达式

但是，如果我尝试如下复杂的 let 表达式（请参阅我的代码中的测试 4 和 5），我会得到多个输出值：

我想像这样重写上面的表达式

以下是我当前的 Redex 实施，以防有人想提供帮助。

在此先感谢温贝托