2.13.2. ОГРАНИЧЕНИЯ, НАЛАГАЕМЫЕ ОБЪЯВЛЕНИЯМИ ФУНКЦИЙ

Объявления функций имеют вид

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

Определения функций должны удовлетворять ограничениям, налагаемым входными и выходными форматами функций. Чтобы описать эти ограничения, мы введем на множестве форматов отношение частичного порядка.

Пусть F1 и F2 два формата. Запись F2>>F1 будет означать, что формат F1 является (частным) случаем формата F2. Отношение >> определяется следующими правилами.

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

(1) У всех переменных, входящих в Re, отбрасываются индексы.

(2) Вызовы всех функций, появляющиеся в Re, заменяются на выходные форматы этих функций. А именно, если в Re имеется вызов функции вида <Fname Re'>, a объявление функции Fname имеет вид $func Fname Farg = Fres; либо $func? Fname Farg = Fres;, то <Fname Re'> заменяется на Fres.

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

(1) У всех переменных, входящих в P, отбрасываются индексы.

(2) Если P имеет указатель направления сопоставления, то этот указатель отбрасывается.

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

В дальнейшем form[Re] будет обозначать формат результатного выражения Re, form[P] - формат образца P, а form[He] - формат жесткого выражения He.

Следует подчеркнуть, что формат результатного выражения Re зависит не только от внешнего вида выражения Re, но и от выходных форматов тех функций, вызовы которых содержатся в Re. Тем не менее, для каждой конкретной программы form[Re] определен однозначно.

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

Пусть объявление функции Fname имеет входной формат Farg, выходной формат Fres, а в ее определении

образцовое распутье Palt имеет вид \{P1 R1; ... Pn Rn;}.

Тогда должны быть выполнены следующие условия.

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

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

Пусть вызов этой функции имеет вид <Fname Re>. Тогда должно выполнятся условие

Чтобы описать ограничения, налагаемые на результаты, вырабатываемые тропами, введем следующие обозначения.

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

Точно так же, тот факт, что результаты, вырабатываемые образцовым распутьем Palt, удовлетворяют формату F, мы будем записывать в виде F |- Palt.

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

Если функция Fname имеет определение Fname Palt и выходной формат Fres, то должно быть выполнено Fres |- Palt.

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