r5 - 25 Jul 2005 - 09:03:14 - Luba ParmyonovaYou are here: TWiki >  Refaldevel Web > FuturePlans > SpecR2 > Algorithms > OptTheorem

Переупорядочение дыр

Теорема 1.

Пусть G - подстановка, а X и Y - кортежи пар выражений. Рассмотрим множество W[G,X], упорядоченное отношением линейного порядка, и выберем в нем самую левую подстановку DX из числа таких подстановок D, что W[D, Y] /= <0>. Тогда
RCG[G, X Y] = RCG[DX, Y]

Теорема 2.

Пусть G - подстановка, а X и Y - такие кортежи пар выражений, что
VARS[X] * VARS[Y] SUBSET VARS[G]

Тогда, если DX IN W[G,X] и DY IN W[G,Y], то DX + DY IN W[G, X Y].

Теорема 3.

Пусть G - подстановка, а X и Y такие кортежи пар выражений, что
VARS[X] * VARS[Y] SUBSET VARS[G].

Тогда RCG [G, X Y] = RCS [G, X] + RCG [G, Y].

Теорема 4.

Пусть G - подстановка, а X и Y, Z такие кортежи пар выражений, что
VARS[X] * VARS[Y] SUBSET VARS[G] + VARS[Z].

Тогда RCG [G, Z X Y] = RCS [G, Z Y X].

Теорема 5.

Пусть G - подстановка, а X1, X2,,...,XN, Y1, Y2,...,YN - кортежи из пар выражений. Обозначим
X = X1 X2 ... XN
Y = Y1 Y2 ... YN
Z = X1 Y1 X2 Y2 ... XN YN
тогда, если
VARS[X] * VARS[Y] SUBSET VARS[G]
то
RCG [G, Z] = RCG [G, X] + RCG [G, Y]

Отделение удлиняющегося выражения

Если B - объектное выражение, через ZT[B] обозначается множество составляющих его нуль-термов.

Если A - типовое выражение, через ZT[A] обозначается объединение всех множеств ZT [SUBST [D, A]], где D - некоторая подстановка, применимая к A. Рассматриваются только такие подстановки, где VARS [D] = VARS [A].

Для любых типовых выражений A' и A'' справедливо

ZT [A' A''] SUBSET ZT [A'] + ZT [A''].

Равенство

ZT [A' A''] = ZT [A'] + ZT [A''] может и не иметь места.

Если А - типовое выражение (которое, в частности, может быть и объектным выражением, A = T1 T2 ... TN), нуль-длиной выражения называется целое число N и обозначается через ZL[A].

Теорема.

