Divergence (computer science)

In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge.[citation needed] 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.

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 f:A∪{⊥}→B∪{⊥} 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: Clock=tick→Clock The traces of this process are defined as: traces⁡(Clock)={⟨⟩,⟨tick⟩,⟨tick,tick⟩,…}={tick}∗ Now, consider the following process, which hides the tick event of the Clock process: P=Clock∖tick As P cannot do anything other than perform hidden actions forever, it is equivalent to the process that does nothing but diverge, denoted 𝐝𝐢𝐯. 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

Notes

References

  • Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203.
  • Hoare, C.A.R. (October 1969). "An Axiomatic Basis for Computer Programming" (PDF). Communications of the ACM. 12 (10): 576–583. doi:10.1145/363235.363259. S2CID 207726175.
  • Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press.
  • Roscoe, A.W. (2010). Understanding Concurrent Systems. Texts in Computer Science. doi:10.1007/978-1-84882-258-0. ISBN 978-1-84882-257-3.

Bibliography

Martin, J. M. R.; Jassim, S. A. (1997). "How to Design Deadlock-Free Networks Using CSP and Verification Tools: A Tutorial Introduction". In Bakkers, André W. P. (ed.). Parallel Programming and Java: Proceedings of WoTUG-20. WoTUG-20. Amsterdam: IOS Press. Archived from the original on 8 July 2022.{{cite conference}}: CS1 maint: miscellaneous url (link)