Divergence (computer science)

<h2 id="definitions">Definitions</h2>
<p>Various subfields of computer science use varying, but mathematically precise, definitions of what it means for a computation to converge or diverge.
</p>
<h3>Rewriting</h3>
<p>In <a href="/facts/Abstract_rewriting/FNIYHu2k">abstract rewriting</a>, an <a href="/facts/Abstract_rewriting_system/FNIYHu2k">abstract rewriting system</a> is called convergent if it is both <a href="/facts/Confluent_(abstract_rewriting)/kzGnhPVV">confluent</a> and <a href="/facts/Abstract_rewriting_system/FNIYHu2k">terminating</a>.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a>
</p><p>The notation <i>t</i> ↓ <i>n</i> means that <i>t</i> reduces to normal form <i>n</i> in zero or more <a href="/facts/Reduction_(abstract_rewriting)/tTVTXTKN">reductions</a>, <i>t</i>↓ means <i>t</i> reduces to some normal form in zero or more reductions, and <i>t</i>↑ means <i>t</i> does not reduce to a normal form; the latter is impossible in a terminating rewriting system.
</p><p>In the <a href="/facts/Lambda_calculus/DaD3RuQ4">lambda calculus</a> an expression is divergent if it has no <a href="/facts/Normal_form_(abstract_rewriting)/JERru3Fx">normal form</a>.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a>
</p>
<h3>Denotational semantics</h3>
<p>In <a href="/facts/Denotational_semantics/yRs3ygRA">denotational semantics</a> an <a href="/facts/Function_(computer_science)/9vFJrg0A">object function</a> <i>f</i> : <i>A</i> → <i>B</i> can be modelled as a <a href="/facts/Function_(mathematics)/CdReEKCh">mathematical function</a> 
  
    
      
        f
        :
        A
        ∪
        {
        ⊥
        }
        →
        B
        ∪
        {
        ⊥
        }
      
    
    {\displaystyle f:A\cup \{\perp \}\rightarrow B\cup \{\perp \}}
  
 where ⊥ (<a href="/facts/Bottom_element/JVn2B3mo">bottom</a>) indicates that the object function or its <a href="/facts/Argument_(computer_science)/LcuLbbSq">argument</a> diverges.
</p>
<h3>Concurrency theory</h3>
<p class="note">See also: <a href="/facts/Communicating_sequential_processes/bzKGnJ50">Communicating sequential processes § Failures/divergences model</a></p>
<p>In the calculus of <a href="/facts/Communicating_sequential_processes/bzKGnJ50">communicating sequential processes</a> (CSP), divergence occurs when a process performs an endless series of hidden actions.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> For example, consider the following process, defined by CSP notation:

C
        l
        o
        c
        k
        =
        t
        i
        c
        k
        →
        C
        l
        o
        c
        k
      
    
    {\displaystyle Clock=tick\rightarrow Clock}

The traces of this process are defined as:

traces
        ⁡
        (
        C
        l
        o
        c
        k
        )
        =
        {
        ⟨
        ⟩
        ,
        ⟨
        t
        i
        c
        k
        ⟩
        ,
        ⟨
        t
        i
        c
        k
        ,
        t
        i
        c
        k
        ⟩
        ,
        …
        }
        =
        {
        t
        i
        c
        k
        
          }
          
            ∗
          
        
      
    
    {\displaystyle \operatorname {traces} (Clock)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\ldots \}=\{tick\}^{*}}

Now, consider the following process, which hides the <i>tick</i> event of the <i>Clock</i> process:

P
        =
        C
        l
        o
        c
        k
        ∖
        t
        i
        c
        k
      
    
    {\displaystyle P=Clock\setminus tick}

As 
  
    
      
        P
      
    
    {\displaystyle P}
  
 cannot do anything other than perform hidden actions forever, it is equivalent to the process that does nothing but diverge, denoted 
  
    
      
        
          d
          i
          v
        
      
    
    {\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.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Infinite_loop/NG4b7SFa">Infinite loop</a></li>
<li><a href="/facts/Termination_analysis/T740cWY7">Termination analysis</a></li></ul>
<h2 id="notes">Notes</h2>

<ul><li><a href="/facts/Franz_Baader/t6bYooMc">Baader, Franz</a>; <a href="/facts/Tobias_Nipkow/3drUFKFs">Nipkow, Tobias</a> (1998). <a href="https://books.google.com/books?id=N7BvXVUCQk8C&q=Divergent"><i>Term Rewriting and All That</i></a>. Cambridge University Press. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780521779203.</li>
<li><a href="/facts/Benjamin_C._Pierce/m9DKUgML">Pierce, Benjamin C.</a> (2002). <a href="/facts/Types_and_Programming_Languages/vrEw2McI"><i>Types and Programming Languages</i></a>. MIT Press.</li>
<li>J. M. R. Martin and S. A. Jassim (1997). "<a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.19.1615&rep=rep1&type=pdf">How to Design Deadlock-Free Networks Using CSP and Verification Tools: A Tutorial Introduction</a>" in <i>Proceedings of the WoTUG-20</i>.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>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. <a href="http://extras.springer.com/2002/978-3-642-63970-8/DVD3/rom/pdf/Hoare_hist.pdf" target="_blank">http://extras.springer.com/2002/978-3-642-63970-8/DVD3/rom/pdf/Hoare_hist.pdf</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Baader & Nipkow 1998, p. 9. - Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203. <a href="https://books.google.com/books?id=N7BvXVUCQk8C&q=Divergent" target="_blank">https://books.google.com/books?id=N7BvXVUCQk8C&q=Divergent</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Pierce 2002, p. 65. - Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
<li id="fn:4"><p>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. <a href="978-1-84882-257-3" target="_blank">978-1-84882-257-3</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li>
</ol>

Divergence (computer science) open-in-new

Divergence (computer science)