Divergence (computer science)

{{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.{{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–583 | date=Oct 1969 | doi=10.1145/363235.363259 | s2cid=207726175 }}{{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 $f : A \cup\{\perp\} \rightarrow B \cup\{\perp\}$ 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.{{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 }} For example, consider the following process, defined by CSP notation:

$Clock = tick \rightarrow Clock$

The traces of this process are defined as:

$\operatorname{traces}(Clock) = \{\langle\rangle, \langle tick \rangle, \langle tick,tick \rangle, \ldots \} = \{ tick \}^*$

Now, consider the following process, which hides the tick event of the Clock process:

$P = Clock \setminus tick$

As $P$ cannot do anything other than perform hidden actions forever, it is equivalent to the process that does nothing but diverge, denoted $\mathbf{div}$ . 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.

Notes

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