2.10.2. ВЫЧИСЛЕНИЕ ТРОП

Вычисление тропы Q производится при условии, что задана среда Env и целое неотрицательное число m. Среда Env содержит значения переменных, которые могут потребоваться в процессе вычисления тропы. Число m, именуемое уровнем тропы, характеризует степень вложенности тропы в заборы, т.е. количество заборов "\?", окружающих Q, еще не закрытых отсечениями "\!".

Если вычисление тропы заканчивается, то результатом вычисления является либо объектное выражение Oe, либо неуспех $fail(k), где целое неотрицательное k характеризует "степень серьезности" неуспеха, либо ошибка $error(Oe), где Oe - сообщение об ошибке.

Если тропа находится на уровне m, а результатом ее вычисления является неуспех $fail(k), "серьезность неуспеха" всегда удовлетворяет условию 0 <= k <= m+1. В частности, если тропа находится на уровне 0, всегда либо k=0, либо k=1.

В дальнейшем запись Env,m,St |- Q => X,St' означает, что если тропа Q находится на уровне m, то результатом ее вычисления в среде Env является X, причем если вычисление тропы Q началось в глобальном состоянии St, то оно завершится в глобальном состоянии St'.

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

Во многих случаях смысл тропы Q может быть объяснен через смысл другой тропы Q'. А именно, чтобы вычислить тропу Q, следует вычислить тропу Q', и то, что получится, следует считать результатом вычисления тропы Q. Формально это можно выразить с помощью следующего правила вывода:

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