Divergens (datavetenskap)

"Terminating" omdirigerar här. För annan användning, se Uppsägning .

Inom datavetenskap sägs en beräkning divergera om den inte avslutas eller avslutas i ett exceptionellt tillstånd . Annars sägs det konvergera . I domäner där beräkningar förväntas vara oändliga, såsom processkalkyler , sägs en beräkning divergera om den inte lyckas vara produktiv (dvs. att fortsätta producera en åtgärd inom en begränsad tid).

Definitioner

Olika delområden av datavetenskap använder olika, men matematiskt exakta, definitioner av vad det betyder att en beräkning konvergerar eller divergerar.

Omskrivning

I abstrakt omskrivning kallas ett abstrakt omskrivningssystem konvergent om det är både konfluent och avslutande .

Notationen t ↓ n betyder att t reducerar till normalform n i noll eller fler reduktioner , t ↓ betyder t reducerar till någon normalform i noll eller fler reduktioner, och t ↑ betyder t reduceras inte till normalform; det senare är omöjligt i ett avslutande omskrivningssystem.

I lambdakalkylen är ett uttryck divergent om det inte har någon normalform .

Denotationssemantik

I denotationssemantik kan en objektfunktion f : A → B modelleras som en matematisk funktion $f:A\cup \{\perp \}\högerpil B\cup \{\perp \}$ där ⊥ ( längst ner ) indikerar att objektfunktionen eller dess argument divergerar.

Samtidighetsteori

I kalkylen för att kommunicera sekventiella processer är divergens en drastisk situation där en process utför en oändlig serie av dolda handlingar. Tänk till exempel på följande process, definierad av CSP- notation:

$Clock=tick\rightarrow Clock$

Spåren av denna process definieras som:

$\operatornamn {spår } (Klocka)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\cdots \}=\{tick\}^{*}$

Tänk nu på följande process, som döljer tick- händelsen för Clock -processen:

$P=Clock\backslash tick$

Per definition kallas P en divergerande process.

Se även

• Oändlig loop
• Avslutningsanalys

Anteckningar

•   Baader, Franz ; Nipkow, Tobias (1998). Termomskrivning och allt det där . Cambridge University Press. ISBN 9780521779203 .
• Pierce, Benjamin C. (2002). Typer och programmeringsspråk . MIT Press.
• JMR Martin och SA Jassim (1997). " Hur man designar deadlock-fria nätverk med hjälp av CSP och verifieringsverktyg: en självstudieinledning" i Proceedings of the WoTUG-20 .