Корухова Ю.С.
- Главная
- Разное
- Дизайн
- Бизнес и предпринимательство
- Аналитика
- Образование
- Развлечения
- Красота и здоровье
- Финансы
- Государство
- Путешествия
- Спорт
- Недвижимость
- Армия
- Графика
- Культурология
- Еда и кулинария
- Лингвистика
- Английский язык
- Астрономия
- Алгебра
- Биология
- География
- Детские презентации
- Информатика
- История
- Литература
- Маркетинг
- Математика
- Медицина
- Менеджмент
- Музыка
- МХК
- Немецкий язык
- ОБЖ
- Обществознание
- Окружающий мир
- Педагогика
- Русский язык
- Технология
- Физика
- Философия
- Химия
- Шаблоны, картинки для презентаций
- Экология
- Экономика
- Юриспруденция
Синтез функциональных программ при помощи метода дедуктивных таблиц. презентация
Содержание
- 1. Синтез функциональных программ при помощи метода дедуктивных таблиц.
- 2. Содержание Автоматический синтез программ Дедуктивные таблицы Свойства
- 3. Автоматический синтез программ Предпосылки : Увеличение сложности
- 4. Дедуктивные таблицы (1) Один из методов дедуктивного
- 5. Дедуктивные таблицы (2) Структура дедуктивной таблицы
- 6. Дедуктивные таблицы (3) Терм t, не содержащий
- 7. Дедуктивные таблицы (4) Доказательство в дедуктивной таблице
- 8. Свойства дедуктивных таблиц (1) Двойственность строка
- 9. Свойства дедуктивных таблиц (2) Переименование свободных переменных
- 10. Свойства дедуктивных таблиц (3) Добавление примера λ
- 11. Свойства дедуктивных таблиц (4) Тождественные преобразования Эквивалентность
- 12. Свойства дедуктивных таблиц (5) Добавление и удаление
- 13. Дедуктивные правила (1) Вычислимые термы – термы,
- 14. Дедуктивные правила (2) Правило OR- и AND-разделения
- 15. Дедуктивные правила (3) Правило резолюции
- 16. Дедуктивные правила (4) Правило индукции. wf-отношение –
- 17. Дедуктивные правила (5) Правило замены эквивалентных термов
- 18. Пример синтеза функциональной программы (1) Спецификация: z
- 19. Пример синтеза функциональной программы (2) OR-разделение
- 20. Вспомогательные таблицы (1) Пусть в таблице присутствуют
- 21. Вспомогательные таблицы (2) Если t’[a]
- 22. Вспомогательные таблицы (3) Исходная цель Гипотеза
- 23. Вспомогательные таблицы (4) 15.02.2009 Синтез функциональных программ
- 24. Пример вывода вспомогательной таблицы (1) Для функции
- 25. Пример вывода вспомогательной таблицы (2) В ходе
- 26. Исходная цель вспомогательной таблицы
- 27. Конец 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц
- 28. Источники Источники Kreitz, C. Program Synthesis Chapter
Содержание Автоматический синтез программ Дедуктивные таблицы Свойства дедуктивных таблиц Дедуктивные правила Пример синтеза Вспомогательные таблицы Пример ввода вспомогательных таблиц Заключение 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 1Синтез функциональных программ при помощи метода дедуктивных таблиц.
Подготовил: Фастовец Н.Н.
Научный руководитель:
Слайд 2Содержание
Автоматический синтез программ
Дедуктивные таблицы
Свойства дедуктивных таблиц
Дедуктивные правила
Пример синтеза
Вспомогательные таблицы
Пример ввода вспомогательных
таблиц
Заключение
Заключение
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 3Автоматический синтез программ
Предпосылки :
Увеличение сложности ПО
Увеличение требований к надежности ПО
Основные направления:
Дедуктивный
синтез
Индуктивный синтез
Трансформационный синтез
Индуктивный синтез
Трансформационный синтез
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 4Дедуктивные таблицы (1)
Один из методов дедуктивного синтеза.
Спецификация задается в виде формулы
логики предикатов первого порядка
∀x ∃y Q[x,y]
где x – входная переменная,
y – выходная переменная,
Q – логическая формула, устанавливающая связь между входными и выходными переменными.
∀x ∃y Q[x,y]
где x – входная переменная,
y – выходная переменная,
Q – логическая формула, устанавливающая связь между входными и выходными переменными.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 5Дедуктивные таблицы (2)
Структура дедуктивной таблицы
If(A1 ∨ … ∨ An) then (G1
∧ … ∧ Gm)
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 6Дедуктивные таблицы (3)
Терм t, не содержащий свободных (на связанных с квантором)
переменных, удовлетворяет строке таблицы
или
если для некоторой подстановки λ:
Утверждение Aλ не содержит свободных переменных и является ложным (Gλ – истинным)
Если строка имеет выходной терм s, то sλ не содержит свободных переменных и равен tλ.
или
если для некоторой подстановки λ:
Утверждение Aλ не содержит свободных переменных и является ложным (Gλ – истинным)
Если строка имеет выходной терм s, то sλ не содержит свободных переменных и равен tλ.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 7Дедуктивные таблицы (4)
Доказательство в дедуктивной таблице проводиться до получения финальной строки
или
15.02.2009
Синтез
функциональных программ при помощи метода дедуктивных таблиц
Слайд 8Свойства дедуктивных таблиц (1)
Двойственность
строка
эквивалентна строке
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных
таблиц
Слайд 9Свойства дедуктивных таблиц (2)
Переименование свободных переменных
π – перестановка
строка
эквивалентна строке
15.02.2009
Синтез функциональных программ
при помощи метода дедуктивных таблиц
Слайд 10Свойства дедуктивных таблиц (3)
Добавление примера
λ – подстановка
Таблица
эквивалентна
15.02.2009
Синтез функциональных программ при
помощи метода дедуктивных таблиц
Слайд 11Свойства дедуктивных таблиц (4)
Тождественные преобразования
Эквивалентность таблиц не нарушается при применении в
строках тождественных преобразований на основе тождеств алгебры логики:
A ∧ A = A; A ∧ false = false;
A ∨ true = true; ¬ ¬ A = A;
A ∧ A = A; A ∧ false = false;
A ∨ true = true; ¬ ¬ A = A;
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 12Свойства дедуктивных таблиц (5)
Добавление и удаление тождественно истинного утверждения и тождественно
ложной цели
Добавление и удаление свободной переменной
Добавление и удаление свободной переменной
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 13Дедуктивные правила (1)
Вычислимые термы – термы, не содержащие свободных переменных, которые
можно получить на основе уже определенных констант, функций и предикатов.
Таблицы, для которых совпадают множества удовлетворяющих им вычислимых термов термов совпадают, называются подобными.
Таблицы, для которых совпадают множества удовлетворяющих им вычислимых термов термов совпадают, называются подобными.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 14Дедуктивные правила (2)
Правило OR- и AND-разделения
G1,G2,A1,A2 – логические выражения,
t – выходной терм.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 15Дедуктивные правила (3)
Правило резолюции
G1,G2 – логические выражения,
P, P’ – некоторые подвыражения
G1 и G2,
λ – подстановка, для которой Pλ = P’λ,
s и t – выходные термы.
λ – подстановка, для которой Pλ = P’λ,
s и t – выходные термы.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 16Дедуктивные правила (4)
Правило индукции.
wf-отношение – отношение, исключающее бесконечно убывающие цепочки.
Спецификация:
где a
– входной параметр, z – выходная переменная, Q – логическая формула.
Гипотеза индукции:
где
Гипотеза индукции:
где
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 17Дедуктивные правила (5)
Правило замены эквивалентных термов
где G1, G2 – логические выражения,
[L=R]
– подвыражение G1,
T – некоторый терм, входящий в G2, такой что для некоторой подстановки λ:Tλ = Lλ,
s и t – выходные термы.
T – некоторый терм, входящий в G2, такой что для некоторой подстановки λ:Tλ = Lλ,
s и t – выходные термы.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 18Пример синтеза функциональной программы (1)
Спецификация:
z = fact(n) is
if n =
0 then z = 1 else z = n*fact(n-1)
В таблице
согласно тождеству
if A then B else C ≡ A ∧ B ∨ ¬A ∧ C
В таблице
согласно тождеству
if A then B else C ≡ A ∧ B ∨ ¬A ∧ C
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 19Пример синтеза функциональной программы (2)
OR-разделение
Резолюция. Общее подвыражение . (n=0).
Добавление примера{z1←1,z2 ←
n*fact(n-1) }
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 20Вспомогательные таблицы (1)
Пусть в таблице присутствуют строки
где G, F – логические
выражения, a – входной параметр, t[a], t’[a] – термы над входным параметром, x, x’ – выходные переменная, r[a,x], r’[a,x’] – выходные термы. F содержит реплику G.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 21Вспомогательные таблицы (2)
Если t’[a]
все вхождения t[a] на произвольную константу и построить обобщенную цель G’[c,x], которая станет исходной целью для вспомогательной таблицы (соответственно – спецификацией для вспомогательных функций).
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 22Вспомогательные таблицы (3)
Исходная цель
Гипотеза индукции
Воспроизведение шагов доказательства
Резолюция с гипотезой индукции
15.02.2009
Синтез функциональных
программ при помощи метода дедуктивных таблиц
Слайд 23Вспомогательные таблицы (4)
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Лемма
имеющаяся строка
(i)
их резолюция завершает доказательство
их резолюция завершает доказательство
Слайд 24Пример вывода вспомогательной таблицы (1)
Для функции сортировки списка чисел задается спецификация
вида
z = sort(a) is perm(a,z) ∧ ord(z)
perm(x,y) – предикат, равный true, если его аргументы-списки есть перемтановки друг-друга.
ord(x) – предикат, равный true, если его аргумент-список упорядочен.
z = sort(a) is perm(a,z) ∧ ord(z)
perm(x,y) – предикат, равный true, если его аргументы-списки есть перемтановки друг-друга.
ord(x) – предикат, равный true, если его аргумент-список упорядочен.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 25Пример вывода вспомогательной таблицы (2)
В ходе доказательства получается строка
Далее, строка
15.02.2009
Синтез функциональных
программ при помощи метода дедуктивных таблиц
Слайд 26
Исходная цель вспомогательной таблицы
Лемма
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
Слайд 28Источники
Источники
Kreitz, C. Program Synthesis Chapter III.2.5 of Automated Deduction – A
Basis for Applications, pp. 105–134, Kluwer, 1998.
Ayari, A., Basin D.: A High-Order Interpretation Of Deductive Tableau
J. Symbolic Computation (2001) 11, 1-32
Manna Z., Waldinger R.: Fundamentals of Deductive Program Synthesis
IEEE Transactions on Software Engineering, vol. 12, No. 8, August 1992
Traugott J. Deductive Synthesis of Sorting Programs
Journal of Symbolic Computation, vol.7, 1989.
Ayari, A., Basin D.: A High-Order Interpretation Of Deductive Tableau
J. Symbolic Computation (2001) 11, 1-32
Manna Z., Waldinger R.: Fundamentals of Deductive Program Synthesis
IEEE Transactions on Software Engineering, vol. 12, No. 8, August 1992
Traugott J. Deductive Synthesis of Sorting Programs
Journal of Symbolic Computation, vol.7, 1989.
15.02.2009
Синтез функциональных программ при помощи метода дедуктивных таблиц
