ダイバージェンス（コンピュータサイエンス）

コンピュータサイエンスでは、計算が終了しないか、例外的な状態で終了する場合、その計算は発散すると言われます。^{[1] : 377}それ以外の場合は収束すると言われます。プロセス計算など、計算が無限であることが予想される分野では、計算が生産的でない場合（つまり、有限の時間内にアクションを生成し続けることができない場合）、その計算は発散すると言われます。

コンピュータ サイエンスのさまざまなサブフィールドでは、計算が収束または発散するという意味について、さまざまな、しかし数学的に正確な定義を使用します。

抽象書き換えにおいて、抽象書き換えシステムが合流性と停止性の両方を備えている場合、その抽象書き換えシステムは収束的であると呼ばれます。^[2]

t ↓ n という表記は、 tが 0 回以上の縮約で正規形nに縮約されることを意味し、t ↓ はtが 0 回以上の縮約で何らかの正規形に縮約されることを意味し、t ↑ はt が正規形に縮約されないことを意味します。後者は停止性書き換えシステムでは不可能です。

ラムダ計算では、式が正規形を持たない場合、その式は発散するという。^[3]

表示的意味論では、オブジェクト関数 f  : A → Bは数学関数 としてモデル化することができ、⊥ (下) はオブジェクト関数またはその引数が発散することを示します。 ${\displaystyle f:A\cup \{\perp \}\rightarrow B\cup \{\perp \}}$

通信逐次プロセス計算(CSP) では、プロセスが隠れたアクションを際限なく実行するときに発散が発生します。^[4]たとえば、CSP 表記法で定義された次のプロセスを考えてみましょう。 このプロセスのトレースは次のように定義されます。 ここで、 Clockプロセスのtickイベント を非表示にする次のプロセスを考えてみましょう。 は隠れたアクションを永久に実行する以外は何もできない ため、 で表される発散以外の何も行わないプロセスと同等です。 CSP のセマンティック モデルの 1 つに、失敗発散モデルがあります。これは、プロセスが発散できるトレースのセットに基づいてプロセスを区別することで、安定した失敗モデルを改良したものです。 $${\displaystyle 時計=tick\rightarrow 時計}$$$${\displaystyle \operatorname {traces} (Clock)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\ldots \}=\{tick\}^{*}}$$$${\displaystyle P=Clock\setminus tick}$$${\displaystyle P}$${\displaystyle \mathbf {div} }$

• 無限ループ
• 終了分析

• バーダー、フランツ、ニプコウ、トビアス（1998）。用語の書き換えとそのすべて。ケンブリッジ大学出版局。ISBN 9780521779203。
• ピアス、ベンジャミン C. (2002)。型とプログラミング言語。MIT プレス。
• JMR Martin および SA Jassim (1997)。「CSP および検証ツールを使用してデッドロックのないネットワークを設計する方法: チュートリアルの紹介」、WoTUG-20 の議事録。