Дивергенция (информатика)

Вычисление, которое не завершается или завершается в исключительном состоянии

В информатике говорят, что вычисление расходится, если оно не завершается или завершается в исключительном состоянии . ^{[1] : 377} В противном случае говорят, что оно сходится . В областях, где вычисления, как ожидается, будут бесконечными, таких как исчисления процессов , говорят, что вычисление расходится, если оно не может быть продуктивным (т. е. продолжать производить действие в течение конечного периода времени).

Определения

Различные разделы компьютерной науки используют разные, но математически точные определения того, что означает сходимость или расходимость вычисления.

Переписывание

В абстрактном переписывании абстрактная система переписывания называется конвергентной, если она является одновременно конфлюэнтной и завершающей . ^[2]

Запись t ↓ n означает, что t приводится к нормальной форме n за ноль или более редукций , t ↓ означает, что t приводится к некоторой нормальной форме за ноль или более редукций, а t ↑ означает, что t не приводится к нормальной форме; последнее невозможно в терминальной системе переписывания.

В лямбда-исчислении выражение является расходящимся, если оно не имеет нормальной формы . ^[3]

Денотационная семантика

В денотативной семантике функция объекта f  : A → B может быть смоделирована как математическая функция , где ⊥ ( внизу ) указывает на то, что функция объекта или ее аргумент расходятся. ${\displaystyle f:A\cup \{\perp \}\rightarrow B\cup \{\perp \}}$

Теория параллелизма

В исчислении последовательных процессов связи (CSP) дивергенция — это драматическая ситуация, когда процесс выполняет бесконечную серию скрытых действий. Например, рассмотрим следующий процесс, определенный нотацией CSP:

${\displaystyle Clock=tick\rightarrow Clock}$

Следы этого процесса определяются как:

${\displaystyle \operatorname {traces} (Clock)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\cdots \}=\{tick\}^{*}}$

Теперь рассмотрим следующий процесс, который скрывает событие тика процесса Clock :

${\displaystyle P=Clock\backslash tick}$

По определению, P называется расходящимся процессом.

Смотрите также

• Бесконечный цикл
• Анализ прекращения

Примечания

1. CAR Hoare (октябрь 1969 г.). "Аксиоматическая основа компьютерного программирования" (PDF) . Сообщения ACM . 12 (10): 576–583. doi :10.1145/363235.363259. S2CID  207726175.
2. Баадер и Нипков 1998, стр. 9.
3. Пирс 2002, стр. 65.

Ссылки

• Баадер, Франц ; Нипков, Тобиас (1998). Переписывание терминов и все такое. Cambridge University Press. ISBN 9780521779203.
• Пирс, Бенджамин С. (2002). Типы и языки программирования . MIT Press.
• JMR Martin и SA Jassim (1997). «Как проектировать сети без тупиков с использованием CSP и инструментов проверки: введение в учебник» в трудах WoTUG-20 .