2.8.2. СОПОСТАВЛЕНИЕ С ОБРАЗЦОМ

Мы говорим, что среда Env является результатом сопоставления объектного выражения Oe с образцом P в начальной среде Env0, если выполнены следующие условия.

(1) Среда Env является расширением среды Env0, т.е. область определения среды Env является расширением области определения среды Env0, и для любой переменной V из области определения среды Env0 имеет место Env(V)=Env0(V).
(2) Если все переменные, входящие в P, заменить на их значения в соответствии с Env, а указатель направления отбросить, получится объектное выражение Oe.

 

В этом случае среду Env мы будем также называть вариантом сопоставления Oe с P в среде Env0, a множество таких вариантов сопоставления будем обозначать через Match(Env0,Oe,P).

На множестве Match(Env0,Oe,P) вводится отношение порядка следующим образом.

Пусть Match(Env0,Oe,P) содержит два различных варианта сопоставления Env1 и Env2. Рассматриваются все вхождения переменных в P.

Если P имеет указатель направления $l, то отыскивается самое первое слева вхождение, которое принимает для двух вариантов сопоставления Env1 и Env2 различные значения.

Если P имеет указатель направления $r, то отыскивается самое первое справа вхождение, которое принимает для двух вариантов сопоставления Env1 и Env2 различные значения.

Пусть найденное вхождение является вхождением переменной V. Тогда если Env1(V) короче чем Env2(V), считается, что Env1 предшествует Env2. В противном случае считается, что Env2 предшествует Env1.

Конечную последовательность сред Env1, Env2, ..., Envn будем записывать в виде [Env1, Env2, ... , Envn], пустую последовательность - в виде [].

Запись [Env0]^[Env1,...,Envn] будет обозначать [Env0, Env1,..., Envn].

Запись Env0 |- Oe : P => [Env1,...Envn] будет означать, что Match(Env0,Oe,P) = {Env1,...,Envn} и при этом Envi предшествует Envj для всех i<j.