発散（コンピュータサイエンス）

コンピュータサイエンスでは、計算が終了しないか、例外的な状態で終了する場合、発散すると言われます。^{[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 Clock=tick\rightarrow Clock}$$ $${\displaystyle \operatorname {traces} (Clock)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\ldots \}=\{tick\}^{*}}$$ $${\displaystyle P=時計\setminus tick}$$ ${\displaystyle P}$ ${\displaystyle \mathbf {div} }$

参照

• 無限ループ
• 終了解析

注記

1. CAR Hoare (1969年10月). 「コンピュータプログラミングの公理的基礎」(PDF) . Communications of the ACM . 12 (10): 576– 583. doi :10.1145/363235.363259. S2CID  207726175.
2. バーダー＆ニプコウ 1998年、9ページ。
3. ピアース 2002、65ページ。
4. Roscoe, AW (2010). 『並行システムの理解』 コンピュータサイエンステキスト. doi :10.1007/978-1-84882-258-0. ISBN 978-1-84882-257-3。

参考文献

• バーダー、フランツ、ニプコウ、トビアス(1998)。『用語書き換えとそのすべて』ケンブリッジ大学出版局。ISBN 9780521779203。
• ピアス、ベンジャミン・C. (2002).型とプログラミング言語. MIT出版
• JMR MartinとSA Jassim (1997)。「CSPと検証ツールを用いたデッドロックフリーネットワークの設計方法：チュートリアル入門」、WoTUG-20 Proceedingsに掲載。