Dywergencja (informatyka) - Divergence (computer science)

W informatyce mówi się, że obliczenia są rozbieżne, jeśli nie kończą się lub kończą się w wyjątkowym stanie . W przeciwnym razie mówi się, że są zbieżne . W dziedzinach, w których oczekuje się, że obliczenia są nieskończone, takich jak rachunki procesowe , mówi się, że obliczenia rozchodzą się, jeśli nie są produktywne (tj. kontynuują działanie 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 abstrakcyjnej przepisywanie , abstrakcyjny układ przepisywanie nazywany jest zbieżny, jeżeli jest zarówno zlewające się i kończący .

Zapis t ↓ n oznacza, że t redukuje się do postaci normalnej n w zerowej lub większej liczbie redukcji , t ↓ oznacza t redukuje się do pewnej postaci normalnej w 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 denotational semantyki obiektu funkcji f  : A → B może być modelowana jako funkcja matematyczna, gdzie ⊥ ( dolny ) wskazuje, że funkcja obiektu lub argumentów są różne. ${\ Displaystyle f: A \ filiżanka \ {\ sprawca \} \ rightarrow B \ filiżanka \ {\ sprawca \}}$

Teoria współbieżności

W rachunku komunikowania procesów sekwencyjnych dywergencja 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 Clock = zaznacz \ Rightarrow Clock}$

Ślady tego procesu definiuje się jako:

${\ Displaystyle \ Operatorname {ślady} (zegar) = \ {\ langle \ rangle \ langle tik \ langle tik \ langle tik \ rangle \ cdots \} = \ {zaznacz \} ^ {*}}$

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

${\ Displaystyle P = zegar \ kleszcz odwrotnego ukośnika}$

Z definicji P nazywa się procesem rozbieżnym.

Zobacz też

• Nieskończona pętla
• Analiza terminacji

Uwagi

Bibliografia

• Baader, Franz ; Nipkow, Tobiasz (1998). Przepisywanie terminów i tak dalej . Wydawnictwo Uniwersytetu Cambridge. Numer ISBN 9780521779203.
• Pierce, Benjamin C. (2002). Typy i języki programowania . MIT Naciśnij.
• JMR Martin i SA Jassim (1997). „ Jak projektować sieci wolne od zakleszczeń za pomocą CSP i narzędzi do weryfikacji: wprowadzenie do samouczka ” w postępowaniu w sprawie WoTUG-20 .

Ten artykuł o informatyce jest skrótem . Możesz pomóc Wikipedii, rozwijając ją .

• v
• t
• mi