Divergence (computer science)
In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state.[1]:377 Otherwise it is said to converge. 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.[2]
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.[3]
Denotational semantics
In denotational semantics an object function f : A → B can be modelled as a mathematical function [math]\displaystyle{ f : A \cup\{\perp\} \rightarrow B \cup\{\perp\} }[/math] where ⊥ (bottom) indicates that the object function or its argument diverges.
Concurrency theory
In the calculus of communicating sequential processes (CSP), divergence is a drastic situation where a process performs an endless series of hidden actions. For example, consider the following process, defined by CSP notation:
- [math]\displaystyle{ Clock = tick \rightarrow Clock }[/math]
The traces of this process are defined as:
- [math]\displaystyle{ \operatorname{traces}(Clock) = \{\langle\rangle, \langle tick \rangle, \langle tick,tick \rangle, \cdots \} = \{ tick \}^* }[/math]
Now, consider the following process, which conceals the tick event of the Clock process:
- [math]\displaystyle{ P= Clock \backslash tick }[/math]
By definition, P is called a divergent process.
See also
Notes
- ↑ C.A.R. Hoare (Oct 1969). "An Axiomatic Basis for Computer Programming". Communications of the ACM 12 (10): 576–583. doi:10.1145/363235.363259. http://extras.springer.com/2002/978-3-642-63970-8/DVD3/rom/pdf/Hoare_hist.pdf.
- ↑ Baader & Nipkow 1998, p. 9.
- ↑ Pierce 2002, p. 65.
References
- Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203. https://books.google.com/books?id=N7BvXVUCQk8C&q=Divergent.
- Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press.
- J. M. R. Martin and S. A. Jassim (1997). "How to Design Deadlock-Free Networks Using CSP and Verification Tools: A Tutorial Introduction" in Proceedings of the WoTUG-20.
 |  |
