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 中会是什么样子，但看起来所有的工具都在那里。