Неограниченный недетерминизм

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

Справедливость

Обсуждение неограниченного недетерминизма имеет тенденцию переплетаться с дискуссиями о справедливости . Основная концепция заключается в том, что все пути вычислений должны быть «справедливыми» в том смысле, что если машина бесконечно часто входит в какое-либо состояние, она должна совершать все возможные переходы из этого состояния. Это равносильно требованию, чтобы машина гарантированно обслуживала запрос, если может, поскольку бесконечная последовательность состояний будет разрешена только в том случае, если не существует перехода, который приводит к обслуживанию запроса. Эквивалентно, каждый возможный переход должен произойти в конечном итоге в ходе бесконечных вычислений, хотя для того, чтобы переход произошел, может потребоваться неограниченное количество времени. Эту концепцию следует отличать от локальной справедливости подбрасывания «честной» монеты, под которой понимается, что результат всегда может быть орлом для любого конечного числа шагов, хотя по мере увеличения числа шагов это не произойдет почти наверняка .

Пример роли справедливого или неограниченного недетерминизма в слиянии строк был приведен Уильямом Д. Клингером в его диссертации 1981 года. Он определил «справедливое слияние» двух строк как третью строку, в которой в конечном итоге должен появиться каждый символ каждой строки. Затем он рассмотрел набор всех справедливых слияний двух строк. merge (S, T) , предполагая, что это монотонная функция. Тогда он утверждал, что объединить (⊥,1 ^ой )⊆ объединить (0,1 ^ой ) , где ⊥ — пустой поток. Сейчас объединить (⊥,1 ^ой ) = {1 ^ой }, так что должно быть так 1 ^ой является элементом объединить (0,1 ^ой ) , противоречие. Он пришел к выводу, что:

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

О возможности реализации неограниченного недетерминизма

Эдсгер Дейкстра утверждал, что невозможно реализовать системы с неограниченным недетерминизмом. . По этой причине Тони Хоар предположил, что «эффективная реализация должна быть достаточно справедливой».

Недетерминированные автоматы

Недетерминированные машины Тьюринга имеют только ограниченный недетерминизм. Аналогично, последовательные программы, содержащие защищенные команды в качестве единственного источника недетерминизма, имеют только ограниченный недетерминизм. Короче говоря, недетерминизм выбора ограничен. Гордон Плоткин дал доказательство в своей оригинальной статье о доменах власти:

Теперь набор начальных сегментов последовательностей выполнения данной недетерминированной программы P , начиная с заданного состояния, образует дерево. Точки ветвления будут соответствовать точкам выбора в программе. Поскольку в каждой точке выбора всегда имеется лишь конечное число альтернатив, фактор ветвления дерева всегда конечен. То есть дерево финитно. гласит Лемма Кенига , что если каждая ветвь конечного дерева конечна, то конечна и сама ветвь. В данном случае это означает, что если каждая последовательность выполнения P завершается, то существует только конечное число последовательностей выполнения. Итак, если выходной набор P бесконечен, он должен содержать [незавершающееся вычисление].

автоматов

Уильям Клингер представил следующий анализ приведенного выше доказательства Плоткина:

Это доказательство основано на предпосылке, что если каждый узел x определенной бесконечной ветви может быть достигнуто с помощью некоторых вычислений c , то существует вычисление c, который посещает каждый узел х на ветке. ... Очевидно, что эта посылка вытекает не из логики, а скорее из интерпретации точек выбора. Эта предпосылка не работает из-за недетерминизма прибытия [при поступлении сообщений в модели Актера] из-за конечной задержки [при поступлении сообщений]. Хотя каждый узел бесконечной ветви должен лежать на ветви с пределом, сама бесконечная ветвь не обязательно должна иметь предел. Таким образом, существование бесконечной ветви не обязательно означает непрерывные вычисления.

и

Спаан и др. утверждали, что неограниченно недетерминированная программа может решить проблему остановки ; их алгоритм состоит из двух частей, определяемых следующим образом:

Первая часть программы запрашивает натуральное число из второй части; получив его, он выполнит итерацию желаемой машины Тьюринга на указанное количество шагов и примет или отклонит ее в зависимости от того, остановилась ли машина.

Вторая часть программы недетерминированно выбирает натуральное число по запросу. Число сохраняется в переменной, которая инициализируется значением 0; затем программа неоднократно выбирает, увеличивать ли переменную или обслуживать запрос. Ограничение справедливости требует, чтобы запрос в конечном итоге был обслужен, иначе возникает бесконечный цикл, в котором всегда выполняется только ветвь «увеличить переменную».

Очевидно, что если машина остановится, у этого алгоритма есть путь, который принимает. Если машина не остановится, этот алгоритм всегда отклонит, независимо от того, какое число вернет вторая часть программы.

в пользу

Клингер и Карл Хьюитт разработали модель (известную как Модель Актера ) параллельных вычислений со свойством неограниченного недетерминизма, встроенного в [Clinger 1981; ; ; ]; это позволяет выполнять вычисления , которые не могут быть реализованы с помощью машин Тьюринга, как показано выше. Однако эти исследователи подчеркивают, что их модель параллельных вычислений не может реализовать какие-либо функции, находящиеся вне класса рекурсивных функций. определено Чёрчем, Клини, Тьюрингом и т. д. (см. «Неопределённость в параллельных вычислениях »).

