1.8.2. Реализация

Предположим, что процесс реализован ЛИСП-функцией Р, и пусть s – некоторый протокол. Определить, является ли s возможным протоколом Р, можно с помощью функции

протокол_ли(s,Р) = if s = NIL then истина

else if P(s₀) = "ВLEEР then ложь

else протокол_ли(s’, Р(s₀))

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

1.8.3. После

Если s ∈ протоколы(Р),то

P / s (P после s) –

это процесс, ведущий себя так, как ведет себя Р с момента завершения всех действий, записанных в протоколе s. Если s не является протоколом Р, то (P / s) не определено.

Примеры

X1. (ТАП / <мон>) = (шок ТАП)

Х2. (ТАП / <мон, шок>) = ТАП

Х3. (ТАС / <n1>³) = СТОП

Х4. Во избежание убытка от установки ТАДОВЕР (1.1.3 Х5, Х6) первую шоколадку владелец автомата решает съесть сам:

(ТАДОВЕР / <шок>) = ТАП2

В древовидном представлении Р (рис. 1.1) конструкции Р / s) соответствует все поддерево с корнем в конечной вер­шине пути, помеченного символами из s. Таким образом, в на­шем примере поддерево, исходящее из черной вершины, опи­сывается как TAС / (n2, мал, сд1)

Следующие законы раскрывают значение операции /. Ни­чего не сделав, процесс остается неизменным:

L1. P / <> = P

Поведение процесса Р после завершения событий из s^t совпадает с поведением (P / s) после завершения событий из t:

L2. P / (s^t) = (P / s) / t;

Если процесс участвовал в событии с, его дальнейшее пове­дение определяется именно этим начальным выбором:

L3. (x : В → Р(x)) / <c> = Р(с) при условии, что с ∈ В

В качестве следствия мы получаем, что оператор /<с> яв­ляется обратным по отношению к оператору префиксации

с →:

L3A. (с Р) / <c> = Р

Протоколы (P / s) определяются как

L4. протоколы(Р / s) = (t | s^t ∈ протоколы(Р)} при условии, что s ∈ протоколы(Р)

Для доказательства того, что процесс Р работает бесконечно, достаточно доказать, что

Р / s = СТОП для всех s ∈ протоколы (Р)

Другим желательным свойством процесса является циклич­ность; по определению процесс Р – циклический, если при любых обстоятельствах он может вернуться в начальное со­стояние, т. е.

∀s : протоколы(P). ∃t.(P / (s^t) = P)

СТОП – это тривиальный циклический процесс; если же лю­бой другой процесс цикличен, он также обладает полезным свойством никогда не останавливаться.

Примеры

X1. Следующие процессы являются циклическими (1.1.3 Х8, 1.1.2 X2, 1.1.3 X3, 1.1.4 X2):

ИСП_А, ТАП, (шок → ТАП), ТАШИ, СТ₇

Х2. Следующие процессы не являются циклическими, потому что они не могут вернуться в начальное состояние (1.1.2 X2, 1.1.3 X3, 1.1.3 X2):

(мон → ТАП), (шок → ТАШИ), (вокруг → СТ₇)

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

Предостережение. Использование / в рекурсивно опреде­ленных процессах, к сожалению, лишает их свойства предваренности, и поэтому возникает опасность получения неодно­значных решений. Например, уравнение Х = (а → (Х / <а>)) не является предваренным и имеет решением любом процесс вида а → Р для любого Р,

Доказательство:

(а → ((а →) / <а>)) = (а → Р) согласно L3A

По этой причине мы никогда не будем использовать опера­цию «/» в рекурсивных определениях процесса.