r3 - 25 Aug 2005 - 16:45:36 - OrloVYou are here: TWiki >  Refaldevel Web > FuturePlans > SpecR2

О спецификаторах

По работе С.А.Романенко "Реализация Рефала-2".

Алгоритмы отождествления

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

Пространством спецификаторов называется упорядоченная тройка
(PSPEC,OTERM,YES), где
PSPEC - счетное множество объектов, именуемых первичными спецификаторами
OTERM - счетное множество объектов, именуемых объектными термами
YES - функция, которая каждому первичному спецификатору ставит в соответствие некоторое множество объектных термов
При этом функция YES обладает следующими свойствами:

  1. Для любых первичных спецификаторов P и P'
    YES[P] = YES[P'] => P = P'
  2. Для любых первичных спецификаторов P и P'выполнено хотя бы одно из следующих отношений:
    пересечение YES[P] и YES[P'] пусто
    YES[P] является подмножеством YES[P']
    YES[P'] является подмножеством YES[P]
  3. Для любого первичного спецификатора P
    YES[P] непусто

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

Спецификатором называется конструкция вида
Q1 Q2 ... QN,
где каждое Q[i] - это либо первичных спецификатор, либо отрицание первичного спецификатора. Спецификатор может быть пустым. Семантика первичных спецификаторов задается функцией YES. Для любого первичного спецификатора P, YES[P] - это множество всех тех объектных термов Т, которые удовлетворяют P. Семантика произвольного спецификатора определяется через семантику составляющих его первичных спецификаторов.

Каждый спецификатор представляет собой как бы устройство, имеющее один вход и три выхода: YES, NO, THRU. На вход спецификатора можно подать произвольный объектный термT, который будет проанализирован, и спецификатор либо выдаст на выход сигнал YES или NO, либо пропустит этот терм сквозь себя и выдаст на выход THRU.

Пусть P - произвольный первичный спецификатор, а Q и R - произвольные спецификаторы. Значение функции YES определяется из следующих рекурсивных соотношений:

  1. YES[< >] = <0>
  2. YES[P R] = YES[P] + YES[R]
  3. YES[(P) R] = YES[R ] - YES[P]
Функция YESкаждому спецификатору Q ставит в соответствие то множество объектных термов YES[Q], которое оно изображает.

Далее определяется с помошью рекурсивных соотношений функцию NO, которая каждоу спецификатору Q ставит в соответствие некоторое множество объектных термов NO[Q].

  1. NO[< >] = <0>
  2. NO[P R] = NO[R] - YES[P]
  3. NO[(P) R] = YES[P] + NO[R]
Если X - некоторое множество объектных термов, то через
   _
   X
обозначается его дополнение до множества всех объектных термов.

Функция THRU выражается через функции YES и NO следующим образом:

       ________________   
THRU = [YES[Q] + NO[Q]]
С помощью рекурсивных соотншений определяется унарная операция отрицания:
      _____
   1. [< >] = < >
      _____       ___
   2. [P Q] = (P) [Q]
      _______     ___
   3. [(P) Q] = P [Q]
Для любого спецификатора Q отрицание отрицания Q равно Q.

Используя операцию отрицания, можно выразить значение функции NO через значение функции YES и наоборот.

Определение.
Спецификатор Q называется полным, если

        ______
NO[Q] = YES[Q]
Свойства конкатенации спецификаторов
Пусть даны два спецификатора Q и R. Образуем их конкатенацию QR. Значения функций YES, NO, THRU на спецификаторе QR выражаются через значения этих функций на спецификаторах Q и R.

Достаточные условия полноты спецификаторов.
Пусть W первичный спецификатор, такой что YES[W] совпадает с множеством всех объектных термов, т.е. YES[W] = OTERM.

Теорема
Если спецификатор Q имеет вид Q = Q'W, то Q - полный спецификатор, т.е.

        ______
NO[Q] = YES[Q]

Теорема
Если спецификатор Q имеет вид Q = Q'(W), то Q - полный спецификатор, т.е.

        ______
NO[Q] = YES[Q]

В рефал-программах используются только полные спецификаторы, ибо согласно описанию языка рефал, к каждому спецификатору, встречающемуся в тексте программы, перед его интерпретацией приписывается сзади либо W, если этот спецификатор кончается на правую скобку ")", либо (W), если этот спецификатор не кончается на правую скобку.

Пересечением двух первичных спецификаторов P и P' называется первичный спецификатор, который обозначается P*P' и удовлетворяет условиям:

   1. Если YES[P]*YES[P'] = <0>, то P*P' = < > 
   2. Если YES[P] SUSET YES[P'], то P*P' = P
   3. Если YES[P'] SUSET YES[P], то P*P' = P'

Сужением спецификатора Q по первичному спецификатору P называется спецификатор, который обозначается через CONTR[P,Q] и определяется следующими рекурсивными соотношениями:

   1. CONTR[P,< >] = < >
   2. CONTR[P, QP'] = CONTR[P, Q][P*P']
   3. CONTR[P, Q(P')] = CONTR[P,Q]([P*P'])

Объединением спецификаторов P и Q называется спецификатор, который обозначается R+Q и определяется рекурсивными соотношениями:

   1. < > + Q = < >
   2. [PR] + Q = P[R + Q]
   3. [(P)R] + Q = CONTR[P,Q] [R + Q],
где P - произвольный первичный спецификатор, а R и Q - произвольные спецификаторы.

Пересечением спецификаторов R и Q называется спецификатор, который обозначается R*Q и определяется соотношением

        _______
         _   _
R * Q = [R + Q]

Разностью спецификаторов R и Q называется спецификатор, который обозначается R - Q и определяется соотношением:

            _           
R - Q = R * Q

В описании Рефала разрешается строить спецификаторы не только из первичных спецификаторов, но и из других, ранее определенных спецификаторов.

Элементарным спецификатором называется либо первичный спецификатор, либо конструкция вида <: R :>, где R - спецификатор.

Отрицанием элементарного спецификатора называется конструкция вида (R), где R - элементарный спецификатор.

Спецификатором называется произвольная последовательность
Q1 Q2 ... QN,
где каждое Qi - либо элементарный спецификатор, либо отрицание элементарного спецификатора.

Функция YES, ставящая в соответствие каждому спецификатору Q множество объектных тремов YES[Q], определяется с помощью следующих рекурсивных соотношений:


   1. YES[< >] = <0>
   2. YES[P R] = YES[P] + YES [R]
   3. YES[(P) R] YES[R] - YES[P]
   4. YES[<: Q :> R] = YES[Q] + YES[R]
   5. YES[(<: Q :>) R] = YES[R] - YES[Q]

Оказывается, что для любого спецификатора Q, содержащего конструкции вида <: R :>, можно построить спецификатор Q', такой что YES[Q] = YES[Q'] и при этом Q' не содержит конструкций вида <: R :>.


   1. PLAIN[< >] = (W)
   2. PLAIN[P R] = [P (W)] + PLAIN[R]
   3. PLAIN[(P) R] = PLAIN[R] - [P (W)]
   4. PLAIN[<: Q :> R] = PLAIN[Q] + PLAIN[R]
   5. PLAIN[(<: Q :>) R] = PLAIN[Q] - PLAIN[R]

где P - первичный спецификатор, W - универсальный спецификатор, для которого YES[W]=OTERM, Q и R - спецификаторы. с помощью рекурсивных соотношений определяется операция PLAIN, которая каждому спецификатору ставит в соответствие спецификатор PLAIN[Q], не содержащий конструкций вида <: R :>. При оптимизации рефал-программ требуется распознавать истинность следующих соотношений:

   1. YES[R] * YES[Q] = <0>
   2. YES[R] SUBSET YES[Q]
   3. YES[R] = YES[Q]

при условии, что R и Q - полные спецификаторы. Проверку этих соотношений можно свести к проверке истинности соотношения YES[Q] = <0>, где Q - полный спецификатор.

Будем говорить, что конечное множество первичных спецификаторов <*P1, P2, ..., PN*>, где N >= 2, является разложением первичного спецификатора P, если
YES[P] = YES[P1] + YES[P2] + ... + YES[PN].

Очевидно, что если <*P1, P2,..., PN*> - разложение первичного спецификатора P, то YES[P[I]] SUBSET YES[P] для I = 1,2,...N.

Можно показать, что если мы умеем для любого первичного P и любого конечного множества первичных спецификаторов <*P1, P2,..., PN*> распознавать истинность соотношения
YES[P] = YES[P1] + YES[P2] + ... + YES[PN], то мы можем построить и алгоритм распознавания соотносшения YES[Q] = <0>.

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