7. Технология предикатного программирования Базовые трансформации Подстановка определения на место вызова Замена хвостовой рекурсии циклом Склеивание переменных Метод обобщения исходной задачи Трансформация кодирования структурных объектов Пример. Сортировка простыми вставками Лекция 7 Предикатное программирование

7. Технология предикатного программирования

метод управляемой полуавтоматической трансляции применением последовательности трансформаций, преобразующих предикатную программу в эффективную императивную программу на императивном расширении языка P Базовыми трансформациями являются: - склеивание переменных, реализующее замену нескольких переменных одной; - замена хвостовой рекурсии циклом; - подстановка определения предиката на место его вызова; - кодирование структурных объектов низкоуровневыми структурами с использованием массивов и указателей.

Подстановка определения предиката на место вызова A(x: y) { S } определение предиката на императивном расширении языка P, а A(e: z) вызов предиката в теле предиката B. x, y, z списки переменных, а e список выражений. Подстановка определения предиката на место вызова A(e: z) есть замена вызова композицией: | x | = | e |; { S }; | z | = | y | (7.1) x и y становятся локальными переменными предварительное систематическое переименование переменных. Исполнение (7.1) эквивалентно исполнению вызова A(e: z). |x| = |e| - групповой оператор присваивания раскрытие группового оператора

x состоит из x 1, x 2, …, x n ; а e - e 1, e 2, …, e n. Пусть e j - переменная. e j должна быть отлична от x j. Почти всегда замена x j на e j дает эквивалентную программу. Склеивание x j с e j уменьшает число переменных на 1 и позволяет удалить x j = e j в групповом операторе |x| = |e|. Склеивание переменных x j и e j корректно кроме случая, когда x j перевычисляется внутри S, что возможно как результат склеивания x j с другими переменными, а переменная e j используется не только в вызове A(e: z), но и после него. Еще одно условие: до проведения замены x j на e j переменная e j не должна встречаться в измененной версии S в (7.1); последнее возможно в случае, когда проведено склеивание переменных x k и e k, причем e k совпадает с e j. Склеивание результирующих переменных набора y с переменными набора z. Поскольку переменные, входящие в набор z должны быть различными, то склеивание результатов всегда возможно. В результате склеивания результатов устраняется групповой оператор |z| = |y|. Отмеченное склеивание (замену x j на e j и y j на z j ) можно не проводить, если склеиваемые переменные обозначены одинаковыми идентификаторами в исходной программе. Если имеется вызов A(e: z) и требуется запрограммировать определение предиката A, то в качестве результирующих параметров y в определении A выбираются переменные набора z. Переменные в составе набора e становятся соответствующими аргументами определения A с учетом ограничений, указанных выше.

Замена хвостовой рекурсии циклом Это специальный случаем подстановки определения предиката на место вызова Рекурсивный вызов определяет хвостовую рекурсию, если: имя вызываемого предиката совпадает с именем определяемого предиката, в теле которого находится вызов; вызов является последней исполняемой конструкцией в определении предиката, содержащем вызов. last(S) - множество последних исполняемых конструкций в операторе S. Тогда: last(A; B) = last(B), last(if (C) A else B) = last(A) last(B), last(D(e: z)) = {D(e: z)}, last(A || B) =. Однако если A || B реализуется последовательным исполнением A и B, например, как B; A, то last(A || B) = last(A). Умн(nat a, b: nat c) { if (a = 0) c = 0 else c = b + Умн(a – 1, b) } не хвостовая рекурсия!! D(nat a, b: nat c) { if (a = b) c = a else if (a < b) D(a, b - a: c) else D(a - b, b: c) } это хвостовая рекурсия

Определение предиката A(x: y) { S } Вызов A(e: z) с хвостовой рекурсией внутри S. Тогда этот вызов должен иметь вид A(e: y), т.е. z = y. Подставим определение предиката A на место вызова A(e: y). Получим: |x| = |e|; { S }. Обозначим через S оператор, полученный заменой в S подстановкой определения на место вызова A(e: y). Можно заменить в S второе вхождение S передачей управления на начало оператора S. В итоге определение предиката A преобразуется к виду: A(x: y) { M: S }, где S получается из S заменой вызова A(e: y) парой операторов: |x| = |e|; goto M. трансформация замены хвостовой рекурсии циклом.

