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

1 Глава 1. Язык реализации: TSG

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

3 Язык программирования Определение [А. П. Ершов] Язык программирования L = (P L, D L, S L ), где P L синтаксис, множество синтаксически правильных программ (строк), обычно заданное грамматикой D L предметная область, множество данных; иногда определяют еще входные D in L, выходные D out L, промежуточные данные D run L S L :: P L ×D L D L семантика, функция (частичная и вычислимая), которая определяет, выдает ли какой-либо результат r D L (или не выдает) программа p P L на входных данных d D L : p d * L r S L (p,d) = r

4 Предметная область Предметная область D: D = (ATOM Atoms) | (CONS D D) Atoms конечное множество атомов (будем использовать строки) S-выражения заимствованы из Лиспа. Стандартное представление строк: "ABBA" (CONS (ATOM "A") (CONS (ATOM "B") (CONS (ATOM "B") (CONS (ATOM A") (ATOM "Nil")))))

5 Предметная область Сокращенная запись атомов: (ATOM "string") 'string "ABBA" (CONS 'A (CONS 'B (CONS 'B (CONS 'A 'Nil)))) Универсальность D: таких структур достаточно для представления любых данных А-значение атом, (ATOM a) Е-значение любое значение либо атом ( ATOM a) либо CONS-пара e-значений: (CONS е е)

6 Синтаксис TSG-программ prog ::= [def 1,... def n ] 1n def ::= (DEFINE fname [parm 1,...parm n ] term) 0n term ::= (ALT cond term 1 term 2 ) | (CALL fname [arg 1,... arg n ]) 0n | e-exp cond ::= (EQA? a-exp 1 a-exp 2 ) | (CONS? e-exp e-var 1 e-var 2 a-var) a-exp ::= a-val | a-var e-exp ::= a-val | a-var | e-var | (CONS e-exp 1 e-exp 2 ) parm ::= a-var | e-var arg ::= a-exp | e-exp a-var ::= (PVA name) e-var ::= (PVE name)

7 Синтаксис TSG-программ Все имена функций в определениях различны Каждая вызываемая функция должна быть определена Каждая переменная, используемая в выражении, должна быть определена в окружающем контексте (DEFINE fname [v 1,... v n ] term) v 1,... v n можно использовать в term (ALT (CONS? exp ev 1 ev 2 av) term 1 term 2 ) ev 1 ev 2 можно использовать в term 1 av можно использовать в term 2

8 Синтаксис TSG-программ PVA-переменная (PVA "name") a.name может принимать только a-значения PVE-переменная (PVE "name") e.name может принимать любые е-значения Как следствие: значением a-выражения может быть только a-значение значением е-выражения может быть только е-значение

9 Синтаксис TSG-программ Совместимость а/е-типов при вызове функций: (DEFINE fname [prm 1,...prm n ] term) (CALL fname [arg 1,... arg n ]) Длины списков параметров и аргументов должны быть равны Если prm k a-переменная, то arg k a-выражение (если prm k е- переменная, то arg k е-выражение...)

10 Синтаксис TSG-программ Совместимость а/е-типов при вызове программы: p=[(DEFINE main[prm 1,...prm n ] term),…] d k D: p [ d 1,... d n ] *... Длины списков параметров у main и входных данных должны быть равны Если prm k a-переменная, то d k a-значение (если prm k e- переменная, то d k е-значение...)

11 Проверка вхождения одной строки в другую match = [ (DEFINE "Match"[e.subs, e.str] (CALL "CheckPos"[e.subs, e.str, e.subs, e.str])), (DEFINE "CheckPos"[e.subs, e.str, e.subs1, e.str1] (ALT (CONS e.subs e.subs-head e.subs-tail a._) (ALT (CONS e.subs-head e._ e._ a.subs-head) FAILURE (ALT (CONS e.str e.str-head e.str-tail a._) (ALT (CONS e.str-head e._ e._ a.str-head) FAILURE (ALT (EQA a.subs-head a.str-head) (CALL "CheckPos"[e.subs-tail, e.str-tail, e.subs1, e.str1]) (CALL "NextPos"[e.subs1, e.str1]))) FAILURE)) SUCCESS)), (DEFINE "NextPos"[e.subs, e.str] (ALT (CONS e.str e._ e.str-tail a._) (CALL "Match"[e.subs, e.str-tail]) FAILURE)) ]

12 Определение семантики TSG S R :: P R ×D R D R семантика, функция (частичная и вычислимая), которая определяет, выдает ли какой-либо результат r D R (или не выдает) программа p P R на входных данных d DR: p d * R r S R (p,d) = r Подход: определение семантики через определение интерпретатора

13 Определение семантики TSG Среда список пар env = [… (var := value) …] Состояние вычисления пара s = (term, env) Процесс process(p,d) вычисления программы p над данными d последовательность переходов от одного состояния вычисления программы p к другому p d r p d * r process(p,d) = s 0 s 1 … s n

14 Вспомогательные функции в описании интерпретатора getDef fname prog в программе prog находит определение функции с именем fname getDef fn p = head[ d | fn' _ _)<-p, fn' == fn] mkEnv vars vals построение среды по списку переменных vars и списку значений vals mkEnv vars vals = zipWith (:=) vars vals Пример: mkEnv [a.x, a.y, e.z, e.u] ['A, 'B, (CONS 'D 'E), 'F ] = [a.x:='A, a.y:='B, e.z:=(CONS 'D 'E), e.u:='F]

15 Вспомогательные функции в описании интерпретатора t /. env замена в t вхождений переменных на их значения из env, «посчитать значение выражения на среде». Пример: (CONS (CONS a.x e.z) a.y)/. [a.x:='A, a.y:='B, e.z:='C] = (CONS (CONS A C) B) env+.env' обновление среды env средой env'. Пример: [a.x:='A,a.y:='B,e.z:='C] +. [e.z:=(CONS 'D 'E),e.u:='F] = [e.z:=(CONS 'D 'E),e.u:='F,a.x:='A,a.y:='B]

16 Интерпретатор языка TSG (1/2) int :: ProgR -> [EVal] -> EVal int p ds = eval s p where (DEFINE f prms _) : p' = p e = mkEnv prms ds s = ((CALL f prms), e) eval :: State -> ProgR -> EVal eval f args), e) p = eval s' p where DEFINE _ prms t' = getDef f p e' = mkEnv prms (args/.e) s' = (t',e') eval c t1 t2), e) p = case cond c e of TRUE ue -> eval (t1,e+.ue) p FALSE ue -> eval (t2,e+.ue) p eval p = exp/.e

17 Интерпретатор языка TSG (2/2) (функция cond) data CondRes = TRUE Env | FALSE Env cond :: Cond -> Env -> CondRes cond (EQA? x y) e = let x' = x/.e; y' = y/.e in case (x', y') of (ATOM a, ATOM b) | a==b -> TRUE [ ] (ATOM a, ATOM b) -> FALSE[ ] cond (CONS? x vh vt va) e = let x' = x/.e in case x' of CONS h t ->TRUE [vh:=h,vt:=t] ATOM a ->FALSE[va:=x']

18 Глава 1 обзор и выводы Предметная область D: D = (ATOM Atoms) | (CONS D D) Синтаксис TSG. Плоский функциональный полный язык, типизированные программные переменные, два вида условий: (EQA? a-exp 1 a-exp 2 ) (CONS? e-exp e.i e.j a.k) Пример программы: проверка вхождения одной строки в другую Семантика TSG: предъявлен Haskell-текст интерпретатора int. Состояние s i вычисления программы p над данными d: (term, env)

19 Глава 1 обзор и выводы Процесс process(p,d) вычисления программы p над данными d последовательность переходов от одного состояния вычисления программы p к другому p d r p d * r process(p,d) = s 0 s 1 … s n

20 Глава 1 обзор и выводы Трасса tr(p,d) вычисления программы p над данными d последовательность значений (для TSG это логические значения TRUE и FALSE), описывающих, какие варианты продолжения (какие ветви в конструкциях ветвления) избирались в процессе вычисления p над d в те моменты вычисления, когда в принципе были возможны различные варианты продолжения вычисления tr(p,d) = [ b 1, b 2,... ], где b i {TRUE, FALSE}

21 Глава 1 Заключение Фиксация языка реализации для конкретности изложения, точности построений и обоснований. Все построения и рассуждения могут быть повторены и для любого другого языка реализации со свойствами: алгоритмическая полнота и предметная область языка построена при помощи некоторого алфавита атомов и конечного набора жестких конструкторов.