2.13.4. ОГРАНИЧЕНИЯ НА ИСПОЛЬЗОВАНИЕ ПЕРЕМЕННЫХ

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

А именно, если переменная используется в результатном выражении, она должна быть к этому моменту определена. Определением переменной является ее появление в образце, если к этому моменту она еще не была определена.

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

Сформулируем эти требования более точно. Для этого введем следующие обозначения.

vars[X] обозначает множество переменных, входящих в конструкцию X.

{} обозначает пустое множество.

v1+v2 обозначает объединение множеств v1 и v2.

v1++v2 обозначает пополнение множества переменных v1 переменными из v2. А именно, v1++v2 содержит все переменные из v2, а также все переменные из v1, индексы которых отличаются от индексов всех переменных из v2. Например, {sX, sY} ++ {eY, eZ} = {sX, eY, eZ}.

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

Аналогично, запись v |- Palt означает, что все переменные из v имеют разные индексы, и все переменные, значения которых могут понадобиться для вычисления образцового распутья Palt, входят в v.

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

Пусть функция Fname имеет определение Fname Palt. Тогда должно выполняться {} |- Palt.

Отношения v |- Q и v |- Palt определяются с помощью следующих правил.

v |- S v |- S

v |- R v++vars[He] |- R

---------- -----------------

v |- S R v |- S :: He R

 

v |- S"

v++vars[He] |- S' v |- S

v++vars[He] |- R v+vars[P] |- R

------------------------- ---------------

v |- S" $iter S' :: He R v |- S : P R

 

v |- S

v |- Q v |- R v |- Q

--------- ----------- ----------

v |- , Q v |- # S R v |- \? Q

 

v |- Q v |- Q

---------- v |- $fail ---------

v |- \! Q v |- = Q

 

v |- Q

v |- Q v |- Palt

-------------- ------------------------

v |- $error Q v |- $trap Q $with Palt

 

v |- Qj для всех j=1,...,n

----------------------------

v |- \{Q1; ... Qn;}

 

v |- S

v |- Palt

--------------

v |- S : Palt

 

все переменные из v имеют разные индексы

все переменные из vars[Re] входят в v

-----------------------------------------

v |- Re

 

v+vars[Pj] |- Rj для всех j=1,...,n

-------------------------------------

v |- \{P1 R1; ... Pn Rn;}