D(nat a, nat b: nat c) { M:if (a = b) c = a else if (a < b) |a, b| = |a, b - a|; goto M else |a, b| = |a - b, b|; goto M } Раскроем групповые операторы присваивания, а также заменим фрагмент с операторами перехода на цикл for. Получим: D(nat a, nat b: nat c) { for ( ; ; ) { if (a = b) {c = a; break; } if (a < b) b = b – a else a = a – b }

Склеивание переменных Трансформация склеивания переменных - замена нескольких переменных одной. a b, c - замена всех вхождений имен b и c на имя a. Условия корректности, гарантирующих эквивалентность определений предиката до и после проведения склеивания. Задачи экономии памяти в классических работах А.П. Ершова, С.С. Лаврова, В.В. Мартынюка. Склеиваются переменные одного типа, между которыми имеется информационная связь. В каждом операторе программы определяются аргументы и результаты оператора. Результат оператора может быть склеен с любым аргументом соответствующего типа при условии, что аргумент не используется далее после завершения исполнения оператора. Сложные формы склеивания.

Метод обобщения исходной задачи Проблема приведения рекурсии к хвостовому виду. Техника автоматических преобразований. М етод обобщения исходной задачи для получения решения с хвостовой формой рекурсии. Умн(nat a, b: nat c) { if (a = 0) c = 0 else c = b + Умн(a – 1, b) } Прием – использование дополнительного параметра d качестве накопителя. Умн1(nat a, b, d: nat c) pre a 0 & b 0 & d 0 post c = a b + d; Умн(a, b: c) Умн1(a, b, 0: c). Тогда: Умн(nat a, b: nat c) pre a 0 & b 0 { Умн1(a, b, 0: c) } post c = a b;

Умн1(nat a, b, d: nat c) pre a 0 & b 0 & d 0 { if (a = 0) c = d else Умн1(a – 1, b, d + b: c) } post c = a b + d; Склеивание c d. Умн1(nat a, b, c: nat c) { if (a = 0) c = c else Умн1(a – 1, b, с + b: c) } Замена хвостовой рекурсии циклом: Умн1(nat a, b, c: nat c) {M: if (a = 0) else |a, b, c| = |a – 1, b, с + b|; goto M } Раскрытие группового оператора и оформления цикла: Умн1(nat a, b, c: nat c) {for (; a 0 ;) {a = a – 1; c = с + b} } Подстановка определения на место вызова |a, b, c| = | a, b, 0 |; for (; a 0 ;) {a = a – 1; c = с + b} Раскрытие группового оператора: c = 0; for (; a != 0 ;) {a = a – 1; c = с + b}

Трансформация кодирования структурных объектов Пример. Программа суммирования sum(s: c) эл-тов посл-ти s. type seqR = list (real); formula SUM(seqR s, real c) = s = nil ? c = 0 : exists real a. SUM(s.cdr, a) & c = s.car + a; sum(seqR s: real c) { switch (s){ case nil: c = 0 case cons(h, t): c = h + sum(t) } } post SUM(s, c); sum(seqR s: real c) nil?(s) or cons?(s) = true { if (nil?(s)) c = 0 else {{h = s.car || t = s.cdr}; c = h + sum(t)} } post SUM(s, c); sum(seqR s: real c) { if (s = nil) c = 0 else c = s.car + sum(s.cdr) } post SUM(s, c);

type seqR = list (real); formula SUM( seqR s, real c) = s = nil ? c = 0 : exists real a. SUM(s.cdr, a) & c = s.car + a; sum(seqR s: real c) post SUM(s, c); sum_total: lemma exists c. SUM(s, c); formula SUMG( seqR s, real d, c) = e. SUM(s, e) & c = e + d; sumG(seqR s, real d: real c) post SUMG(s, d, c); sum(seqR s: real c) { sumG(s, 0: c) } post SUM(s, c); Цель: SUM(s, c) => sumG(s, 0: c) Правило FB1.R(x, y) P(x) & Q(x, y) R(x, y) LS(A(x: y)) sum_FB1: lemma SUM(s, c) => SUMG(s, 0, c);

formula SUM( seqR s, real c) = s = nil ? c = 0 : exists real a. SUM(s.cdr, a) & c = s.car + a; formula SUMG( seqR s, real d, c) = e. SUM(s, e) & c = e + d; sumG(seqR s, real d: real c) { if (s = nil ) c = d else sumG(s.cdr, d + s.car : c) } post SUMG(s, d, c) measure len(s); Цель: Induct(s,V) & SUMG(s, d, c) => LS( ) Правило FB3. R(u, x, y1) m(u) < m(x) & P(u) & Q(u, y1) Лемма 17. Induct(x, V) & R(u, x, y1) LS(A(u: y1)) sum_if: lemma SUMG(s, d, c) => s = nil ? c = d : len(s.cdr) < len(s) & SUMG(s.cdr, d + s.car, c)

sumG(seqR s, real d: real c) { if (s = nil ) c = d else sumG(s.cdr, d + s.car : c) } post SUMG(s, d, c) measure len(s) ; Склеивание c d. sumG(seqR s, real с: c) { if (s = nil ) c = c else sumG(s.cdr, c + s.car : c) } Замена хвостовой рекурсии циклом. При раскрытии группового оператора меняется порядок присваивания параметрам s и с. sumG(seqR s, real с: real c) { for (; s != nil; ) { с = с + s.car; s = s.cdr } Подстановка определения на место вызова real c = 0; for (; s != nil; ) { с = с + s.car; s = s.cdr }

Кодирование списка вырезкой массива Кодирование начального и текущего состояния списка S type SEQR = array (real, M..N); Начальное S[m..n], текущее S[j..n]. SEQR S; int j = m; Значения границ M и N должны быть достаточными, т.е. M m, n, j N. Кодирование операций: s = nil j > n s != nil j

Кодирование списка через указатели type LISTP = struct (real car, LISTP *cdr); LISTP *S; s S Кодирование операций: s = nil S = NULL s != nil S != NULL s.car S->car s = s.cdr S = S->cdr Итоговая программа real c = 0; for ( ; S != NULL; ) { c = с + S->car; S = S->cdr } real c = 0; for (; s != nil; ) { c = с + s.car; s = s.cdr }

Пр имер. Сортировка простыми вставками type T{ :axiom a. a a, axiom a, b. a b & b a a = b, axiom a, b, c. a b & b c a = c, axiom a, b. a b b a }; type S = list (T); Свойство сортированности списка s : SORT(s) s1, s2 S. a, b T. (s = s1 + a + b + s2 a b) }; Лемма 7.1. SORT(nil) & a T. SORT( [[a]] ). Лемма 7.2. len(s) 1 s = nil a. s = [[a]]. Лемма 7.3. len(s) 1 SORT(s). sort(s) s vub sort1(u, b, v) pop_into(u, b) pop_into1(y, z, b) b b u yz

perm(u, v) s1,s2,s3 S. a,b T. u = s1 + a + s2+ b + s3 & v = s1 + b + s2+ a + s3 Свойство перестановочности: PERM(u, v) u = v w. perm(u, w) & PERM(w, v) Лемма 7.4. length(u) 1 & PERM(u, v) u = v. sort(S s: S s) post SORT(s) & PERM(s, s); Штрих в имени s предполагает склеивание sort1(S u, T b, S v: S r) pre u != nil & SORT(u) post SORT(r) & PERM(u + b + v, r); Лемма 7.5. Спецификация sort1 тотальна и однозначна, Лемма 7.6. len(s) > 1 s = s.car + s.cdr.car + s.cdr.cdr sort(S s: S s) {if (len(s) 1) s' = s elsesort1(s.car, s.cdr.car, s.cdr.cdr: s') } post SORT(s) & PERM(s, s); sort_: lemma Q_sort(s, s) => len(s) 1 ? s' = s : P_sort1(s.cdr) & Q_sort1( s.car, s.cdr.car, s.cdr.cdr, s' )

