Глава 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, как язык логического программирования. Инверсное программирование программ-предикатов предоставляет больше изобразительных средств в распоряжение программиста, нежели традиционные языки логического программирования. Концепция инверсного программирования не исчерпывается инверсным программированием программ-предикатов. Ее можно использовать для гораздо более широкого класса задач.