Глава 6. Окрестностный анализ. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений.

Презентация:



Advertisements
Похожие презентации
Глава 1. Язык реализации: TSG. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений.
Advertisements

Глава 3. Дерево процессов. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений.
Глава 5. Инверсное программи- рование. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений.
метасистемная лестница
Лекция 2 Языки, операции над языками. Определение 2.1 Языком в алфавите называется произвольное множество цепочек в. Как следует из определения языка,
Глава 7. Окрестностное тестирование программ. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы.
ДРУГИЕ ФОРМЫ РЕКУРСИИ I Функциональноепрограммирование Григорьева И.В.
NP-полнота Теорема Кука. Полиномиальная сводимость Пусть Π 1 =(X 1,Y 1 ) и Π 2 =(X 2,Y 2 ) задачи распознавания. Будем говорить, что Π 1 полиномиально.
Нестандартные приемы решения нестандартных уравнений и неравенств Разработала учитель математики МБОУ «СОШ 38» г.Чебоксары Карасёва Вера Васильевна.
Лекция 2 Предикатное программирование 2. Постановка задачи дедуктивной верификации Программа в виде тройки Хоара, однозначность программы, тотальность.
Иррациональные уравнения. Функциональный метод решения. Лекция 3. Автор : Чипышева Людмила Викторовна, учитель математики МОУ Гимназии 80 г. Челябинска.
Лектор Белов В.М г. Математический анализ Раздел: Введение в анализ Тема: Бесконечно большие последовательности Предел функции (определение и свойства.
Введение в формальные (аксиоматические) системы. Формальные системы - это системы операций над объектами, понимаемыми как последовательность символов.
Что нужно знать: динамическое программирование – это способ решения сложных задач путем сведения их к более простым задачам того же типа динамическое.
Лекция 5 Метод максимального правдоподобия. ММП позволяет получить по крайней мере асимптотически несмещенные и эффективные оценки параметров распределения.
Применение производной к исследованию функций Производная и экстремумы. Исследование функций на монотонность. Урок в 10-3 классе. Учитель – Ирина Геннадьевна.
1 Кубенский А.А. Функциональное программирование. Глава 2. Средства функционального программирования. Потоки. «Завязывание узлов» Часто обработку данных.
Область определения, Область значений функции Функция математическое понятие, отражающее связь между элементами множеств. Более точно, это «закон», по.
1 Кубенский А.А. Функциональное программирование. Глава 2. Средства функционального программирования. Еще один пример функциональной программы
1 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления Рекурсия в лямбда-исчислении fac = λn.(if (= n 0) 1 (* n (fac.
Транксрипт:

Глава 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