termination (computer science)
   HOME

TheInfoList



OR:

In
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
, a computation is said to diverge if it does not terminate or terminates in an exceptional
state State may refer to: Arts, entertainment, and media Literature * ''State Magazine'', a monthly magazine published by the U.S. Department of State * ''The State'' (newspaper), a daily newspaper in Columbia, South Carolina, United States * ''Our S ...
. Otherwise it is said to converge. In domains where computations are expected to be infinite, such as
process calculi In computer science, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and ...
, 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 In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a Formalism (mathematics), formalism that captures the quintessential notion and ...
, an
abstract rewriting system In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting s ...
is called convergent if it is both
confluent In geography, a confluence (also: ''conflux'') occurs where two or more flowing bodies of water join to form a single channel. A confluence can occur in several configurations: at the point where a tributary joins a larger river (main stem); o ...
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 In mathematics, a function from a set to a set assigns to each element of exactly one element of .; the words map, mapping, transformation, correspondence, and operator are often used synonymously. The set is called the domain of the functi ...
f : A \cup\ \rightarrow B \cup\ where ⊥ (
bottom Bottom may refer to: Anatomy and sex * Bottom (BDSM), the partner in a BDSM who takes the passive, receiving, or obedient role, to that of the top or dominant * Bottom (sex), a term used by gay couples and BDSM * Buttocks or bottom, part of th ...
) indicates that the object function or its argument diverges.


Concurrency theory

In the calculus of
communicating sequential processes In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or ...
, 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: :Clock = tick \rightarrow Clock The traces of this process are defined as: :\operatorname(Clock) = \ = \^* Now, consider the following process, which conceals the ''tick'' event of the ''Clock'' process: :P= Clock \backslash tick By definition, ''P'' is called a divergent process.


See also

*
Infinite loop In computer programming, an infinite loop (or endless loop) is a sequence of instructions that, as written, will continue endlessly, unless an external intervention occurs ("pull the plug"). It may be intentional. Overview This differs from: * ...
*
Termination analysis In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for ''each'' input. This means to determine whether the input program computes a ''total'' function. It is c ...


Notes


References

* * * 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''. Programming language theory Process (computing) Rewriting systems Lambda calculus Denotational semantics {{comp-sci-stub