Пусть G - подстановка, L#M = (A' A'', B) X, где A' и A'' - типовые выражения, B - объектное выражение, а X - кортеж из пар выражений. Пусть EZ - E-переменная, не входящая в множество VARS [G] + VARS [L] и при этом выполняются следующие условия:

  1. для любых двух подстановок, D1 и D2 применимых к A', и таких, что G SUBSET D1 и G SUBSET D2, из того, что ZL [SUBST [D1, A']] < ZL [SUBST [D2, A']] следует, что D1 < [(A')] D2 (D1 "левее, чем" D2 на A')
  2. VARS [A'] * [VARS [A''] + VARS [X]] SUBSET VARS [G]
  3. для любых объектных выражений C', C'' и C таких, что B = C' C C'', из того, что W [G, (A', C' C)] /= <0> и W [G, (A'', C'')] /= <0> следует, что W [G, (A'', C C'')] /= <0>

Обозначим D = RCG [G, (A' EZ, B)]. Тогда, если D = UNDEF, то и RCG [G, L#M] = UNDEF. Если D /= UNDEF, то RCG [G, L#M] можно вычислить следующим образом.

Представим D в виде

D = G + D0 + < EZ, B > , где VARS[G], VARS[D0] и < EZ > попарно не пересаются. Тогда

RCG [G, L#M] = D0 + RCG [G, (A'', B'') X].

Теорема.

Пусть G - подстановка, L#M = (A' A'', B) X, где А' и A'' - типовые выражения, B - объектное выражение, X - кортеж из пар выражений. Пусть EZ - E-переменная, входящая в множество VARS [G] + VARS [L] и при этом выполняются следующие условия:

  1. A' имеет вид A' = U(X) A0, где U(X) - VE - переменная, A0 - типовое выражение, такое что каждая VE - переменная, входящая в A0 на нулевом уровне скобок, принадлежит множеству VARS [G] + <* UX *>
  2. VARS [A'] * [VARS [A''] + VARS [X]] SUBSET VARS [G]
  3. A'' имеет вид A'' = T1 T2 ... TN U(R)Y A1, где А1 типовое выражение, UY - VE - переменная, а T1 T2 ... TN - типовые термы, которые не являются VE-переменными, такие что
ZT[A'] = SUBSET ZT[T1] SUBSET ZT[T2] SUBSET ... ZT[TN] SUBSET YES[R]
и при этом попарно не пересекаются множества
VARS[G] + VARS[A'] + VARS [A1] + VARS [X], VARS[T1], VARS [T2], ..., VARS[TN], < UY >.

Обозначим D = RCG [G, (A' EZ, B)]. Тогда, если D = UNDEF, то и RCG [G, L#M] = UNDEF. Если D /= UNDEF, то RCG [G, L#M] моцно вычислить следующим образом.

Представим D в виде
D = G + D0 + < EZ, B'' >, где VARS [G], VARS [D0] и < EZ > попарно не пересекаются. Тогда
RCG [G, L#M] = D0 + RCG [G, (A'', B'') X]

Отделение максимальных выражений

Пусть T - множество объектных термов, а B - объектное выражение. Рассмотрим множество выражений B', удовлетворяющее условиям:

  1. существует выражение B'', такое что B = B' B''
  2. ZT[B'] SUBSET T.

Это множество непусто, и все входящие в него выражения имеют разную нуль-длину. В нем существует единственое выражение, имеющее максимальную длину. Это выражение обозначается LMAX[T, B].

Аналогично рассматривается множество объектных выражений B'', удовлетворяющее условиям:

  1. существует выражение B', такое что B = B' B''
  2. ZT[B''] SUBSET T. (ZT[B'] - множество составляющих его нуль-термов).

Самое длинное выражение из этого множества обозначается RMAX[T, B].

Теорема 1.

Пусть L#M = X (A' A'', B) Y (L#M - кортеж из упорядоченных пар (LI, MI), L - типовое выражение, M - образ) и B = B' B'', где B' = LMAX [ZT [A'], B].

Тогда значение выражения A' не может быть длиннее, чем выражение B', т.е. для любого отождествления D из W [G, L#M] существует такое выражение C, что B' = C' C, где C' = SUBST [D, A'].

Теорема 2.

Пусть L#M = X (A' A'', B) Y и B = B' B'', где B'' = RMAX [ZT [A''], B].

Тогда значение выражения A'' не может быть длиннее, чем выражение B'', т.е. для любого отождествления D из W [G, L#M] существует такое выражение C, что B' = C C'', где C'' = SUBST [D, A''].

Теорема 3.

Пусть L#M = X (A' A'', B) Y, ZT [A'] * ZT [A''] = <0> и B = B' B'', где B'' = LMAX [ZT [A'], B]. Тогда RCG [G, X (A' A'', B) Y] = RCG [G, X (A' B')(A'' B'') Y]

Теорема 4.

Пусть L#M = X (A' A'', B) Y, ZT [A'] * ZT [A''] = <0> и B = B' B'', где B'' = RMAX [ZT [A'], B]. Тогда RCG [G, X (A' A'', B) Y] = RCG [G, X (A' B')(A'' B'') Y]

Теорема 5.

Пусть L#M = X (A' A'' A0, B) Y, ZT [A'] * ZT [A''] = <0> и B = B' B'', где B' = LMAX [ZT [A'] B]. Тогда, если для любой подстановки D из W [G, L#M] верно SUBST [D, A''] /= < >, то
RCG [G, X (A' A'' A0, B) Y] = RCG [G, X (A', B') (A'' A0, B'') Y]

Теорема 6.

Пусть L#M = X (A0 A'' A', B) Y, ZT [A'] * ZT [A''] = <0> и B = B' B'', где B' = RMAX [ZT [A'] B]. Тогда, если для любой подстановки D из W [G, L#M] верно SUBST [D, A''] /= < >, то
RCG [G, X (A0 A' A'', B) Y] = RCG [G, X (A0 A'', B'') (A', B') Y]

Теорема 7.

Пусть G - подстановка, L#M = X ( E(Q1)1 E(Q2)2 ... E(QN)N) - вхождения Е-переменных, а U(R)A - вхождение VE-переменной. Пусть каждая из переменных E1, E2, ..., EN, UA входит в L только один раз и не входит в VARS[G]. Пусть B = B'' B', где B' = RMAX [YES[R], B]. Тогда
RCG [G, L#M] = RCG [G, X (E(Q1)1 E(Q2)2 ... E(QN)N, B'') (U(R)A, B') Y]

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

С помощью рекурсивных соотношений определяют функцию ZTS, которая каждому типовому выражению A ставит в соответствие спецификатор ZTS[A].


   1. ZTS [< >] = (W)
   2. ZTS [T A] = ZTS [T] + ZTS[A]
   3. ZTS [Z] = Z (W)
   4. ZTS [(A)] = B (W)
   5. ZTS [S(Q)X] = [S (W)] * Q
   6. ZTS [W(Q)X] = Q
   7. ZTS [E(Q)X] = Q
   8. ZTS [V(Q)X] = Q

где B и W - первичные спецификаторы, изображающие множества объектных термов вида (А) и всех объектных термов соответственно, A - произвольное типовое выражение, T - произвольный типовой терм, Z - произвольный символ, S(Q)X, V(Q)X, W(Q)X, E(Q)X - вхождения произвольной S-, W-, V-, E-переменной соответственно со спецификатором Q.

Теорема.

Для любого типового выражения A, ZTS [A] - полный спецификатор.

Теорема.

Для любого типового выражения A справедливо
ZT [A] SUBSET YES [ZTS [A]]

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

Требуется проверить соотношение вида
ZT [A] SUBSET ZT [U(R)Y], где A - типовое выражение, а U(R)Y - вхождение VE-переменной со спецификатором R. Следует заметить, что ZA [A] SUBSET YES [ZTS [A]], а ZT [U(R)Y] = YES [R]. Достаточным условияем того, что чтобы соотношение ZT [A] SUBSET ZT [U(R)Y] выполнялось, является справедливость соотношения YES [ZTS [A]] SUBSET YES [R]. Последнее равносильно соотношению YES [R - ZTS [A]] = <0>.

Требуется вычислять выражения вида LMAX [ZT [A], B] и RMAX [ZT [A], B], где A - типовое, B - объектное выражение. На практике A - это вхождение VE-переменной со спецификатором Q. В этом случае ZT [A] = YES [Q], поэтому приходится вычислять только LMAX [YES [Q], B] и RMAX [YES [Q], B].

Требуется проверять справедливость соотношений вида ZT [A'] * ZT [A''] = <0>, где А' и A'' - типовые выражения. Поскольку ZT [A'] = SUBSET YES [ZTS [A']], ZT [A''] SUBSET YES [ZTS [A'']], достаточным условием справедливости проверяемого соотношения является справедливость соотношения YES [ZTS [A']] * YES [ZTS [A''] = <0>], которое равносильно соотношению YES [ZTS [A'] * ZTS [A'']] = <0>. Последнее можно проверить с помощью алгоритма распознавания YES[Q] = <0>.

-- Luba Parmyonova - 21 Jul 2005

Edit | WYSIWYG | Attach | Printable | Raw View | Backlinks: Web, All Webs | History: r5 < r4 < r3 < r2 < r1 | 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