В информатике говорят, что вычисления расходятся, если они не завершаются или не завершаются в исключительном состоянии . [1] : 377 В противном случае говорят, что он сходится . В областях, где ожидается бесконечность вычислений, таких как вычисления процессов , считается, что вычисление расходится, если оно не может быть продуктивным (т.е. продолжать производить действие в течение конечного промежутка времени).
Определения
В различных подразделах информатики используются различные, но математически точные определения того, что означает схождение или расхождение вычислений.
Перезапись
При абстрактном переписывании система абстрактного переписывания называется конвергентной, если она одновременно сливается и завершается . [2]
Обозначение t ↓ n означает, что t сводится к нормальной форме n за ноль или более сокращений , t ↓ означает, что t приводится к некоторой нормальной форме за ноль или более сокращений, а t ↑ означает, что t не сводится к нормальной форме; последнее невозможно в прерывающейся системе перезаписи.
В лямбда-исчислении выражение считается дивергентным, если оно не имеет нормальной формы . [3]
Денотационная семантика
В денотационной семантике объекта функция F : → B может быть смоделирован как математическая функция где ⊥ ( внизу ) указывает, что функция объекта или ее аргумент расходятся.
Теория параллелизма
В исчислении взаимодействия последовательных процессов дивергенция - это серьезная ситуация, когда процесс выполняет бесконечную серию скрытых действий. Например, рассмотрим следующий процесс, определенный нотацией CSP :
Следы этого процесса определяются как:
Теперь рассмотрим следующий процесс, который скрывает событие тика процесса Clock :
По определению P называется расходящимся процессом.
Смотрите также
Заметки
- ↑ CAR Hoare (октябрь 1969). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации ACM . 12 (10): 576–583. DOI : 10.1145 / 363235.363259 . S2CID 207726175 .
- ^ Баадер & Нипково 1998 , стр. 9.
- Перейти ↑ Pierce, 2002 , p. 65.
Рекомендации
- Баадер, Франц ; Нипков, Тобиас (1998). Перезапись терминов и все такое . Издательство Кембриджского университета. ISBN 9780521779203. CS1 maint: обескураженный параметр ( ссылка )
- Пирс, Бенджамин С. (2002). Типы и языки программирования . MIT Press.
- JMR Martin и SA Jassim (1997). « Как проектировать сети без тупиков с использованием CSP и инструментов проверки: введение в учебное пособие » в материалах WoTUG-20 .