2.13.5. ОГРАНИЧЕНИЯ НА ИСПОЛЬЗОВАНИЕ ОТСЕЧЕНИЙ Каждой тропе, входящей в определение функции, может быть поставлено в соответствие целое неотрицательное число k, именуемое ее уровнем. Если двигаться вдоль тропы, то прохождение через "\?" увеличивает текущий уровень на 1, а прохождение через "\!" уменьшает уровень на 1. Таким образом, каждому отсечению "\!" должен однозначно соответствовать некоторый "парный" забор "\?".
Сформулируем это требование более точно. Для этого введем следующие обозначения.
Пусть k - целое неотрицательное число, а Q - тропа. Запись k |- Q означает, что тропе Q может быть приписан уровень k. Поскольку хвосты, источники и результатные выражения являются частными случаями троп, то же самое обозначение используется и для них.Аналогично, если
Palt - образцовое распутье, то запись k |- Palt означает, что образцовому распутью Palt может быть приписан уровень k. Теперь мы можем описать ограничения, налагаемые на использование отсечений в определениях функций, следующим образом.Пусть функция Fname имеет определение
Fname Palt. Тогда должно выполняться 0 |- Palt. Отношения k |- Q и k |- Palt определяются с помощью следующих правил.0 |- S 0 |- S
k |- R k |- R
--------- ---------------
k |- S R k |- S :: He R
0 |- S"
0 |- S' 0 |- S
k |- R k |- R
------------------------- -------------
k |- S" $iter S' :: He R k |- S : P R
0 |- S
k |- Q k |- R k+1 |- Q
--------- ----------- ----------
k |- , Q k |- # S R k |- \? Q
k |- Q 0 |- Q
------------ k |- $fail ---------
k+1 |- \! Q k |- = Q
0 |- Q
0 |- Q k |- Palt
-------------- ------------------------
k |- $error Q k |- $trap Q $with Palt
k |- Qj для всех j=1,...,n
----------------------------
k |- \{Q1; ... Qn;}
0 |- S
k |- Palt
-------------- k |- Re
k |- S : Palt
k |- Rj для всех j=1,...,n
----------------------------
k |- \{P1 R1; ... Pn Rn;}