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

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



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

Глава 3. Дерево процессов. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений.
Глава 6. Окрестностный анализ. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений.
метасистемная лестница
Глава 7. Окрестностное тестирование программ. Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы.
Метавычисления и их применение (слайды к циклу лекций) Абрамов С.М. Парменова Л.В. Университет города Переславля им. А. К. Айламазяна.
2012 год Кафедра прикладной математики Руководитель работы: д.т.н., проф. Фальк В.Н. Национальный исследовательский университет «МЭИ» Выпускная работа.
ОТОБРАЖАЮЩИЕ ФУНКЦИОНАЛЫ. Важный класс функционалов в практическом программировании на языке Лисп образуют отображающие функции или МАР-функции. МАР-функционалы.
Метавычисления и их применение (слайды к циклу лекций) Абрамов С.М. Парменова Л.В. Университет города Переславля им. А. К. Айламазяна.
Математическая логика. Применение в логике математических методов становится возможным тогда, когда суждения формулируются на некотором точном языке.
Лекция 2 Предикатное программирование 2. Постановка задачи дедуктивной верификации Программа в виде тройки Хоара, однозначность программы, тотальность.
ИМЯ И ЗНАЧЕНИЕ СИМВОЛА Функциональное программирование Григорьева И.В.
Реляционное исчисление. Общая характеристика Запрос – формула некоторой формально-логической теории; описывает свойства желаемого результата. Ответ –
МЕТОДЫ ОПТИМИЗАЦИИ § 1. Основные понятия. Под оптимизацией понимают процесс выбора наилучшего варианта из всех возможных В процессе решения задачи оптимизации.
Выполнила : студ. Гр. 2 У 00 Крутова Н. П. Проверила : Тарбокова Татьяна Васильевна.
Лекция 7: Метод потенциальных функций Предположим, что требуется разделить два непересекающихся образа V1 и V2. Это значит, что в пространстве изображений.
Лектор Янущик О.В г. Математический анализ Раздел: Определенный интеграл Тема: Определенный интеграл и его свойства. Формула Ньютона - Лейбница.
Моделирование в среде Microsoft Office Выполнил ученик 11 б класса НОУ «Эврика» Медведев Сергей Научный руководитель Кошкаров С.А Кошкаров С.А.
Дерево это связный ациклический граф. Связность означает наличие путей между любой парой вершин, ацикличность отсутствие циклов и то, что между парами.
Транксрипт:

Глава 5. Инверсное программи- рование

Супер- компиляция scp Специализация программ Приложения суперкомпиляции, в том числе Базовые понятия и методы метавычислений int, SR, ptr Инверсное вычисление ura Окрестностный анализ nan Приложения метавычислений Иные методы Иные приложения [2] Л.В.Парменова «Метавычисления и их применения. Суперкомпиляция» [1] С.М.Абрамов «Метавычисления и их применения» Область возможных новых исследований Окрестностное тестирование Реализация нестандартных семантик Инверсное программиро- вание Методы метавычислений Структура курса

Глава 5. Инверсное программирование µ Технология программирования, основанная на использовании инверсных вычислений µ Инверсное программирование: программист вместо того, чтобы программировать требуемую в задании функцию f, реализует программу p, функция которой при инверсном вычислении совпадает с функцией f

Глава 5. Инверсное программирование µ С каждым текстом программы p можно связать не одну, а две функции программы: p :: D -> EVal обычная функция программы (семантика): p d = int p d p inv :: D inv -> R inv инверсная функция (семантика) программы: p inv (x,y) = ura p x y где D inv =(Class, Eval) тип запросов на инверсное вычисление; R inv =[(Subst,Restr)] тип результатов инверсного вычисления.

Перенос инверсных вычислений на произвольный язык L мотивация и варианты п еренос а инверсных вычислений с языка R на произвольный язык программирования L µ inv :: ProgR -> D -> Dinv -> Rinv inv intL p (x,y) = ura intL (p.:.x) y where (.:.) :: ProgL->Class -> Class p.:.(ces,r) = ((p:ces),r)

Корректность переноса инверсных вычислений Теорема. Пусть L произвольный язык программирования, p L- программа, intL L/R -интерпретатор, x класс, обобщенное данное для p, y значение. Тогда вычисление: inv intL p (x, y) * [(s 1,r 1 ), (s 2,r 2 ),...] реализует инверсное вычисление и выполнено:

Корректность переноса инверсных вычислений 1. Классы x i = x/.s i /.r i попарно непересекающиеся подклассы класса x 2. Для любого i и любого данного d программа p определена на d и p d *= y 3. Для любого данного d, на котором программа p определена и p d * L y, существует номер i такой, что d. Кроме того, в данном случае, префикс длины i списка будет построен inv intL p (x, y) за конечное число шагов

Глава 5. Инверсное программирование µ Сравнение логического программирования с инверсным программированием программ- предикатов: Свойства инверсного программирования программ- предикатов позволяют рассматривать язык L inv, как язык логического программирования. Инверсное программирование программ-предикатов предоставляет больше изобразительных средств в распоряжение программиста, нежели традиционные языки логического программирования. Концепция инверсного программирования не исчерпывается инверсным программированием программ-предикатов. Ее можно использовать для гораздо более широкого класса задач.