Dywergencja (informatyka)

„Zakończenie” przekierowuje tutaj. W przypadku innych zastosowań zobacz Zakończenie .

W informatyce mówi się, że obliczenia są rozbieżne , jeśli nie kończą się lub kończą w wyjątkowym stanie . W przeciwnym razie mówi się, że jest zbieżny . W dziedzinach, w których oczekuje się, że obliczenia będą nieskończone, takich jak rachunki procesowe , mówi się, że obliczenia rozchodzą się, jeśli nie są produktywne (tj. Kontynuują wytwarzanie działania w skończonym czasie).

Definicje

Różne poddziedziny informatyki używają różnych, ale matematycznie precyzyjnych definicji tego, co oznacza zbieżność lub rozbieżność obliczeń.

Przepisanie

W abstrakcyjnym przepisaniu abstrakcyjny system przepisywania nazywany jest zbieżnym, jeśli jest zarówno konfluentny , jak i końcowy .

Zapis t ↓ n oznacza, że ​​t redukuje się do postaci normalnej n przy zerowej lub większej liczbie redukcji , t ↓ oznacza, że ​​t redukuje się do jakiejś postaci normalnej przy zerowej lub większej liczbie redukcji, a t ↑ oznacza, że ​​t nie redukuje się do postaci normalnej; to ostatnie jest niemożliwe w kończącym się systemie przepisywania.

W rachunku lambda wyrażenie jest rozbieżne, jeśli nie ma postaci normalnej .

Semantyka denotacyjna

W semantyce denotacyjnej funkcję obiektu fa : ZA → B można modelować jako funkcję matematyczną ${\ Displaystyle f: A \ kubek \ {\ perp \} \ rightarrow B \ puchar \{\perp \}}$ gdzie ⊥ ( dół ) wskazuje, że funkcja obiektu lub jej argument jest rozbieżny.

Teoria współbieżności

W rachunku komunikowania się procesów sekwencyjnych rozbieżność to drastyczna sytuacja, w której proces wykonuje niekończącą się serię ukrytych działań. Rozważmy na przykład następujący proces, zdefiniowany przez notację CSP :

${\ Displaystyle Zegar = zaznacz \ strzałka w prawo Zegar}$

Ślady tego procesu definiuje się jako:

$\ Displaystyle \ operatorname {ślady } (Zegar)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\cdots \}=\{tick\}^{*}}$

Rozważmy teraz następujący proces, który ukrywa zdarzenie tick procesu Clock :

${\ Displaystyle P = Zegar \ odwrotny ukośnik zaznaczenia}$

Z definicji proces P nazywany jest procesem rozbieżnym.

Zobacz też

• Nieskończona pętla
• Analiza zakończenia

Notatki

•   Baader Franz ; Nipkow, Tobiasz (1998). Przepisywanie terminów i to wszystko . Wydawnictwo Uniwersytetu Cambridge. ISBN 9780521779203 .
• Pierce, Benjamin C. (2002). Typy i języki programowania . MIT Press.
• JMR Martin i SA Jassim (1997). „ Jak projektować sieci wolne od zakleszczeń przy użyciu CSP i narzędzi do weryfikacji: wprowadzenie do samouczka ” w Proceedings of the WoTUG-20 .