pop_into(S u, T b: S w) pre u != nil & SORT(u) post SORT(w) & PERM(u + b, w); Лемма 7.7. Спецификация pop_into тотальна и однозначна. sort1(S u, T b, S v: S r) pre u != nil & SORT(u) {pop_into(u, b: S w); if (v = nil ) r = w elsesort1(w, v.car, v.cdr: r) } post SORT(r) & PERM(u + b + v, r) measure len(v); sort1_1: lemma P_sort1(u) => P_ pop_into (u) sort1_2: lemma P_sort1(u) & Q_sort1(u, b, v, r) & Q_pop_into(u, b, w) => v = nil ? r = w : len(v,cdr) < len(v) & P_sort1( w ) & Q_sort1( w, v.car, v.cdr, r )

pop_into(S u, T b: S w) pre u != nil & SORT(u) post SORT(w) & PERM(u + b, w); pop_into1(S y, z, T a, b: S w) pre SORT(y + a + z) & (z != nil b z.car) post SORT(w) & PERM(y + a + b + z, w); Лемма 7.8. Спецификация pop_into1 тотальна и однозначна. pop_into(S u, T b: S w) pre u != nil & SORT(u) {pop_into1(prec(u), nil, last(u), b: w) } post SORT(w) & PERM(u + b, w); pop_into_FB1: lemma P_pop_into(u) & Q_pop_into(u, b, w) => P_pop_into1(prec(u), nil, last(u), b) & Q_pop_into1(prec(u), nil, last(u), b, w);