Хьюитт оправдал свое использование неограниченного недетерминизма, утверждая, что не существует ограничений, которые можно установить на то, сколько времени потребуется вычислительной схеме, называемой арбитром, для стабилизации (см. Метастабильность в электронике ). Арбитры используются в компьютерах для решения ситуации, когда компьютерные часы работают асинхронно с входными данными извне, например. , ввод с клавиатуры, доступ к диску, сетевой ввод и т. д. Таким образом, получение сообщения, отправленного на компьютер, может занять неограниченное время, и в то же время компьютер может проходить неограниченное количество состояний.

Он далее утверждал, что электронная почта обеспечивает неограниченный недетерминизм, поскольку почта может храниться на серверах неопределенное время, прежде чем будет доставлена, и что каналы передачи данных на серверы в Интернете также могут быть недоступными на неопределенный срок. Это привело к спорам о неограниченном недетерминизме .

Хьюитта

Хьюитт утверждал, что вопросы справедливости частично вытекают из точки зрения глобального государства. Самые старые модели вычислений (например, машины Тьюринга , Пост-продукция, лямбда-исчисление и т. д.) основаны на математике, которая использует глобальное состояние для представления вычислительного шага . Каждый вычислительный шаг осуществляется от одного глобального состояния вычислений к следующему глобальному состоянию. Подход с глобальным состоянием был продолжен в теории автоматов для конечных автоматов и машин с толкающим стеком , включая их недетерминированные версии. Все эти модели обладают свойством ограниченного недетерминизма: если машина всегда останавливается при запуске в исходном состоянии, то существует ограничение на количество состояний, в которых она может остановиться.

Хьюитт утверждал, что существует фундаментальное различие между выбором в недетерминизме глобального состояния и неопределенностью порядка прибытия (недетерминизмом) его модели Актера . В недетерминизме глобального состояния делается «выбор» в пользу «следующего» глобального состояния. При неопределенности порядка прибытия арбитраж решает каждый порядок прибытия локально в течение неограниченного периода времени. Пока идет местный арбитраж, неограниченная деятельность может иметь место в другом месте. Не существует глобального состояния и, следовательно, не существует «выбора» относительно «следующего» глобального состояния.

Ссылки

• Хьюитт, Карл ; Епископ Питер; Штайгер, Ричард (август 1973 г.). «Универсальный модульный формализм ACTOR для искусственного интеллекта». Материалы 3-й международной совместной конференции по искусственному интеллекту . IJCAI'73. Стэнфорд: Морган Кауфманн. стр. 235–245.
• Милнер, Робин (1973). «Процессы: математическая модель вычислительных агентов». Материалы логического коллоквиума . Логический коллоквиум '73. Бристоль: Северная Голландия. стр. 157–173.
• Хьюитт, Карл ; Епископ Питер; Грейф, Ирен ; Смит, Брайан; Мэтсон, Тодд; Штайгер, Ричард (октябрь 1973 г.). «Актерская индукция и метаоценка». Материалы 1-го ежегодного симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования . ПОПЛ'73. Бостон, Массачусетс: Ассоциация вычислительной техники. стр. 153–168. дои : 10.1145/512927.512942 .
• Хьюитт, Карл ; Епископ Питер; Штайгер, Ричард; Грейф, Ирен ; Смит, Брайан; Мэтсон, Тодд; Хейл, Роджер (апрель 1974 г.). «Поведенческая семантика нерекурсивных управляющих структур». В Робине, Б. (ред.). Материалы коллоквиума по программированию . Симпозиум по программированию. Париж: Springer Berlin Heidelberg. стр. 385–407. дои : 10.1007/3-540-06859-7_147 . ISBN  9783540378198 .
• Грейф, Ирен (август 1975 г.). Семантика взаимодействия параллельных процессов (кандидатская диссертация). Массачусетский технологический институт, факультет электротехники и информатики. hdl : 1721.1/57710 .
• Хьюитт, Карл ; Бейкер, Генри (август 1977 г.). «Акторы и непрерывные функционалы». В Нойхолде, Эрих Дж. (ред.). Материалы рабочей конференции ИФИП по формальному описанию концепций программирования . ИФИП'78. Сент-Эндрюс, Северная Каролина, Канада: Северная Голландия. ISBN  9780444851079 .
• Кан, Жиль ; МакКуин, Дэвид (1976). Сопрограммы и сети параллельных процессов (отчет об исследовании) . Проверено 9 марта 2022 г.
• Бейкер, Генри (январь 1978 г.). Акторные системы для вычислений в реальном времени (кандидатская диссертация). Массачусетский технологический институт, факультет электротехники и информатики.
• Смит, Майкл (1978). «Домены власти» . Журнал компьютерных и системных наук . 16 :23–36. дои : 10.1016/0022-0000(78)90048-X .
• Милн, Джордж; Милнер, Робин (апрель 1979 г.). «Параллельные процессы и их синтаксис» . Журнал АКМ . 6 (2): 302–321. дои : 10.1145/322123.322134 . S2CID   16565064 .
• Франсес, Ниссим ; Хоар, Африка ; Леманн, Дэниел Дж.; де Ровер, Виллем П. (декабрь 1979 г.). «Семантика недетерминизма, параллелизма и коммуникации» . Журнал компьютерных и системных наук . 19 (3): 290–308. дои : 10.1016/0022-0000(79)90006-0 .
• Линч, Нэнси А .; Фишер, Майкл Дж. (июль 1979 г.). «Об описании поведения и реализации распределенных систем». В Кане, Жиль (ред.). Труды международного симпозиума по семантике параллельных вычислений . Семантика параллельных вычислений. Эвиан, Франция: Springer-Verlag. стр. 147–171. дои : 10.1007/BFb0022468 . ISBN  9783540351634 .
• Шварц, Джеральд С. (июль 1979 г.). «Денотационная семантика параллелизма». В Кане, Жиль (ред.). Труды международного симпозиума по семантике параллельных вычислений . Семантика параллельных вычислений. Эвиан, Франция: Springer-Verlag. стр. 191–202. дои : 10.1007/BFb0022470 . ISBN  9783540351634 .
• Уодж, Уильям В. (июль 1979 г.). «Расширенное лечение тупиковой ситуации потока данных». В Кане, Жиль (ред.). Труды международного симпозиума по семантике параллельных вычислений . Семантика параллельных вычислений. Эвиан, Франция: Springer-Verlag. стр. 285–299. дои : 10.1007/BFb0022475 . ISBN  9783540351634 .
• Назад, Ральф-Йохан (июль 1980 г.). «Семантика неограниченного недетерминизма». Ин де Баккер, Жако ; ван Леувен, Ян (ред.). Седьмой коллоквиум по автоматам, языкам и программированию . Международный коллоквиум по автоматам, языкам и программированию. Нордвейкерхаут, Нидерланды: Springer-Verlag Berlin Heidelberg. стр. 51–63. дои : 10.1007/3-540-10003-2_59 .
• Парк, Дэвид (1979). «О семантике справедливого параллелизма». В Бьёрнере, Дайнс (ред.). Абстрактные спецификации программного обеспечения . 1979 Копенгагенская зимняя школа. Копенгаген: Springer-Verlag Берлин Гейдельберг. стр. 504–526. дои : 10.1007/3-540-10007-5_47 .

