我正在尝试构建 redex - 不幸的是它失败了：

但我安装了这个库：

我从https://github.com/google/double-conversion安装它

所以昨晚我在Ubuntu上安装了redex，一切都很顺利。我今天在我的 Mac 上设置它时遇到问题。

我在这autoreconf -ivf && ./configure && make && make install一步遇到了 3 个错误。

Please install double-conversion library

Please install google-glog library

Please install google-gflags library

我不会一下子得到这些。我得到了第一个，所以我在这里遵循了解决方案，但这没有用，所以我只是从 configure.ac 文件中删除了该检查。这导致了第二个错误，然后导致了第三个错误。

我不确定为什么会发生这种情况，我按照与昨晚完全相同的步骤进行操作。

有什么建议么？

所以我遵循了拉尔夫的建议，现在我遇到了一个不同的错误 -

在http://fbredex.com/的 Redex 页面中有一个非常好的说明。

我按照说明进行操作，但有两个步骤出现问题。

1.我对第一个命令的运行没有问题（我的操作系统是Ubuntu）

2. 我在笔记本电脑的某个地方克隆了愚蠢的回购

3. 我去目录$ cd android/projects/folly/folly/

4. 我跑了git submodule update --init，但什么也没发生。我什至在其中运行此命令，$ cd android/projects/folly/但也没有任何反应。

5. 我跑autoreconf -ivf && ./configure && make && make install。似乎有效，因为我看到过程大约需要一两分钟，并且打印出很多 og 消息。

6. 我将示例 .apk 文件复制/粘贴到我的桌面并运行redex ~/Desktop/my_android_app.apk -o ~/Desktop/my_android_app-redexed.apk. 但是，我在终端上收到此消息。

   未找到命令“redex”，您的意思是：来自包“redet”（universe）的命令“redet”redex：找不到命令

当我在/home/hesam/android/projects/folly/follyor中时，我运行了上面的命令/home/hesam/android/projects/folly/。但我得到相同的输出。

更新

我克隆了 Redex repo 并遵循了 Bert 的指示。它有效，我可以通过运行看到正在发生的事情git submodule update --init。所以感谢伯特。但是，我在autoreconf -ivf && ./configure && make && make install命令结束时出错。

请查看以下输出：

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

Hutton 在 Haskell 中编程 说：

具有函数形式的表达式应用于一个或多个可以通过执行应用程序“减少”的参数，称为可简化表达式，或简称 redex。

是一个可简化的表达式，即 redex 完全

• 一个函数应用程序，其中该函数不是另一个函数应用程序的结果，

• 等效地，函数是函数名还是 lambda 表达式的函数应用程序？

以上两点中的任何一点是否都是对我之前在最外层评估策略如何评估函数的部分应用和柯里化函数的应用的问题的答案？

我已经将字典定义为 BNF 语法中的这个判断：

意思是，字典是空的，或（任何布尔值）或此类对的列表。

如果我想创建一个映射，说“一个真实的”，我该怎么做？

如果我做

它只是创建一个新的 d，不映射到先前定义的判断 d。

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

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

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

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

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

假设我在 Redex 中定义了以下内容：

现在，我认为该表达式的(λ y x) x意思是：

用（外大括号）替换出现的yin x（上述表达式中的大括号内）。x既然没有yin x，答案应该是 just x。然后(λ y x) x y应该返回x y。但：

为什么它返回一个函数？是什么y<<0>>意思？我误会了term (substitute ..)吗？

我也不明白这个结果：

有人可以帮我破译这个吗？我是 Racket/Redex 的新手。

我有judgement以下合同：

当我运行这个：

我回来了：

#t

#t

#t

. . down：判断输入值与其合约不匹配；（由_表示的未知输出值）合约：（down Γ e Γ e）值：（down empty lam1^* _ _）

但这没有意义，因为我redex-match?上面明明用过来测试：

• 那empty匹配Γ
• 那lam1^*匹配e
• 而且那lam1^*匹配z。

我错过了什么？#:contract除了匹配之外，还有更多的含义Γ e Γ e吗？

在查看 PLT redex 时，我想玩简化规则；所以我为布尔值定义了这个最小的语言：

我想简化一个链，(not (not ...))所以我扩展了语言来处理上下文并定义了一个归约关系来简化not：

现在我想将我的语言扩展到布尔方程并允许not在方程的每一边进行简化，所以我定义了：

希望：

会做的事情。but no：red1可以减少(not (not (not F)))))但不能减少(= (not T) F)))

我在这里做了什么很傻的事情吗？