racket - PLT-Redex 可以对这些特征进行建模吗？

Question

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

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

提前致谢，

Answer 1

我自己是 PLT Redex 的新手，但如果没有其他人回答：

1. 是：请参阅“为什么选择 PLT Redex？” 页面，他们给出了一个使用可变状态的例子：http ://redex.racket-lang.org/why-redex.html

2. 我应该这么认为，因为他们为 1 提供的解决方案似乎很笼统。您的程序状态将包括许多术语，每个术语都是一个线程的状态。创建一个线程只需将一个新术语添加到列表中。同步比较棘手，尽管原则上应该可以在 PLT Redex 中对 π 演算进行建模，然后你就拥有了你可能想要的所有线程原语等等。我还不能告诉你这在 Redex 中会是什么样子，但看起来所有的工具都在那里。