• Дана Скотт . Что такое денотационная семантика? Выдающаяся серия лекций Лаборатории компьютерных наук Массачусетского технологического института. 17 апреля 1980 года.

• Клингер, Уильям (август 1982 г.). «Недетерминированный вызов по необходимости не ленив и не по имени». Ин Парк, Дэвид М.Р.; Фридман, Дэниел П. (ред.). Материалы симпозиума ACM 1982 года по LISP и функциональному программированию . ЛФП'82. Питтсбург, Пенсильвания: Ассоциация вычислительной техники. стр. 226–234. дои : 10.1145/800068.802154 .
• Брукс, SD; Хоар, Африка ; Роско, AW (июль 1984 г.). «Теория взаимодействия последовательных процессов» . Журнал АКМ . 31 (3): 560–599. дои : 10.1145/828.833 . S2CID   488666 .
• Роско, AW (январь 1988 г.). «Неограниченный недетерминизм в CSP». Две статьи о CSP (PDF) (Техническая монография). Вычислительная лаборатория Оксфордского университета. ПРГ67 . Проверено 10 марта 2022 г.
• Роско, AW (10 ноября 1997 г.). Теория и практика параллелизма . Прентис-Холл. ISBN  9780136744092 .
• Шмидт, Дэвид А. (март 1994 г.). Структура типизированных языков программирования . Массачусетский технологический институт Пресс. ISBN  9780262193498 .
• Батлер, Майкл ; Морган, Кэрролл (январь 1995 г.). «Системы действий, неограниченный недетерминизм и бесконечные следы» . Формальные аспекты вычислений . 7 (1): 37–53. дои : 10.1007/BF01214622 . S2CID   2135743 .
• Судкамп, Томас А. (3 января 1997 г.). Языки и машины: введение в теорию информатики (2-е изд.). Аддисон-Уэсли. ISBN  9780201821369 .
• Ачето, Лука; Гордон, Эндрю Д. , ред. (август 2005 г.). Исчисление алгебраических процессов: первые двадцать пять лет и позже . ПА'05. Жилой центр Болонского университета Бертиноро (Форли), Италия: БРИКС.
• Брукс, Стивен (август 2005 г.). «Восстановление CSP» (PDF) . В Ачето, Лука; Гордон, Эндрю Д. (ред.). Исчисление алгебраических процессов: первые двадцать пять лет и позже . ПА'05. Жилой центр Болонского университета Бертиноро (Форли), Италия: БРИКС. стр. 75–80 . Проверено 10 марта 2022 г.