Логико-термальная эквивалентность
Отношение эквивалентности Е, заданное на парах стандартных схем, называют корректным, если для любой пары схем S1 и S2 из S1 ~Е~ S2 следует, что S1~ S2, т. е. S1 и S2 функционально эквивалентны.
Поиск разрешимых корректных отношений эквивалентности представляет значительный интерес с точки зрения практической оптимизации преобразования программ, поскольку в общем виде функциональная эквивалентность стандартных схем алгоритмически неразрешима.
Идея построения таких (корректных и разрешимых) отношений связанна с введением понятия истории цепочки схем. В истории с той или иной степенью детальности фиксируются промежуточные результаты выполнения операторов рассматриваемой цепочки. Эквивалентными объявляются схемы, у которых совпадают множества историй всех конечных цепочек.
Одним из отношений эквивалентности является логико-термальная эквивалентность (ЛТЭ).
Определим термальное значение переменной х для конечного пути w схемы S как терм t (w, x), который строится следующим образом.
1.Если путь w содержит только один оператор А, то: t (w, x) = t, если А – оператор присваивания, t (w, x) = х, в остальных случаях.
2.Если w = w’Ае, где А – оператор, е – выходящая из него дуга, w ’ – непустой путь, ведущий к А, а x1, …, xn – все переменные терма t (Ае, x), то t (w, x) = t (Ае, x)[ t (w’, x1)/ x1, …, t (w’, xn)/ xn ].
Понятие термального значения распространим на произвольные термы t:
t (w, x) = t [ t (w, x1)/ x1, …, t (w, xn)/ xn ].
|
|
|
Например, пути start (х); y:=x; p1 (x); x:=f (x); p 0(y); y:=x; p 1(x); x:=f (x) в схеме на рисунке 1.5, а соответствует термальное значение f (f (x)) переменной х.
Для пути w в стандартной схеме S определим ее логико-термальную историю (ЛТИ) lt (S, w) как слово, которое строится следующим образом.
1.Если путь w не содержит распознавателей и заключительной вершины, то lt (S, w) – пустое слово.
2.Если w = w’vе, где v – распознаватель с тестом p (t1,..., tk), а е – выходящая из него Δ-дуга, Δ 
{0,1}, то
lt (S, w) = lt (S, w’) p Δ(t (w’, t1), …, t (w’, tk)).
3.Если w = w’v, где v – заключительная вершина с оператором stop (t1,..., tk), то lt (S, w) = lt (S, w’) t (w’, t1) … t (w’, tk).
Например, логико-термальной историей пути, упомянутого в приведенном выше примере, будет p1 (x) p0 (x) p1 (f (x)).
Детерминантом (обозначение: det (S)) стандартной схемы S называют множество ЛТИ всех ее цепочек, завершающихся заключительным оператором.
Схемы S1 и S2 называют ЛТЭ (лт - эквивалентными) S1 ~ЛТ~ S2, если их детерминанты совпадают.
Приведем без доказательства следующие утверждение:
Логико-терминальная эквивалентность корректна, т. е. из ЛТЭ следует функциональная эквивалентность (S1 ~ЛТ~ S2 
S1 ~ S2). Обратное утверждение как видно из рисунка 1.5 не верно.
ЛТ – эквивалентность допускает меньше сохраняющих ее преобразований, чем функциональная эквивалентность.
|
|
|
Дата добавления: 2015-12-20; просмотров: 23; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!