进程演算

在计算机科学中，进程演算（或进程代数）是用于形式化建模并发系统的多种相关方法。进程演算提供了具体描述多个独立代理人程序或者是多个进程之间交互、通信、同步的方法，其中包含了对进程操作和分析的描述、以及证明形式化推导进程之间存在等价关系（例如：双向模拟的运用）的代数法则。关于进程演算的典例主要包括CSP、CCS、ACP，和LOTOS。最近新增的演算包括π演算，环境演算，PEPA，融合演算和联接演算。

基本特征

虽然目前为止的进程演算种类繁多（包括含有随机行为，定时信息，专门研究基础的的交互的特例），但是所有的进程演算都有以下几个共同特征：

• 在独立进程之间进行通信（消息传递）时比修改共享变量更能体现交互性；
• 使用基本元和能合并这些基本元的操作符的集合来描述进程和系统；
• 定义了能通过方程式推理方法推导出进程表达式的操作符的代数法则。

数学表示

定义进程演算，起步于定义一组“名字”（或通道），它们的用途是提供通信手段。在许多实现中，通道有优秀的内部结构以提高效率，不过这是从理论模型中抽象出来的。除命名之外，需要从之前的进程中运用一个方法来构建新的进程，其中的基础运算符，总是以某些形式或其他方式呈现，包括：

• 进程的并行组合；
• 详述用于传送和接受数据的通道；
• 交互操作的顺序化；
• 隐藏交互点；
• 递归或进程复制。

并行组合

两个进程P和Q的并行组合，通常写做P|Q，它是将进程演算从运算序列模型中识别出来的关键基本式。并行组合允许P和Q相互独立并且同时进行运算。但它也允许进行交互，那就是同步及P通过两者共享的通道将信息流传递至Q（或反之亦然）。至关重要的是，代理或进程可以一次连接到多个通道。通道可以是同步或异步的。在同步通道的情况下，发送信息的代理需要等待至另一个代理接收到信息。异步通道不要求任何的同步。在一些进程演算（特别是π演算）中，它们的通道本身可以作为信息通过（其他的）通道发送，允许进程相互连接的拓扑结构发生改变。一些进程演算也允许通道在执行运算的过程中被创建。

通信

交互可以作为（但不总是）有向的信息流。也就是说，输入和输出能作为双重交互基本元被区分。进行这种区分的进程演算通常定义一个输入操作符（e.g X(v)）和一个输出操作符（e.g X<y>）,这两者作为一个以双重交互基本元进行同步的交互点（这里是X）。 信息应该被交换，它将从输出流向输入进程。输出基本元将指定要发送的数据。在X<y>中，这个数据是y。类似的，如果一个输入想要接受数据，当数据到达时，一个或多个绑定变量将作为占位符来替换数据。在X(v)中，v扮演那个角色。在交互中可以交换的数据类型的选择是区分不同进程演算的关键特征之一。

顺序组合

有时交互必须在时间上有序。例如，它可能要求指定算法：首先在X上接收数据，然后在y上传送数据。顺序组合可用于这些目的。在其他运算模型中它非常有名。在进程演算中，序列化运算符通常与输入或输出或两者结合。例如，进程X（v）.P将等待（数据）输入到X上，只有当这个输入完成时进程P才会被激活，通过X接受的数据代替标识符v。

归约语义

归约法则运用的关键，包含了进程演算的计算实质，单独的依据并行组合、顺序化、输入和输出。演算间的归约细节不同，但是实质保持大致相同。通用的归约法则是：$x\langle y\rangle \cdot P\;\vert \;x(v)\cdot Q\longrightarrow P\;\vert \;Q[^{y}\!/\!_{v}]$。

该归约规则的解释是：

1. 进程$x\langle y\rangle \cdot P$发送信息，即此处的y，沿着双向的通道X，进程$x(v)\cdot Q$接受通道X上的信息。
2. 一旦信息被发送，$x\langle y\rangle \cdot P$就成为了进程P，而$x(v)\cdot Q$就变成了进程$Q[^{y}\!/\!_{v}]$，即Q与占位符v取代y，接受到了X上的数据。

P这类进程涉及的输出运算符的连续性本质上影响了演算的性质。

隐藏

进程不限制能给出交互点的连接数量，但是交互点允许相互干扰（即交互作用）。对于一个简洁，微小和组合式的综合系统，抗干扰的能力是至关重要的。当组合代理并行时，隐藏操作允许控制交互点之间形成的连接。隐藏能用多种多样的方式表示。例如，在π演算中，隐藏一个P中的命名X可以被描述为（v X）P,然而在CSP中它可能被写做P\{X}.

递归与复制

