Системы представления знаний Knowledge Representation Systems Автоматический синтез программ Automatic Program Synthesis Ф.А. Новиков

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ2 из 35 Тема 6. Автоматический синтез программ ä 6.1. Задача автоматического синтеза ä 6.2. Дедуктивный синтез программ ä 6.3. Синтез программ на основе метода резолюций ä 6.4. Структурный синтез программ ä 6.5. Индуктивный синтез программ

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ3 из 35 ä Идеал: ä Автоматический синтез программы – по спецификации задачи ä Подходы: ä Дедуктивный синтез = логический вывод ä Индуктивный синтез = по примерам ä Трансформационный синтез = трансляция ä Утилитарный синтез = все остальное 6.1. Задача автоматического синтеза программ Задача Программа Синтез

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ4 из 35 История развития 1 ä 60-е годы XX века: начало ä АДТ, LISP, Метод резолюций АСП ä Логическая верификация ~ дедуктивный синтез ä 70-е годы XX века: первая волна ä Дедуктивный синтез алгоритмически неразрешим Сэр Чарльз Энтони Ричард Хоар, род ä «быстрая сортировка» ä язык Z спецификаций ä параллельная модель взаимодействия последовательных процессов (CSP, Communicating Sequential Process) ä аксиоматика Хоара

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ5 из 35 История развития 2 Дана Стюарт Скотт, род ä исследования теории моделей, теории автоматов, конструктивной математики ä деривационная семантика языков программирования ä 80-е годы: спад Непейвода Николай Николаевич, род ä теория неформализуемых понятий и теории логического синтеза программ на базе конструктивных логик ä методика логического подхода ä интуиционистское доказательство теоремы существования = программа

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ6 из 35 История развития 3 ä 90-е годы XX века: застой ä ООП не способствует синтезу ä XXI век: вторая волна ä Генеративное программирование ä Исполнимые визуальные спецификации ä Модельно-центрированная разработка (Model Driven Architecture – MDA) ä UML ä... СКИФ 4

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ7 из Дедуктивный синтез программ ä Задача: заданы два предиката: ä предусловие P(x) ä постусловие Q(x, y) ä Теорема: ä x (P(x) y Q(x,y)) ä x (P(x) Q(x,f(x))) – сколемизация ä Схема доказательства: нотация Хоара ( наука программирования ) ä P(x) {y: = f(x)} Q(x, y) Задача Теорема Доказательство Программа

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ8 из Дедуктивный синтез программ ä Тотальная корректность proc f(x); y:=x; while Q(x, y) do y:=random(y) end while return y end proc ä Эффективность ä Алгоритма синтеза ä Синтезированной программы ä Реализуемость proc f1(x); y:=f(x); Iif Q(x,y) then return y else return fail end if end proc ä Q(x, y, z) = n>2 x, y, z (x n +y n =z n ) ä Из любого конструктивного доказательства теоремы существования может быть извлечена императивная программа

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ9 из Дедуктивный синтез на основе метода резолюций 1. P(u,x,y,z,s1) P(x,x,y,z,load(a,s1)) 2. P(u,x,y,z,s2) P(u+y,x,y,z,add(b,s2)) 3. P(u,x,y,z,s3) P(u,x,y,u,store(c,s3)) 4. P(e1,e2,e3,e4,d) 5. P(u,x,y,x+y,s) ANS(s) 6. P(x+y,x,y,z,s1) ANS(store(c,s))5,3 7. P(x,x,y,z,s2) ANS(store(c,add(b,s)))6,2 8. P(u,x,y,z,s3) ANS(store(c,add(b,load(a,s))))7,1 9. ANS(store(c,add(b,load(a,d))))8,4 Программа в функциональной форме Одноадресная машина с тремя ячейками и сумматором Задача: c:=a+b Команды: load, add, store

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ10 из 35 Алгоритм извлечения программы из доказательства ä Вход: дерево вывода T 0 (в узлах - предложения) ä Выход: схема программы T (дерево решений) ä Шаг 1: на дуги отрицание литерала с унификатором (T 1 ) ä Шаг 2: удаление всех узлов (и ребер), где нет ANS (T 2 ) ä Шаг 3: переворот дерева и удаление предложений (T 3 ) ä Шаг 4: удаление литералов на дугах, выходящих из узлов с одним выходом (T)

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ11 из 35 Пример: синтез программы y := if x>0 then 1 else –1 end if 1. P(x) Q(x,1) P(x) Q(x, 1) 2. P(x) Q(x,-1) P(x) Q(x, –1) 3. Q(x,y) ANS(y) 4. P(x) ANS(1)1,3 5. P(x) ANS(–1)2,3 6. ANS(1) ANS(–1) 4,5

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ12 из 35 Преобразование дерева вывода P(x ) )(xP y:=1 y:= –1 )1,()(xQxP )(),(yANSyxQ )(),(yANSyxQ )1,()( xQxP )1()1( ANS )1()( xP )1()( ANSxP Q(x,1) y:=1 Q(x,1) Q(x,-1) Q(x,-1) y:=-1 P(x) Дерево доказательства Синтезированная блок-схема

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ13 из 35 Синтез невыполнимой программы ä Аксиомы: ä P(x) Q(x, 1) ä P(x) Q(x, –1) ä Цель: ä Q(x, y) ANS(y) ä Вывод: ä Q(x, 1) Q(x, –1)1,2 ä Q(x, –1) ANS(1)3,4 ä ANS(1) ANS(–1)3,5

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ14 из 35 Синтез невыполнимой программы Дерево доказательства Невыполнимая блок-схема )1,()(xQxP )(),(yANSyxQ )(),(yANSyxQ )1()1( ANS )1()1,( xQ )1,()( xQxP )1()1,(ANSxQ )(xP)(xP )1,(xQ )1,( xQ 1: )1,( y xQ 1: )1,( y xQ )1,( xQ 1: )1,( y xQ 1: y

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ15 из 35 Примитивная резолюция (1) ä Примитивные символы исходной спецификации (константы, функциональные символы, предикаты) – те, которым разрешается появляться в синтезированной программе ä P, 1, – 1 примитивные ä Q не примитивный ä Жизненное предложение – содержит предикат ANS ä Жизненная переменная – входит в жизненное предложение ä P(x) Q(x, 1) не жизненное ä Q(x, –1) ANS(1) жизненное

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ16 из 35 Примитивная резолюция (2) ä C 1 L 1 C 2 L 2 C, где =Н.О.У.(L 1,L 2 ) ä C является примитивной резольвентой, если ä С 1 и С 2 - НЕ жизненные или ä С 1 - жизненное, С 2 - не жизненное и все константы и функции, подставляемые вместо жизненных переменных в являются примитивными ä С 1 и С 2 - жизненные и все константы функции, подставляемые вместо жизненных переменных в являются примитивными и предикаты L 1 и L 2 являются примитивными ä Примитивная резолюция полна

Пример: y := if x>0 then 1 else –1 end if Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ17 из 35 )1,()(xQxP )(),(yANSyxQ )(),(yANSyxQ )1,()( xQxP )1()1( ANS )1()( xP )1()( ANSxP )1,()(xQxP )(),(yANSyxQ )(),(yANSyxQ )1()1( ANS )1()1,( xQ )1,()( xQxP )1()1,(ANSxQ Не жизненная!

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ18 из R(0,1)R(x,y):= y=f(x)f(0)=1 2. R(x,y) R(x+1,(x+1)*y)f(x+1)=(x+1)*f(x) ( y R(0,y) x ( y 1 R(x,y 1 ) y 2 R(x+1,y 2 ))) x y R(x,y) 3. R(0, y 2 ) ANS(y 2 ) 4. R(y 1,y 2 ) 5. R(y 1 +1, y 2 ) ANS(y 2 ) Синтез циклических программ (1) y:=y 2 y 1 :=0 y 1 =x y 1 x y 1 :=y 1 +1 A B Специальная схема для частного случая

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ19 из 35 Синтез циклических программ (2) ä Синтез программы А: ä 6. ANS(1) из1,3 т.е. A = y 2 :=1 ä Синтез программы B: ä 7. R(y 1 +1,(y 1 +1)*y 2 ) ANS(y 2 ) из 2,3 ä 8. ANS((y 1 +1)*y 2 ) из 5,7 ä т.е. A = y 2 :=(y 1 +1)*y 2 В общем случае невозможно автоматически догадаться, какую схему нужно применить y 1 :=0 y 1 =x y:=y 2 y 1 x y 1 :=y 1 +1 y 2 :=(y 1 +1)*y 2 y 2 :=1

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ20 из Структурный синтез программ ä Синтез программ из операторов: не стоят трудов ä Примитивы: не операторы, а БОЛЬШИЕ компоненты (библиотека программ) ä Правильность программы определяется правильностью компонент (не доказывается) ä Синтезируется только управляющая структура (все вычисления заданы заранее в компонентах) ä Ограничение: нет времени ( x := f(…, x, …) )

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ21 из 35 История развития ä 70-е годы XX века: Таллинн ä Тыугу Энн Харальдович, род ä идея структурного синтеза программ ä система ПРИЗ – Программа Решения Инженерных Задач - реализация ä 80-е: Ленинград под руководством С.С. Лаврова ä идея была значительно развита ä несколько десятков реализаций ä Настоящее время: В.Б.Новосельцев ä programming in constraints, СКИФ 4

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ22 из 35 Синтез программ в концептуальных базах знаний ä База знаний: понятия (величины, атрибуты) и система отношений (связей) = модель предметной области M ä Этапы: ä Синтезируется «абстрактная» программа решения исходной задачи в концептуальной компоненте базы знаний M (здесь же проводится анализ разрешимости задачи) ä Конкретизация зависимостей конкретная программа ä Вычислительная задача Дерево анализа задачи Программа решения задачи

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ23 из 35 Модель предметной области (Семантическая вычислительная сеть) Направленный двудольный граф Модель предметной области: M = {( X f Y)} f F, X V, Y V Задача: на M найти W по U Множество функций F Множество переменных V x y f g M

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ24 из 35 Алгоритм прямой волны Proc Wave (U, W, M) : P S:=U;P:= S:=U;P:= L:if W S then return OK end if g:=nil for f F do if X(f) S & Y(f) S then g:=f end if if X(f) S & Y(f) S then g:=f end if end for if g=nil then return fail else S:=S Y(g); F:=F\{g}; P:=P+g; go to L end if end proc Трудоемкость O(|M| 2 ) Обратная волна - чистка программы

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ25 из 34 Предварительная обработка МПО Каждый узел входит в 2 двухсвязных списках

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ26 из 35 Proc S(u) for x X(u) do del(x) if f(x).l=nil then if f(x).l=nil then G:=G+f /* */ G:=G+f /* применима */ end if end if end for for y Y(u) do del(y) if f(y).r=nil then if f(y).r=nil then G:=G\{f} /* */ G:=G\{f} /* бесполезна */ end if end if end for end proc Алгоритм Диковского-Ульмана Proc DU(U,W,M) P:=nil; G:=nil for u U do W:=W\{u}; S(u) end for L:if W= then return P end if if G=nil then return fail end if g:=car(G); G:=cdr(G); P:=P+g for y Y(g) do S(y); W:=W\{y} end for go to L end proc P - синтезируемая программа G - список применимых функций Линейный по длине модели f(u) - функциональный узел для узла u

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ27 из 35 Расширения и границы применимости ä Условные предложения вычислимости ä определяется условие, при котором можно использовать некоторое уравнение ä синтезируются линейно-ветвящиеся программы ä R-предложения вычислимости ä отношения, а не функции; граф неориентированный ä отношения, а не функции; граф неориентированный ä процедуры ä Рекуррентные предложения вычислимости ä составляются по уравнениям типа F[n] = F[n–1]+F[n–2] ä циклические программы определенного вида ä Предложения вычислимости с функционалами ä процедуры с процедурными параметрами ä Рекурсивные предложения вычислимости ä рекурсивные программы ограниченного вида

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ28 из Индуктивный синтез программ ä Очень любопытный подход, но не очень популярный ä Синтез программ по примерам (протоколам выполнения) ä Синтез общих утверждений по частным ä Синтез доказательства для общего случая по доказательствам для частных случаев ä Т.е. усмотрение общих закономерностей: повторений, прогрессий, …

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ29 из 35 Многоточечные термы ä Алфавит A: N – числа, W – буквы, U – разделители ( ) [ ] { }, T – специальные … ä Символьная разность: x y := 0, если x=y; x-y, если x,y N; не определено в остальных случаях ä …-терм: выражение D= где a i,b i A и q Z i 1 in b i =a i b i a i =q q называется фактором …-терма ä Значение …-терма V(D):=d 1 0 …d n 0 d 1 1 …d n 1 … … d 1 |q| …d n |q| где d i 0 = a i, d i |q| =b i и d i j d i j–1 = 0, если b i =a i ; d i j d i j–1 = +1, если b i a i >0; d i j d i j–1 = –1, если b i a i >0

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ30 из 35 Многоточечные слова и выражения ä Если X N или X W, то X …-слово ä Если X …-слово, то (X) {X} [X] …-слова ä Если X и Y …-слова, то XY …-слово ä Если X и Y …-слова, то …-слово если выполнены условия …-терма если выполнены условия …-терма ä Значение …-слова: рекурсивно по термам Пример: E = … > V(E) = (4)(3)(3)(2)(2)(1) = (4)(3)(3)(2)(2)(1) ä …-выражение это …-слово с параметром k … > ä …-выражение это …-слово с параметром k … >

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ31 из 35 Формальные примеры ä Пример использования языка …-выражений A(2) then A(1) A(2);… if A(k-1)>A(k) then A(k-1) A(k);> … A(2) then A(1) A(2);… if A(1)>A(2) then A(1) A(2);>> ä Формальный пример – значение …-выражения для заданного значения k ä Значение предыдущего …-выражения для k=3 if A(1)>A(2) then A(1) A(2); if A(2)>A(3) then A(2) A(3); if A(1)>A(2) then A(1) A(2); if A(2)>A(3) then A(2) A(3); if A(1)>A(2) then A(1) A(2); ä …-выражения – форма записи циклических программ

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ32 из 34 Правила вывода ä Подслово Y слова X называется (s,t) регулярным, если оно является значением …-терма D = ä Подслово Y слова X называется (s,t) регулярным, если оно является значением …-терма D = ä M(X) max входящее из N, m(X) – min ä f – некоторая целочисленная функция ä Правило A f : ищем самое левое максимальное (s,t)- регулярное подслово, такое что t>f(M(X)) и заменяем его на …-терм ä Правило B: числа х > (M(X)+m(X))/2 заменяем выражением k-c, где с = M(X)-x ä Правило В применимо только если не применимо A f

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ33 из 35 Вывод...-выражения из формального примера ä Пусть слово: X = A(1) A(2) A(3) A(4) A(1) A(2) A(3) A(1) A(2) A(1) ä Ограничение: f – целая часть квадратного корня, f(M(X))=2 Вывод A(1) A(2) A(3) A(4) A(1) A(2) A(3) A(1) A(2) A(1) A(1) A(2) A(3) A(1) A(2) A(1) A(1) A(2) A(1) A(1) … >

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ34 из 35 Основной результат ä Два …-выражения называются почти эквивалентными, если их значения совпадают почти для всех значений k ä X c k>c (S Af,B (V(X,k) X) ä Для любого …-выражения существует такая константа, что для любого формального примера этого выражения, более длинного, чем заданная константа, результат индуктивного синтеза по данному примеру почти эквивалентен исходному …-выражению

Ф. Новиков. SPZ. Тема 6. Автоматический синтез программ35 из 35 Вот и все, что было...