r7 - 22 Jul 2005 - 13:40:34 - Luba ParmyonovaYou are here: TWiki >  Refaldevel Web > FuturePlans > SpecR2 > Algorithms
Существует два подхода к синтаксическому отождествлению в Рефале: аксиоматический и процедурный. В описании Рефала синтаксическое отождествление определяется следующим образом.
Объектное выражение M может быть синтаксически отождествлено как типовое выражение L, если переменные в L можно заменить на такие значения, что M совпадет с L; при этом должны выполняться условия:
  1. значением S-переменной может быть только символ, значением W-переменной - только терм, значением V-переменной - непустое выражение, значением E-переменной - произвольное выражение, которое может быть пустым;
  2. Все вхождения одной и той же переменной должны принимать одинаковые значения;
  3. Если некоторое вхождение переменной имеет спецификатор, то все термы, входящие в выражение на нулевом уровне скобок должны удовлетворять этому спецификатору.

Множество всех способов отождествления M как L обозначают W#[L,M].

Правило отождествления

Пусть W#[L,M] непусто. Пусть X1, X2, ..., XN - VE-переменные, входящие в L, в том порядке, в каком они входят в L. Строится последовательность множеств W0,W1, ..., WN , обладающая следующими свойствами:

  1. W0 = W#[L,M]
  2. Для всех способов отождествления, входящих в Wk, значения переменных X1, ..., Xk не зависят от способа отождествления.
  3. Wk SUBSET W[k-1], причем в Wk входят только такие способы отождествления из Wk, для которых Xk принимает самое короткое значение.

WN содержит только один способ отождествления, который называется саным левым в W#[L,M] и обозначается RCG#[L,M].

Подстановки

Отождествления M как L представляют в виде подстановок.

Подстановкой называется любое конечное множество упорядоченных пар вида (X,B), где X - переменная, B - объектное выражение.

Если D - подстановка, то VARS[D] - множество таких переменных X, для которых существует упорядоченная пара вида (X,B), входящая в D. Если L - типовое выражение, то VARS[L] - множество переменных, входящих в L.

Подстановка называется совместной, если выполняются условия:

  1. для любой переменной X из VARS[D] существует ровно одна пара вида (X,B), входящая в D;
  2. для любой пары (X,B), входящей в D, объектное выражение B является допустимым значением для переменной X.

Подстановка D применима к типовому выражению L, если выполнены следующие условия:

  1. D совместна;
  2. VARS[L] SUBSET VARS[D];
  3. для любого вхождения переменной X в L, имеющего спецификатор Q, из того, что (X,B) входят в D, следует, что все термы, входящие в выражение B на нулевом уровне скобок удовлетворяют этому спецификатору.

Пусть подстановка D применима к типовому выражению L. Результат применения D к L обозначается SUBST[D,L] и определяется с помощью соотношений:


   1. SUBST[D,< >] = < >
   2. SUBST[D, Z] = Z
   3. SUBST[D,A', A''] = SUBST[D,A'] SUBST[D,A'']
   4. SUBST[D, X] = B, где (X,B) IN D

где А' и A'' - произвольные типовые выражения, Z - произвольный символ, X - произвольная переменная, B - произвольное объектное выражение.

Подстановка D является отождествлением объектного выражения M как типового выражения L, если SUBST[D,L] = M.

W#[L,M] - моножество таких подстановок D, для которых SUBST[D,L] = M и, при этом, VARS[D] = VARS[L].

Далее задачу эффективного поиска отождествления заменяют более общей задачей, а именно, предполагают следующие обобщения:

  1. на множество искомых подстановок накладываются дополнительные ограничения; считается, что значения некоторых переменных жестко зафиксированы, это значит, что все искомые подстановки должны содержать в качестве подмножества некоторую подстановку C ;
  2. вместо отождествления одного объектного выражения M как типового выражения L рассматривают отождествление упорядоченной N-ки (кортежа) объектных выражений 1, М2, ... Mn) как упорядоченной N-ки типовых выражений (L1, L2, ... Ln).

Пусть задана упорядоченнаяN-ка типовых выражений L = (L1,L2,...,Ln), называемых дырами, и упорядоченная N-ка объектных выражений, (M1,M2,...,Mn), назывемых образами, а также задана подстановка G. Подстановка D является отождествлением M как L при ограничении G, если выполнены условия:


   1. D - совместна
   2. G SUBSET D
   2. SUBST[D,L] = M

