{{Short description|Computation which does not terminate or terminates in an exceptional state}} {{Redirect|Terminating|other uses|Termination (disambiguation){{!}}Termination}} In computer science, a computation is said to '''diverge''' if it does not terminate or terminates in an exceptional state.<ref>{{cite journal | url=http://extras.springer.com/2002/978-3-642-63970-8/DVD3/rom/pdf/Hoare_hist.pdf | author=C.A.R. Hoare | title=An Axiomatic Basis for Computer Programming | journal=Communications of the ACM | volume=12 | number=10 | pages=576&ndash;583 | date=Oct 1969 | doi=10.1145/363235.363259 | s2cid=207726175 }}</ref>{{rp|377}} Otherwise it is said to '''converge'''.{{cn|date=March 2025}} In domains where computations are expected to be infinite, such as process calculi, a computation is said to diverge if it fails to be productive (i.e. to continue producing an action within a finite amount of time).

== Definitions == Various subfields of computer science use varying, but mathematically precise, definitions of what it means for a computation to converge or diverge.

=== Rewriting === In abstract rewriting, an abstract rewriting system is called convergent if it is both confluent and terminating.{{sfn|Baader|Nipkow|1998|p=9}}

The notation ''t'' ↓ ''n'' means that ''t'' reduces to normal form ''n'' in zero or more reductions, ''t''↓ means ''t'' reduces to some normal form in zero or more reductions, and ''t''↑ means ''t'' does not reduce to a normal form; the latter is impossible in a terminating rewriting system.

In the lambda calculus an expression is divergent if it has no normal form.{{sfn|Pierce|2002|p=65}}

=== Denotational semantics === In denotational semantics an object function ''f'' : ''A'' → ''B'' can be modelled as a mathematical function <math> f : A \cup\{\perp\} \rightarrow B \cup\{\perp\}</math> where ⊥ (bottom) indicates that the object function or its argument diverges.

=== Concurrency theory === {{See also|Communicating sequential processes#Failures/divergences model}}

In the calculus of communicating sequential processes (CSP), divergence occurs when a process performs an endless series of hidden actions.<ref name="ucs">{{cite book |last1=Roscoe |first1=A.W. |date=2010 |title=Understanding Concurrent Systems |series=Texts in Computer Science |doi=10.1007/978-1-84882-258-0 |isbn=978-1-84882-257-3 }}</ref> For example, consider the following process, defined by CSP notation: <math display="block">Clock = tick \rightarrow Clock</math> The traces of this process are defined as: <math display="block">\operatorname{traces}(Clock) = \{\langle\rangle, \langle tick \rangle, \langle tick,tick \rangle, \ldots \} = \{ tick \}^*</math> Now, consider the following process, which hides the ''tick'' event of the ''Clock'' process: <math display="block">P = Clock \setminus tick</math> As <math>P</math> cannot do anything other than perform hidden actions forever, it is equivalent to the process that does nothing but diverge, denoted <math>\mathbf{div}</math>. One semantic model of CSP is the failures-divergences model, which refines the stable failures model by distinguishing processes based on the sets of traces after which they can diverge.

== See also == * Infinite loop * Termination analysis

== Notes == {{reflist|2}}

== References == * {{cite book|first1=Franz|last1=Baader|authorlink1=Franz Baader|first2=Tobias|last2=Nipkow|authorlink2=Tobias Nipkow|title=Term Rewriting and All That|year=1998|publisher=Cambridge University Press|url=https://books.google.com/books?id=N7BvXVUCQk8C&q=Divergent|isbn=9780521779203}} * {{cite book|first=Benjamin C.|last=Pierce|author-link=Benjamin C. Pierce|title=Types and Programming Languages|year=2002|publisher=MIT Press|title-link=Types and Programming Languages}} * J. M. R. Martin and S. A. Jassim (1997). "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.19.1615&rep=rep1&type=pdf How to Design Deadlock-Free Networks Using CSP and Verification Tools: A Tutorial Introduction]" in ''Proceedings of the WoTUG-20''.

Category:Programming language theory Category:Process (computing) Category:Rewriting systems Category:Lambda calculus Category:Denotational semantics

{{comp-sci-stub}}