在 Scala 中实现 CSP（通信顺序进程）答案

【问题标题】：Implementing CSP (Communicating Sequential Processes) in Scala在 Scala 中实现 CSP（通信顺序进程）
【发布时间】：2013-06-19 20:43:16
【问题描述】：

我正在尝试在 Scala 中为“CSP”实现解析器和语义。我已经实现了 parser ，现在我正忙于研究语言的语义部分。我对并发系统和非确定性选择的世界完全陌生。所以这是我的问题：

我想按照说明实现“非确定性选择”和“接口并行” here.

我现在可以理解该过程，但在涉及非确定性时我无法直截了当。我需要一个好的数据类型来在 Scala 中实现这一点，我正在考虑将所有进程放在一个列表中，然后随机化该列表，然后从修改后的列表中选择一个元素。但这对我来说听起来不是那么不确定。

以前有没有人经历过这个问题并且知道一个好的算法？

【问题讨论】：

标签： list scala functional-programming scala-collections

【解决方案1】：

我对 CSP 的理解非常有限，CSP 运算符对应于以下 Haskell 类型：

-- Prefixing corresponds to functions
x :: A
P :: B
x -> P :: A -> C

-- Choice corresponds to product
P :: A
Q :: B
P □ Q :: (A, B)

-- Non-determinism corresponds to sum
-- I don't know how to make the non-determinism symbol, so I use (△)
P :: A
Q :: B
(P △ B) :: Either A B

然后您可以使用代数同构来减少 CSP 表达式。使用维基百科的例子：

(coin -> STOP) □ (card -> STOP)

-- translates to the following Haskell type:
(coin -> Stop, card Stop)

-- which is algebraically isomorphic to:
(Either coin card -> Stop)

-- translates in reverse back to CSP:
coin □ card -> STOP

另外，我认为维基百科的一个例子是错误的（或者我错了）。我相信这个表达式应该简化为：

(a -> a -> STOP) □ (a -> b -> STOP)

-- translates to the following Haskell type:
(a -> a -> STOP, a -> b -> STOP)

-- which is algebraically isomorphic to:
a -> Either a b -> STOP

-- translates in reverse back to CSP:
a -> (a △ b) -> STOP

不过，我还没有弄清楚接口并行的等价物。它似乎不符合一个优雅的概念。

【讨论】：

【解决方案2】：

这是一个高级主题。解析方面很容易。编写正确的并发原语非常困难，几乎可以肯定需要使用 FDR 等工具进行形式验证。

如果您只对编写表达式解析器部分感兴趣，而不是并发原语，您可能更愿意在 JCSP 的基础上进行构建，它已经在 Java API 中提供了这些原语。此 (UKC) 的作者使用形式验证来验证其组件，特别是通道和替代（选择）部分。

【讨论】：