Divergence (computer science)

Rewriting

In abstract rewriting, an abstract rewriting system is called convergent if it is both confluent and terminating.

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.

Denotational semantics

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

Concurrency theory

In the calculus of communicating sequential processes (CSP), divergence occurs when a process performs an endless series of hidden actions. For example, consider the following process, defined by CSP notation: $${\displaystyle Clock=tick\rightarrow Clock}$$ The traces of this process are defined as: $${\displaystyle \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: $${\displaystyle P=Clock\setminus tick}$$ As ${\displaystyle P}$ cannot do anything other than perform hidden actions forever, it is equivalent to the process that does nothing but diverge, denoted ${\displaystyle \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.