pop_into1(S y, z, T a, b: S w) pre SORT(y + a + z) & (z != nil b z.car) {if (a b) w = y + a + b + z elseif (y = nil) w = b + a + z elsepop_into1(prec(y), a + z, last(y), b: w) } post SORT(w) & PERM(y + a + b + z, w) measure len(y) ; Лемма 7.9. PERM(v, w) & SORT(v) & SORT(w) v =w. Pop_into1_: lemma P_pop_into1(y, x, a, b) & Q_pop_into1(y, x, a, b, w) => a b ? w = y + a + b + z : y = nil ? w = b + a + z: len(prec(y)) < len(y) & P_pop_into1( prec(y), a + z, last(y), b) & Q_pop_into1( prec(y), a + z, last(y), b, w)

Склеивания s sort(S s: S s) {if (len(s) 1) s = s elsesort1(s.car, s.cdr.car, s.cdr.cdr: s) } s r; u w; sort1(S u, T b, S v: S s) {pop_into(u, b: S u); if (v = nil ) s = u elsesort1(u, v.car, v.cdr: s) } u w; pop_into(S u, T b: S u) {pop_into1(prec(u), nil, last(u), b: u) };

Замена хвостовой рекурсии циклом. Раскрытие групповых операторов м офорление циклов. В pop_into1 две коллизии sort1(S u, T b, S v: S s) {for (; ;) { pop_into(u, b: S u); if (v = nil ) {s = u; break} else{ b = v.car; v = v.cdr} } pop_into1(S y, z, T a, b: S u) {for (; ;) { if (a b) { u = y + a + b + z; break} elseif (y = nil) { u = b + a + z; break} else{z = a + z; a = last(y); y = prec(y)} }

Подстановка sort1 на место вызова в sort и pop_into1 в pop_into. sort(S s: S s) {if (len(s) 1) return S u =s.car; T b = s.cdr.car; S v = s.cdr.cdr; for (; ;) { pop_into(u, b: S u); if (v = nil ) {s = u; break} else{b = v.car; v = v.cdr } } pop_into(S u, T b: S u) {T a = last(u); S y = pred(u); S z = nil; for (; ;) { if (a b) { u = y + a + b + z; break} elseif (y = nil) { u = b + a + z; break} else{z = a + z; a = last(y); y = prec(y)} }

Подстановка pop_into на место вызова в sort. sort(S s: S s) {if (len(s) 1) return ; S u = s.car; T b = s.cdr.car; S v = s.cdr.cdr; for (; ;) { T a = last(u); S y = pred(u); S z = nil; for (; ;) { if (a b) { u = y + a + b + z; break} elseif (y = nil) { u = b + a + z; break} else{z = a + z; a = last(y); y = prec(y)} } if (v = nil ) {s = u; break} else{b = v.car; v = v.cdr } }

Кодирование списков type SEQ(int p, q) = array p..q of T; S w SEQ(p, q) w = nil p > q len(w) p – q + 1 b = w.car; w := w.cdr b := W[p]; p := p + 1 a = last(w); w := prec(w) a := W[q]; q := q – 1 SEQ(0, n) K; int n; //номер последнего эл-та списка u K[0..i - 1]; b K[ i ]; v K[i +1..n] y K[0..j - 2]; a K[j - 1]; b K[j]; z K[j +1..i] yz v b i j u b ab

S u = s.car и S v = s.cdr.cdr int i = 1 S y = prec(u) и S z = nil int j = i z = a + z K[j] = a sort(S s: S s) { if (n 0) return ; int i = 1; T b = K[1]; for (; ;) { T a = K[i - 1]; int j = i; for (; ;) { if (a b) { K[j] = b; break} elseif (j < 2) { K[0] = b; K[1] = a; break} else{K[j] = a; a = K[j - 2]; j = j - 1 } } if (i >= n) break else{ b = K[i + 1]; i = i + 1 } }

type SEQ(int p, q) = array p..q of T; int n; //номер последнего элемента списка SEQ(0, n) K;... if (n 0) return ; T b = K[1]; for (int i = 1; ;) { T a = K[i - 1]; for (int j = i; ; j = j – 1) { if (a b) { K[j] = b; break} elseif (j = 1) { K[0] = b; K[1] = a; break } else{ K[j] = a; a = K[j - 2] } } if (i = n) break else{ i = i + 1; b = K[i] } } b = K[i] ….. a b для a = K[i - 1] K[j] = b избыточный

pop_into(S u, T b: S w) pre u nil & SORT(u) {T a = last(u); if (a b) w = u + b else pop_into2(prec(u), a, b: w) } post SORT(w) & PERM(u + b, w); pop_into2(S y, z, T b: S w) pre SORT(y + z) & z nil & b z.car {if (y = nil) w = b + z else T c = last(y); if (c b) w = y + b + z else pop_into2(prec(y), c + z, b: w) } post SORT(w) & PERM(y + b + z, w);