迄今提出的操作仅描述有限的交互,也因此不满足包含非终止行为的完全可计算性。递归和复制允许以有限步描述无限的行为。递归具有的连续性领域是众所周知的，复制！P可以被理解为缩写可数集无限数的P进程的并行组合：

$!P=P\mid !P$

空进程

进程演算通常还包含没有交互点的空进程（多样的表示为nil，0，STOP，δ或一些其他的适当符号），它是完全无活动的，并且它唯一的用途表现在作为归纳锚点置于可以被生成的活跃进程之上。 离散和连续进程代数 已经针对离散时间和连续时间研究过进程代数（真实时间和稠密时间）。

历史发展

在20世纪上半叶，提出了各种形式论来获得可计算函数的非正式概念，μ递归函数，图灵机和lambda演算可能是如今最著名的例子，令人惊讶的事实是，在它们可以相互编码的意义上，它们彼此之间基本上是等同的，支撑着Church-Turing论题。另一个难得的对它们共同特征的评论是：它们几乎都是作为最容易理解的连续计算模型，随后的计算机科学的整合需要更细微的计算概念的表达，特别是并行和通信的明确表达。作为并发模型的进程演算，1962年提出的Petri网，以及1973年提出的演员模型，就是在这条探究路线上涌现的。进程演算的研究开始于1973年至1980年期间，与Robin Milner对通信系统演算(CCS)的开创性工作有关。C.A.R. Hoare的通信顺序进程（CSP）首次出现于1978年，随后直到20世纪80年代初期才被开发为一个完整的进程演算。CCS和CSP在发展的过程中，发生了许多思想上的交叉。在1982年Jan Bergstra和Jan Willem Klop开始致力于研究后来被熟知的通信处理代数（ACP），并且提出了术语“进程代数”来描述他们的工作。CCS、CSP和ACP构成了进程演算的三个重要的分支：其余大多数的进程演算的根源都可以追溯到这三个演算的其中之一。

现今研究

研究的进程演算多种多样但不是全部都符合这里描述的范例。最突出的例子可能是灰箱演算。作为进程演算研究预期的热门领域，目前对进程演算的研究集中在以下问题上：

• 发展新的进程演算以更好的对运算情况进行建模。
• 为给定的进程演算找到良好性质的演算进行运算。这是有价值的，因为
  • 大多数演算相当的混乱，这样的情况是相当普遍的，对于任意进程来说都描述不了太多；
  • 计算程式很少耗尽整个演算。相反，它们只使用在形式上受限制的进程。约束进程的模型主要是通过表征系统的方式来研究。
• 遵循Hoare逻辑的思想，进程逻辑允许人们推理有关进程的（实质上的）任意属性；
• 行为理论：两个进程相同意味着什么意思？我们如何确定两个进程是否不同？我们可以找到进程的等价类的典型吗？通常，如果没有上下文（即并行运行的其他进程）可以检测到差异，则认为进程是相同的。不幸的是，使得这样的直觉知识变得准确是很难的，大多产生难处理的相同特征（在大多数情况下也必须是不可判定的，作为停机问题的结果）。互模拟是有助于对进程等价的推理的技术工具。
• 进程的表达性。编程经验表明，某些问题在某些语言中比在其他语言中更容易解决。这种现象要求演算建模运算具有比Church-Turing论文提供的表达性更精确的特征。这样做的一种方法是考虑两种形式论之间的编码，并看看编码可以潜在地保存什么属性。可以保存的属性越多，编码的表达能力就越强。对于进程演算，著名的结果是同步的π演算比其异步变体更具表达性，具有与高阶π演算相同的表达能力，但小于灰箱演算。
• 使用进程演算来对生物系统建模（随机π演算，BioAmbients，Beta Binder，BioPEPA，Brane calculus）。它认为提供一些组合性的进程理论工具能帮助生物学家更加正规的组织他们的知识。

软件实现

进程代数的想法提出后已经产生了许多工具，包括：

• CADP
• 并行工具台
• mCRL2工具集

与其他并发模型的关系

历史独异点是能够一般的表示独立通信进程历史的自由对象。进程演算是形式语言以一致的方式应用于历史独异点之后得到的。即是说，一个历史独异点只能够记录事件的顺序，带有同步性，但是这不表明允许状态的转变。因此，进程演算之于历史独异点相当于形式语言之于自由独异点（形式语言是Kleene star产生的字符所组成的所有可能的有限长度字符串的子集）。

使用通道进行通信是将进程演算与其它并发模型区分开的特征之一，例如Petri网和演员模型（参见演员模型和进程演算条目）在进程演算中包含通道的基本动机之一是实现某些代数方法，从而让用代数方法来推导进程变得简单。