W[G,L#M] - множество таких отождествлений D кортежа М как кортежа L при ограничении G, что VARS[L]+VARS[G] = VARS[D].

Правило отождестления.

Пусть G - подстановка, L#M - кортеж из пар выражений. Функция RCG[G,L#M] определяется следующим образом:


   1. если W[G,L#M] = 0, то RCG[G,L#M] = UNDEF
   2. если W[G,L#M]!=<0>, то RCG[G,L#M] равна самому левому отождествлению из W[G, L#M].

Основная идея алгоритма отождествления заключается в сведении вычисления RCG[G,L#M] к вычислению RCG[G',L'#M'], где L'#M' содержит меньше элементов, чем L#M. В конце концов кортеж L#M становится пустым, и работа алгоритма отождествления заканчивается, поскольку RCG[G,< >] = G (при условии, что G - совместная подстановка).

Символы, скобки, переменные, входящие в L и M называют элементами дыр и образов.

В процессе работы алгоритма отождествления элементы дыр постепенно сопоставляются с элементами образов.

Основной шаг алгоритма отождествления состоит в том, чтобы выбрать в какой-то дыре из L какой-то элемент и соспоставить ему часть образа соответствующей дыры, именуемой в дальнейшем образом этого элемента. После этого элемент удаляется из L, а его образ из M. В результате этого размер кортежа L#M уменьшается. Если сопоставленный элемент из L является какой-то переменной из X, а образом этого элемента является выражение B, то в G добавляется пара (X, B).

Выбор очередного элемента из L для сопоставления происходит следующим образом.

Сначала алгоритм отождествления находит все элементы из L, доступные для сопоставления. Затем доступные элементы делятся на две группы очередности. В первую группу входят все однозначно сопоставимые элементы, а во вторую - открытые вхождения VE-переменных, то есть вхождения VE-переменных, не входящих в VARS[G] и не стоящих одновременно на правом и левом концах дыры.

Алгоритм отождествления стремится в первую очередь соспоставлять элементы из первой группы, и только если их нет - сопоставляет элементы из второй группы.

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

Найдя нужный элемент, алгоритм отождествления пытается его сопоставить. Если элемент однозначно соспоставимый, то попытка его сопоставить либо терпит неудачу, либо проходит успешно. Если сопоставление проходит успешно, алгоритм отождествления вносит изменения в G и L#M и переходит к сопоставлению следующих элементов. Если же соспоставление элемента терпит неудачу, то алгоритм отождествления вырабатывет результат UNDEF и прекращает работу.

Сложнее обстоит дело с открытыми вхождениями VE-переменных. Здесь алгоритм отождествления уже не может решить сразу, каким должно быть значение VE-переменной, поэтому ему приходится перебирать несколько возможностей. Перебор происходит по самому левому вхождению VE-переменной в L, возможные значения переменной рассматриваются в порядке возрастания их длин.

В момент обращения алгоритм получает параметры:
G - ограничения на значения переменных (подстановка);
L = (L1, L2,..., LN) - кортеж дыр;
M = (M1, M2,..., MN) - кортеж образов.

Будем считать, что все вхождения переменных имеют спецификатор (отсутствие спецификатора эквивалентно наличию универсального спецификатора W).

Если G - несовместная подстановка, то RETURN[UNDEF].

Если N=0, т.е. М и N - пустые кортежи, то RETURN[G].

HSCH. Поиск дыры. Если все дыры имеют вид, U(Q')1 A U(Q'')2, где U1, U2 - VE-переменные, не входящие в VARS[G], a A - типовое выражение, то перейти к LVE, иначе найти дыру, которая не имеет указанного вида, и перейти к HARD.

HARD. Сопоставление жестких элементов. Пусть L#M имеет вид L#M = X (A, B) Y, где A - дыра, найденная в HSCH, a B - ее образ.

Если A = < >, то перейти к NIL.

Если A = E (Q) X, где EX - E-переменная, не входящая в VARS[G], то перейти к CE.

Если A = V (Q) X, где VX - V-переменная, не входящая в VARS[G], то перейти к CV.

В этом месте известно, что дыра A не может и начинаться, и кончаться на VE-переменные, не входящие в VARS[G].

Выбрать такой конец дыры A, на котором не находится VE-переменная, не входящая в VARS[G]. Если выбран левый конец, то перейти к HARDL, если выбран правый конец, то перейти к <ttHARDR.

NIL. Сопоставление пустой дыры. Если B = < >, то RETURN [RCG [G, X, Y]], иначе RETURN [UNDEF] .

CE. Сопоставление закрытого вхождения E-переменной. Если ZT[B] SUBSET YES[Q], то RETURN [RCG [G+<* (EX, B) *>, X Y]] , иначе RETURN [UNDEF].

CV. Сопоставление закрытого вхождения V-переменной. Если B = < >, то RETURN [UNDEF]. Если ZT[B] SUBSET YES[Q] , то RETURN [RCG [G+<* (VX, B) *>, X Y]], иначе RETURN [UNDEF] .

HARDL. Жесткий элемент слева.

Если A = (A') A'', то перейти к LB.

Если A = Z A, где Z - символ, то перейти к LSC.

Если A = S(Q)X A' , где SX - S -переменая, то перейти к LS.

Если A = W(Q)X A' , где WX - W -переменая, то перейти к LW.

Если A = E(Q)X A' , где EX - E -переменая, то перейти к LED.

Если A = V(Q)X A' , где VX - V -переменая, то перейти к LVD.

HARDR. Жесткий элемент справа.

Если A = A'(A''), то перейти к RB.

Если A = A Z, где Z - символ, то перейти к RSC.

Если A = A' S(Q)X, где S(X)-S переменная, то перейти к RS.

Если A = A' W(Q)X, где W(X)-W переменная, то перейти к RW.

Если A = A' E(Q)X, где E(X)-E переменная, то перейти к RED.

Если A = A' V(Q)X, где V(X)-V переменная, то перейти к RVD.

LB. Скобка слева. Если B не начинается с "(", то RETURN [UNDEF].
Иначе B = (B')B''. RETURN [RCG [G, X (A', B')(A'', B'') Y]].

LSC. Символ-константа слева. Если B не начинается с символа Z, то RETURN [UNDEF]. Иначе B = Z B'. RETURN [RCG [G, X(A', B') Y]].

LS. S-переменная слева. Если B не начинается с символа, то RETURN [UNDEF]. Иначе B = Z B'. Если Z IN YES[Q], то RETURN [RCG [G+<* (SX, Z) *>, X (A', B') Y]]. Иначе RETURN [UNDEF].

LW. W-переменная слева. Если B = < >, то RETURN [UNDEF]. Иначе B = T B', где T - терм. Если T IN YES[Q], то RETURN [RCG [G+<* (WX,T) *>, X (A'B') Y]]. Иначе RETURN [UNDEF].

LED Повторная E-переменная слева. Пусть E = SUBST [G, EX]. Если B не начинается с E, то RETURN [UNDEF]. Иначе B = E B'. Если ZT[E] SUBSET YES[Q], то RETURN [RCG [G, X (A', B') Y]]. Иначе RETURN [UNDEF].

LVD Повторная V-переменная слева. Пусть V = SUBST [G, VX]. Если B не начинается с V, то RETURN [UNDEF]. Иначе B = V B'. Если ZT[V] SUBSET YES[Q], то RETURN [RCG [G, X (A', B') Y]]. Иначе RETURN [UNDEF].

RB. Скобка справа. Если B не кончается на ")", то RETURN [UNDEF]. Иначе B = B' (B''). RETURN [RCG [G, X (A', B') (A'', B'') Y]].

RSC. Символ-константа справа. Если B не кончается на символ Z, то RETURN [UNDEF]. Иначе B = B' Z. RETURN [RCG [G, X (A', B') Y]].

RS. S-переменная справа. Если B не кончается на символ, то RETURN [UNDEF]. Иначе B = B' Z. Если Z IN YES[Q], то RETURN [ RCG [G+<* (SX, Z) *>, X (A', B') Y]]. Иначе RETURN [UNDEF].

RW. W-переменная справа. Если B = < >, то RETURN [UNDEF]. Иначе B = B' T, где T - терм. Если T IN YES[Q], то RETURN [ RCG+<* (WX,T) *>, X (A',B') Y]. Иначе RETURN [UNDEF].

RED. Повторная E-переменная справа. Пусть E = SUBST [G, EX]. Если B не кончается на E, то RETURN [UNDEF]. Иначе B = B' E. Если ZT[E] SUBSET YES[Q], то RETURN [RCG G, X (A', B') Y]. Иначе RETURN [UNDEF].

RVD. Повторная V-переменная справа. Пусть V = SUBST [G, VX]. Если B не кончается на V, то RETURN [UNDEF]. Иначе B = B' V. Если ZT[V] SUBSET YES[Q], то RETURN [RCG G, X (A', B') Y]. Иначе RETURN [UNDEF].

LVE. Открытое вхождение E-переменной. В этом месте L#E = (U(Q)X A, B) X, где UX - VE-переменная со спецификатором Q, не входящая в VARS[G].

Пусть B = T1 T2 ... TN, где T1, T2, ..., TN - термы. Обозначим B[K] = T1, T2,..., TK, C[K] = T[K+1], ..., TN, G[K] = RCG [G+<* (UX,BK) *>, A, C[K] X].

Если U(X) E-переменная, то рассмотрим значения К = 0, ..., N, a если U(X) - V - переменная, то рассмотрим значения K = 1, ..., N и найдем минимальное К, для которого C[K] /= UNDEF и, при этом, ZT[B[K]] SUBSET YES[Q]. Если такое K существует, то RETURN [G[K]], иначе RETURN [UNDEF].

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

Пусть требуется вычислить

RCG [<0>, (EX E('A')Y E('B')Z, B)] = D

здесь B - некоторое объектное выражение. Сначала нужно представить B = B' BZ, где все нуль-термы BZ равны 'B', a B' кончается на терм, отличный от 'B', либо пусто. Затем B' представить в виде B' = BX BY, где все нуль-термы выражения BY равны 'A', a BX пусто, или кончается на терм, отличный от 'А'. Затем в качестве D следует взять
D = <* (EX, BX), (EY,BY), (EZ, BZ) *>
Нужно сначала "набрать E('B')Z справа по-максимуму", затем "набрать E('A')Y справа по-максимуму", а затем то, что останется, сделать значением переменной EX. Перебор в процессе отождествления совсем не понадобится.

Выполнение оптимизаций в рассмотренных примерах является корректным в силу сформулированных далее теорем .

Edit | WYSIWYG | Attach | Printable | Raw View | Backlinks: Web, All Webs | History: r7 < r6 < r5 < r4 < r3 | More topic actions
 
R+

This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback