Вот есть у меня простая рекурсивная формула, описывающая некоторую систему процессов:
X(i) = if (i == 0) then [left -> X(0) | right -> X(1)] else [left -> X(i-1) | right -> X(i+1)]
Поясню, что означают операторы надо процессами (я обращаюсь к знатокам ТК, но они могут не знать ничего о CSP).
Оператор
a -> P означает: после того, как произойдёт событие
a продолжаем как процесс
P. То есть, он из некоторого события и процесса конструирует новый процесс.
Оператор
a -> P | b -> Q означает: если произойдёт
a, то дальше будет
P, если
b, то
Q.
А вообще (кажется, это важно), это два частных случая оператора выбора
a:A -> P(a), который означает: после того, как произойдёт одно из событий множества
A, процесс продолжится, как определяет функция
P.
a -> P пишут, когда лень указывать множество из одного элемента, а
a -> P | b -> Q пишут, когда лень писать
if.
Для процессов можно определить трассы, то есть, последовательности событий, которые приводят к продолжению процесса. Например, у специального процесса
STOP множество трасс содержит только пустую {""}. А у процесса
a -> STOP | b -> c -> STOP множество трасс будет {"a", "bc", ""}.
Да, в некотором смысле, трассы похожи на языки, задаваемые КС-грамматиками (отличия в том, что у процессов алгебра много богаче той, что я использую здесь).
Далее, в математической интерпретации, процессы отождествляются со своими множествами трасс. На множестве таких процессов можно ввести частичный порядок - порядок по включению одного множества трасс в другое. Это замечательно, потому что, в итоге у нас получается домен, в котором можно решать различные рекурсивные уравнения. При этом, конструктор оператора выбора
a:A -> P(a) будет непрерывной функцией.
Теперь, собственно, к вопросу. Вот (повторюсь) есть у меня формула:
X(i) = if (i == 0) then [left -> X(0) | right -> X(1)] else [left -> X(i-1) | right -> X(i+1)]
Сам Хоар (автор CSP) в этой формуле предлагает видеть такой смысл (это упрощённый вариант примера Хоара, в котором робот двигается по плоскости в клетку): если мы стоим в нулевой клетке, то мы в ней и стоим, при попытках сдвинуться влево; в любой другой клетке двигаемся в указанном направлении.
В этом рекурсивном уравнении справа стоит непрерывная функция. И мы можем, следовательно, применять оператор неподвижной точки. Исходным значением у нас должна быть функция, дно:
λi. STOP. И, вроде как, всё хорошо. И предел даже сходится. Но сходится он совсем не к тому, к чему хотелось бы, чтобы он сошёлся.
В результате получается функция, описывающая систему процессов такая, что в нулевой клетке, при попытке пойти налево (обработка события left) или направо (обработка right), всё зависает (заканчивается процессом STOP), из других клеток можно ходить только налево, при попытке пойти направо, всё зависает.
Можно ли как-нибудь навесить на это всё более близкую к интуитивной семантику? Я вот читаю о теории доменов и категорий, и там есть такое понятие как домен поддоменов (powerdomain), и вроде как, в рамках этой структуры рассматриваются пределы, которые позволяют работать с бесконечными структурами, и разворачивать постепенно семантическую конструкцию. Но, к сожалению, там всё написано на высоченном абстрактном уровне, и я совершенно не понимаю, как это можно применить на практике. Хотя бы вот к такому простому примеру.
Если кто поможет, или хотя бы укажет на книжку с соответствующими примерами, буду премного благодарен.
Простой
Средний