Дивергенция (информатика)
В информатике говорят, что вычисление расходится , если оно не завершается или завершается в исключительном состоянии . [1] : 377 В противном случае говорят, что оно сходится . В областях, где ожидается, что вычисления будут бесконечными, например, в исчислении процессов , говорят, что вычисление расходится, если оно не может быть продуктивным (т. е. продолжать производить действие в течение конечного промежутка времени).
Определения
[ редактировать ]В различных областях информатики используются разные, но математически точные определения того, что означает сходимость или расхождение вычислений.
Переписывание
[ редактировать ]В абстрактном переписывании называется система абстрактного переписывания конвергентной, если она одновременно сливающаяся и завершающаяся . [2]
Обозначение t ↓ n означает, что t приводит к нормальной форме n за ноль или более сокращений , t ↓ означает, что t приводит к некоторой нормальной форме за ноль или более сокращений, а t ↑ означает, что t не приводит к нормальной форме; последнее невозможно в терминирующей системе переписывания.
В лямбда-исчислении выражение считается расходящимся, если оно не имеет нормальной формы . [3]
Денотационная семантика
[ редактировать ]В денотационной семантике объектная функция f : A → B может быть смоделирована как математическая функция. где ⊥ ( внизу ) указывает, что объектная функция или ее аргумент расходятся.
Теория параллелизма
[ редактировать ]В расчете последовательных процессов (CSP) дивергенция — это радикальная ситуация, когда процесс выполняет бесконечную серию скрытых действий. Например, рассмотрим следующий процесс, определенный нотацией CSP:
Следы этого процесса определяются как:
Теперь рассмотрим следующий процесс, который скрывает тика событие процесса Clock :
По определению P называется расходящимся процессом.
См. также
[ редактировать ]Примечания
[ редактировать ]- ^ АВТОМОБИЛЬ Хоара (октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации АКМ . 12 (10): 576–583. дои : 10.1145/363235.363259 . S2CID 207726175 .
- ^ Баадер и Нипков 1998 , с. 9.
- ^ Пирс 2002 , с. 65.
Ссылки
[ редактировать ]- Баадер, Франц ; Нипков, Тобиас (1998). Переписывание терминов и все такое . Издательство Кембриджского университета. ISBN 9780521779203 .
- Пирс, Бенджамин К. (2002). Типы и языки программирования . МТИ Пресс.
- Дж. М. Р. Мартин и С. А. Джассим (1997). « Как спроектировать сети без тупиков с использованием CSP и инструментов проверки: введение в учебное пособие » в Proceedings of WoTUG-20 .