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.[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

edit

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

Rewriting

edit

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

The notation tn 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

edit

In denotational semantics an object function f : AB can be modelled as a mathematical function where ⊥ (bottom) indicates that the object function or its argument diverges.

Concurrency theory

edit

In the calculus of communicating sequential processes (CSP), divergence occurs when a process performs an endless series of hidden actions.[4] For example, consider the following process, defined by CSP notation: The traces of this process are defined as: Now, consider the following process, which hides the tick event of the Clock process: As 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

edit

Notes

edit
  1. ^ C.A.R. Hoare (Oct 1969). "An Axiomatic Basis for Computer Programming" (PDF). Communications of the ACM. 12 (10): 576–583. doi:10.1145/363235.363259. S2CID 207726175.
  2. ^ Baader & Nipkow 1998, p. 9.
  3. ^ Pierce 2002, p. 65.
  4. ^ 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.

References

edit


📚 Artikel Terkait di Wikipedia

Evaluation strategy

call by value will evaluate it regardless. If the argument is a non-terminating computation, the advantage is enormous. However, when the function argument

Fixed-point combinator

computational point of view, applying a fixed-point combinator to an identity function or an idempotent function typically results in non-terminating

Corecursion

as it allows encoding potentially non-terminating computations in a context where every function must terminate. It is supported by theorem provers

Software incompatibility

calls Q with y set to 100, then using Q' instead will lead to a non-terminating computation. If we assume further that f(x) has a numeric value, then component

Non-well-founded set theory

non-well-founded sets has been applied in the logical modelling of non-terminating computational processes in computer science (process algebra and final semantics)

Function type

sufficient either if the programming language allows writing non-terminating computations (which is the case if the programming language is Turing complete)

Theory of computation

mathematics, the theory of computation is the branch that deals with what problems can be solved on a model of computation using an algorithm, how efficiently

Full-employment theorem

compiler, as such a proof for the compiler would have to detect non-terminating computations and reduce them to a one-instruction infinite loop. Thus, the