Глава 6. Окрестностный анализ
Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений int, SR, ptr Инверсное вычисление ura Окрестностный анализ nan Приложения метавычислений Иные методы Иные приложения [2] Л.В.Парменова «Метавычисления и их применения. Суперкомпиляция» [1] С.М.Абрамов «Метавычисления и их применения» Область возможных новых исследований Окрестностное тестирование Реализация нестандартных семантик Инверсное программиро- вание Методы метавычислений Структура курса
Глава 6. Окрестностный анализ Окрестностный анализ в первые введен в рассмотрение в 1970-ых годах В. Ф. Турчиным, при участии других членов московской Рабочей группы по языку Рефал «неточный», «ad hoc». µ Предложенный здесь окрестностный анализ один из методов метавычислений, инструмент общего назначения для построения формальных ответов на интуитивный вопрос: Какая информация о тексте d была использована, и какая информация о d не была использована в некотором процессе обработки текста d?
Глава 6. Окрестностный анализ: Шаги формализации µ Что такое «информация о d не была использована в некотором процессе обработки текста d»? Какой такой процесс? o(p,d) = { d | процесс p d * r такой же, как p d * r } µ o(p,d) = { d | tr(p,d)=tr(p,d), p d = p d } Понятие окрестности: L-класс O является окрестностью данных d, если d. Подокрестность (O d 2 O d 1 ) и собственная подокрестность (O d 2 < O d 1 ) Не существует бесконечной последовательности O d 1 > O d 2 > O d 3 >...
Глава 6. Окрестностный анализ: Алгоритм nan µ Алгоритм окрестностного анализатора nan: nan p d = (res, O d ), где O d окрестность d такая, что = o(p,d)
Глава 6. Окрестностный анализ µ Наглядная (эксплицированная) форма записи окрестности O d c-переменные в O d соответствуют фрагментам данных d, которые можно варьировать; типы c-переменных и рестрикции в окрестности O d ограничения на допустимые вариации данных фрагментов
Глава 6. Окрестностный анализ: операции над классами 1. Пересечение (*) и разность (\) классов, L-классов, окрестностей. 2. Проверка принадлежности данных классу (алгоритм isElem); 3. Декомпозиции окрестности
Глава 6. Окрестностный анализ: декомпозиция окрестности µ Пусть данные d для программы p имеют вид d=d 1 ++d 2 и =o(p, d 1 ++d 2 ). Получаемые в результате декомпозиции decompose O d1++d2 d 1 d 2 = (O d1, O d2 ) окрестности O di (i = 1, 2) определяют, какая информация о фрагменте d i данных d 1 ++d 2 была использована в процессе p(d 1 ++d 2 ) * res обработки данных d 1 ++d 2
6.1 Основные понятия µ Окрестностный анализ инструмент формализации интуитивного вопроса: Какая информация о тексте d была использована, и какая информация о d не была использована в некотором процессе p обработки текста d?
6.1 Шаги формализации µ Рассматриваем только конструктивные процессы p d * res, где d D и p R. µ Что означают слова: «В процессе p d * res не вся информация о d была использована»? d можно подменить на d такой, что процесс обработки p d * res будет таким же, как p d * res
6.1 Шаги формализации µ Ответ на вопрос « Какая информация о тексте d была использована »?: Множество всех возможных таких подмен d, что d можно подменить на d и процесс обработки p d * res будет таким же, как и процесс p d * res o(p,d) = { d | процесс p d * r такой же, как p d * r } Что такое «процесс p d * r такой же, как и процесс p d * r »?: o(p,d) = { d | tr(p,d)=tr(p,d), p d = p d }
6.1 Множество o(p, d) µ Множество o(p, d) = { d | tr(p,d)=tr(p,d), p d = p d } в точности определяет, какая информация о тексте d была использована, и какая информация о тексте d не была использована в процессе p d * res µ Окажется, что p d o(p, d) представимо L-классом и мы научимся его строить...
6.2 Окрестности µ Определение 9 Пусть O=(ces,rs) L- класс, d [EVal]. Тогда будем называть O окрестностью d (окрестностью с центром d)
6.2 Окрестности µ Часто удобно записывать центр d в верхнем индексе: O d µ Окрестность не может быть пустой: d µ O d будут использованы нами для представления o(p,d) информационная интерпретация:
6.2 Окрестности µ O d будут использованы нами для представления o(p,d) информационная интерпретация, например: µ Если d единственный (не единственный) элемент =o(p,d), то...мнение класса... Если =o(p 1,d), =o(p 2,d) и O d 2 O d 1 (или O d 2 < O d 1 ), то...мнение класса...
6.2 Окрестности Теорема 14 Для любого данного d D множество канонических форм окрестностей d конечно и не существует бесконечной последовательности O d 1 > O d 2 > O d 3 >... окрестностей данных d (невозможно бесконечно уточнять информацию о d)
6.3 Вспомогательные функции алгоритма nan µ Пусть список параметров программы p имеет вид: [parm 1,...,parm n ]. Тогда множество Dom(p) всех возможных входных данных p имеет представление: O 0 = (ces 0, RESTR[]), ces 0 = [cvar 1,...,cvar n ], где cvar 1,... cvar n различные c- переменные и cvar i ca-переменная, если parm i a-переменная, cvar i ce- переменная, если parm i e-переменная.
6.3 Вспомогательные функции алгоритма nan µ Пример. Если список параметров p имеет вид [a.x, a.y, e.z], то: Dom(p)= = гдеces 0 = [A.1, A.2, E.3]
6.3 Вспомогательные функции алгоритма nan µ mkCExps :: Parms -> FreeIndx -> (CExps, FreeIndx) mkCExps [ ] i = ([], i) mkCExps (parm:parms) i= ((cvar:ces), i) where (cvar, i)= case parm of PVE _-> mkCEVar i PVA _-> mkCAVar i (ces, i)= mkCExps parms i
6.3.1 Окрестностный анализатор µ Идея: по заданным p и d выполняем «параллельно и синхронно» два вычисления: эталонное вычисление в точности, как это происходит в int p d обобщенное вычисление в точности, как это происходит в ptr p О 0 построение множеств достижимости О i выбор из дерева процессов только одной ветки, которая соответствует эталонному вычислению process(p, d)
6.3.1 Окрестностный анализатор. Аргументы eval µ eval (t, e) p eval t e ce r ces p i evalT ((t, ce), r) p i O k = (ces, r) µ Аргументы eval µ eval ::Term -> Env -> CEnv -> Restr -> CExps -> ProgR -> FreeIndx -> (EVal, Class)
6.3.1 Окрестностный анализатор µ nan :: ProgR -> [EVal] -> (EVal, Class) nan p d = eval (CALL f prms) e ce (RESTR[]) ces p i where (DEFINE f prms _) : p = p (ces, i)= mkCExps prms 1 e= mkEnv prms d ce= mkEnv prms ces
6.3.1 Окрестностный анализатор µ eval (CALL f args) e ce r ces p i = eval t e ce r ces p i where DEFINE _ prms t = getDef f p e= mkEnv prms (args/.e) ce= mkEnv prms (args/.ce)
6.3.1 Окрестностный анализатор µ eval (ALT c t1 t2) e ce r ces p i = case cond c e of TRUE ue -> eval t1 (e+.ue) ce1 r1 ces1 p i FALSE ue -> eval t2 (e+.ue) ce2 r2 ces2 p i where ((cnt1, cnt2), uce1, uce2, i) = ccond c ce i ((ce1,ces1), r1) = ((ce,ces), r) /. cnt1 ce1 = ce1 +. uce1 ((ce2,ces2), r2) = ((ce,ces), r) /. cnt2 ce2 = ce2 +. uce2
6.3.1 Окрестностный анализатор µ eval exp e ce r ces p i = (res, (ces, r)/.subst) where res= exp/.e cres= cexp/.e (True, subst) = unify [cres] [res]
6.3.1 Окрестностный анализатор µ Теорема 15 Пусть p произвольная программа на TSG, d произвольные входные данные для p, процесс вычисления p на d завершается за конечное число (n) шагов. Тогда алгоритм nan на данных p d завершается (за n выполнений функции eval) со следующим результатом:
6.3.1 Окрестностный анализатор µ Теорема 15 … алгоритм nan на данных p d завершается (за n итераций функции eval) со следующим результатом: nan p d = (res, O d ) где res результат вычисления p на d: p d * res, O d окрестность d такая, что: = o(p,d) = { d | tr(p,d) = tr(p,d), p d = p d }
6.3.1 Окрестностный анализатор µ Утверждение 16 Пусть p R, d произвольные входные данные для p, программа p завершается на данных d, nan p d = (res, O d ) и d. Тогда программа p завершается на данных d с теми же результатом и трассой, что и на данных d, nan p d = (res, O d ) и окрестности O d и O d текстуально совпадают: O d =O d
6.4 Интуитивный смысл окрестностей. Примеры µ Алгоритм nan строит представление O d для o(p, d) µ Здесь: O d описывает, «какая информация о данных d была использована в процессе p d * res» µ Насколько данное описание удобно для человека?... Посмотрим на примере программы pmatch...
6.4 Интуитивный смысл окрестностей. Примеры µ nan pmatch d1 = (SUCCESS, O d1 ) µ d1 = [CONS A NIL, CONS A NIL] µ O d1 =([CONS A.14 A.17, CONS A.14 E.10], RESTR[ ])
6.4 Интуитивный смысл окрестностей. Примеры µ Определение. Позволим изображать: ca-переменную в виде любого надчеркнутого атома, над которым надписан индекс, ce-переменную в виде произвольного дважды надчеркнутого e- значения, над которым надписан индекс.
6.4 Интуитивный смысл окрестностей. Примеры µ Определение. Эксплицированная форма записи окрестности O d =(ces,r): в ces все c-переменные v запишем в указанной выше форме, взяв в качестве надчеркиваемого значения значение v/.s c-переменной, полученное при отождествлении ces с d: (True, s) = unify ces d
6.4 Интуитивный смысл окрестностей. Примеры µ Терминология: надчеркнутые фрагменты d покрыты c-переменными в O d µ d1 = [CONS A NIL, CONS A NIL] µ O d1 =([CONS A NIL, CONS A NIL], RESTR[ ])
6.4 Интуитивный смысл окрестностей. Примеры µ При использовании эксплицированной формы записи окрестности нет необходимости особо указывать центр окрестности: µ O d2 =([CONS A NIL, CONS B NIL], RESTR[A.8 :: A.14]) µ O d3 = ([CONS X NIL, CONS Y NIL], RESTR[A.8 :: A.14])
6.4 Интуитивный смысл окрестностей. Примеры µ O d4 = ([CONS A (CONS B NIL), CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.32 :: A.14, A.32 :: A.20, A.32 :: A.26 ] )
6.4 Интуитивный смысл окрестностей. Примеры µ O d5 = ([CONS Z (CONS A NIL), CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.26 :: A.14, A.26 :: A.20 ] )
6.4 Интуитивный смысл окрестностей. Примеры µ Выводы: окрестности в наглядной форме определяют: какая информация о данных была использована в процессе обработки, a какая нет; какие фрагменты в данных и как можно варьировать, сохраняя неизменным процесс p d * res и его результат.
6.5 Конечное объединение классов C 1,... C n µ Обозначим: 1. [C C n ] список классов [C 1,...,C n ] 2. множество....
6.5 Операции над классами и окрестностями µ Теорема 17 (unifC) Пусть C a = (aces, ar) L-класс, C b = (bces, br) класс, c-переменные из C a не входят в C b, i свободный индекс. Тогда, за конечное число шагов алгоритм unifC: unifC C a C b i * (su, [C b 0,C b 1,... C b n ],i) строит подстановку su для C a и подклассы C b jC b (j = 0,... n, n 1), такие, что:
6.5 Операции над классами и окрестностями CbCb Cb2Cb2... Cb1Cb1 CbnCbn unifC C a C b Cb0Cb0 CaCa
6.5 Операции над классами и окрестностями µ Теорема 17 (unifC)... строит подстановку su для C a и подклассы C b jC b (j = 0,... n, n1), такие, что: 1. =, =Ø, где 0 j < k n 2. =, \ =
6.5 Операции над классами и окрестностями µ Теорема 17 (unifC)... строит подстановку su для C a и подклассы C b jC b (j = 0,... n, n1), такие, что: Eсли = Ø, то C b 0 =C b /.emptC, C b 1 =C b /.idC=C b, C b 0 имеет вид (ces 0,INCONSISTENT), =Ø=, \ = =, и su=[] 4. Eсли Ø, то C b 0 C a 0 (общий подкласс C a и C b ), bces=aces/.su и каждое неравенство из ar/.su входит в br
6.5 Операции над классами и окрестностями CbCb Cb2Cb2... Cb1Cb1 CbnCbn unifC C a C b Cb0Cb0 CaCa
6.5 Операции над классами и окрестностями 1. Обозначим:C b * C a = C b 0, C b \C a = [C b C b n ] 2. Если C a, C b L-классы, то C b 0, C b 1,... C b n L-классы. 3. Объединение, пересечение и разность множеств, представленных конечным объединением L-классов, представимы конечным объединений L-классов. Конечное пересечение множеств, представленных L- классами, представимо L-классом. 4. Если O d 1 и O d 2 окрестности d, то O d 1 * O d 2 окрестность d …интерпретация...
6.6 Проверка принадлежности данных классу µ Утверждение 18 Для любого данного d D = [EVal] и класса C = (ces, r) приведенный ниже алгоритм isElem за конечное число шагов определяет, является ли d элементом множества или нет
6.6 Проверка принадлежности данных классу µ isElem::[EVal]->Class -> Bool isElem d (ces, r) = case (b, r) of (True, RESTR[])-> True (_, _ )-> False where (b,s)= unify ces d r= r/.s
6.7 Декомпозиция окрестности µ Данные d [EVal] имеют вид d=d 1 ++d 2, O d1++d2 окрестность d 1 ++d 2, представляющая o(p, d 1 ++d 2 ). µ Нас интересует построение O d1 и O d2 : 1. Представление O d1 множества всех вариаций d фрагмента d 1 в d 1 ++d 2, сохраняющих неизменным процесс и результат p (d 1 ++d 2 ) * res (...интерпретация...)
6.7 Декомпозиция окрестности 2. Представление O d2 множества всех вариаций d фрагмента d 2 в d 1 ++d 2, сохраняющих неизменным процесс и результат p (d 1 ++d 2 ) * res (...интерпретация...)
6.7 Декомпозиция окрестности O d1 d 1 C O 1 C 1 d 1 ++d 2 O d1++d2 C O 2 C 2 d 2 O d2
6.8 Алгоритм декомпозиции окрестности µ decompose :: Class -> [EVal] -> [EVal] -> (Class,Class) decompose o12 d1 d2 = (o1, o2)where l1= length d1 l2= length d2 i= freeindx 0 o12 (ces1, i1) = mkCEVs [ ] l1 i (ces2, i2)= mkCEVs [ ] l2 i1 c1= (ces1++d2, RESTR[]) c2= (d1++ces2, RESTR[]) (_,((ces1,r1):_)) = unifC c1 o12 -- c1*o12 (_,((ces2,r2):_)) = unifC c2 o12 -- c2*o12 o1 = ( (take l1 ces1), r1 ) --взяли первые l1 o2 = ( (drop l1 ces2), r2 ) --откинули первые l1
6.8 Алгоритм декомпозиции окрестности µ -- генератор списка уникальных -- ce-переменных заданной длины mkCEVs::CVars->Int->FreeIndx -> (CVars,FreeIndx) mkCEVs cvs 0 i = (cvs,i) mkCEVs cvs (n+1) i = mkCEVs (cv:cvs) n i where (cv,i) = mkCEVar i
6.9 Примеры пересечения и декомпозиции окрестностей (1/2) µ Рассмотрим эксплицированные канонические формы результатов реального счета nan pmatch для d4 = [s4, str] и d5 = [s5, str] и последущих строк: µ s4 = (CONS A (CONS B NIL) µ s4 = (CONS Z (CONS A NIL) µ str = (CONS X (CONS Y (CONS Z (CONS A (CONS B NIL)))))
6.9 Примеры пересечения и декомпозиции окрестностей (1/2) (res4, O [s4,str] )= nan pmatch O [s4,str] [s4] [str] (res5, O [s5,str] )= nan pmatch O [s5,str] [s4] [str] (O s4, O str 1 )= decompose O [s4,str] [s4] [str] (O s5, O str 2 )= decompose O [s5,str] [s5] [str] O str 1,2 = O str 1 * O str 2
6.4 Интуитивный смысл окрестностей. Примеры µ O [s4,str] = ([CONS A (CONS B NIL), CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.1 :: A.4, A.1 :: A.5, A.1 :: A.6 ] )
6.4 Интуитивный смысл окрестностей. Примеры µ O [s5,str] = ([CONS Z (CONS A NIL), CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.1 :: A.4, A.1 :: A.5 ] )
6.4 Интуитивный смысл окрестностей. Примеры µ O s4 = (CONS A (CONS B NIL), RESTR [ ]) µ O s5 = (CONS Z (CONS A NIL), RESTR [ ]) 1 1
6.4 Интуитивный смысл окрестностей. Примеры O str 1 = (CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.1::A, A.2::A, A.3::A ]) O str 2 = (CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.1::Z, A.2::Z])
6.4 Интуитивный смысл окрестностей. Примеры O str 1,2 = (CONS X (CONS Y (CONS Z (CONS A (CONS B NIL))))], RESTR [A.1 :: A, A.1::Z, A.2 :: A, A.2::Z ] ) 3 1 2
Глава 6. Окрестностный анализ Окрестностный анализ в первые введен в рассмотрение в 1970-ых годах В. Ф. Турчиным, при участии других членов московской Рабочей группы по языку Рефал «неточный», «ad hoc». µ Предложенный здесь окрестностный анализ один из методов метавычислений, инструмент общего назначения для построения формальных ответов на интуитивный вопрос: Какая информация о тексте d была использована, и какая информация о d не была использована в некотором процессе обработки текста d?
Глава 6. Окрестностный анализ: Шаги формализации µ Что такое «информация о d не была использована в некотором процессе обработки текста d»? Какой-такой процесс? o(p,d) = { d | процесс p d * r такой же, как p d * r } µ o(p,d) = { d | tr(p,d)=tr(p,d), p d = p d } Понятие окрестности: L-класс O является окрестностью данных d, если d. Подокрестность (O d 2 O d 1 ) и собственная подокрестность (O d 2 < O d 1 ) Не существует бесконечной последовательности O d 1 > O d 2 > O d 3 >...
Глава 6. Окрестностный анализ: Алгоритм nan µ Алгоритм окрестностного анализатора nan: nan p d = (res, O d ), где O d окрестность d такая, что = o(p,d)
Глава 6. Окрестностный анализ µ Наглядная (эксплицированная) форма записи окрестности O d c-переменные в O d соответствуют фрагментам данных d, которые можно варьировать; типы c-переменных и рестрикции в окрестности O d ограничения на допустимые вариации данных фрагментов
Глава 6. Окрестностный анализ: операции над классами 1. Пересечение (*) и разность (\) классов, L-классов, окрестностей. 2. Проверка принадлежности данных классу (алгоритм isElem); 3. Декомпозиции окрестности
Глава 6. Окрестностный анализ: декомпозиция окрестности µ Пусть данные d для программы p имеют вид d=d 1 ++d 2 и =o(p, d 1 ++d 2 ). Получаемые в результате декомпозиции decompose O d1++d2 d 1 d 2 = (O d1, O d2 ) окрестности O di (i = 1, 2) определяют, какая информация о фрагменте d i данных d 1 ++d 2 была использована в процессе p(d 1 ++d 2 ) * res обработки данных d 1 ++d 2