Математические основы Отношения порядка Наименьшая неподвижная точка Язык исчисления вычислимых предикатов (прод.) Рекурсивные определения типов Логическая. - презентация

1 Математические основы Отношения порядка Наименьшая неподвижная точка Язык исчисления вычислимых предикатов (прод.) Рекурсивные определения типов Логическая и операционная семантика Вызов предиката Оператор суперпозиции Параллельный оператор Условный оператор Конструктор предиката Конструктор массива Программа на языке CCP Предикаты в качестве параметров предикатов Правила построения заместителей Рекурсивные определения предикатов Пример программы Лекция 3 Предикатное программирование

2 4.Математические основы 4.1.Отношения порядка 4.2.Наименьшая неподвижная точка

3 Отношения порядка (D, R) отношение порядка R D D; a R b (a, b) R a D. a R a рефлексивность a D. a R a иррефлексивность a,b D. a R b b R a симметричность a,b D. a R b & b R a a = b антисимметричность a,b,c D. a R b & b R c a R c транзитивность (D, ) частично упорядоченное множество (чум) - рефлексивно, антисимметрично, транзитивно; - частичный порядок Частичный порядок линейный (или тотальный) a,b D. (a b b a). - строгий частичный порядок - иррефлексивно, антисимметрично, транзитивно. (D, ) предпорядок - рефлексивно и транзитивно (D, R) отношение эквивалентности R рефлексивно, симметрично и транзитивно

4 a S наименьший (наибольший) элемент S D s S. a s ( s S. s a ) (bottom) и (top) a D верхняя грань S D s S. s a a D наименьшая верхняя грань S D b D. (b верхняя грань a b) a = lub(S) least upper bound a S минимальный элемент S D b S. ( b a b =a ) нижняя грань, наибольшая нижняя грань, максимальный элемент нижняя полурешетка ч у м с нижней гранью полная решетка ч у м с нижней и верхней гранью Лемма 4.1. Нижняя (верхняя) полурешетка является полной решеткой. вполне упорядоченное множество всякое подмножество имеет нижнюю грань ч у м со свойством обрыва бесконечно убывающих цепей (well-founded partial order) всякое подмножество имеет минимальный элементwell-founded partial order

5 Наименьшая неподвижная точка (D,, ) частично упорядоченное множество с нижней гранью: a D. a - нижняя полурешетка Последовательность {a m } m 0 является возрастающей цепью, если a 0 a 1 … a m …. F: DD монотонная функция a,b D. a b F(a) F(b) Лемма 4.2. {F n ( )} n0 для монотонной функции F определяют возрастающую цепь: F( ) F 2 ( ) … F n ( ) … Лемма 4.3. Если F монотонна и a 0 a 1 a 2… возрастающая цепь, то F(a 0 ) F(a 1 ) F(a 2 )… также возрастающая цепь

6 m 0 a m lub {a m } m 0 наименьшая верхняя грань цепи F: DD непрерывная функция возрастающей цепи {a m } m 0. F( m 0 a m ) = m 0 F( a m ) Лемма 4.4. Непрерывная функция является монотонной. x = F(x) решением этого уравнения является неподвижная точка функции F Теорема 4.1 Клини. F непрерывна. Тогда n 0 {F n ( )} наименьшая неподвижная точка F

7 3. Язык исчисления вычислимых предикатов (продолжение)

8 Рекурсивные типы данных Z = Subset(T, x, P, d) (1) типовый терм Z = X Y (2) φ(X, Y) Z = X + Y (3) Z = Set(X) (4) Z = Pred(D: E) (5) X k = φ k (X 1, X 2,…, X n, T 1, T 2,…, T s ); k = 1,…,n; n > 0, s0 (3.8) система типовых уравнений X = (X 1, X 2,…, X n ), φ = (φ 1, φ 2,…, φ n ) X = φ(X) векторная форма (3.9) (Γ,, ) множество типов; Z Γ. Z нижняя грань Вектора типов X Y k=1..n (X k Y k ) = (,,…, ) нижняя грань ( Φ,, ) множество векторов типов Лемма. ( Φ,, ) является нижней полурешеткой

9 X 0 =, X m+1 = φ(X m ), m 0.(3.10) Лемма. {Y m } m 0 возрастающая цепь типов. a m 0 Y m ( k. n>k. a Y n ) Лемма. Произведение Y Z и объединение Y + Z непрерывны относительно вхождений компонентных типов Y и Z. {Y m } m 0 и {Z m } m 0 возрастающие цепи типов. m 0 (Y m Z m ) = ( m 0 Y m ) ( m 0 Z m ). Лемма 3.1. Функция φ системы (3.9) определений рекурсивных типов X = φ(X) является непрерывной относительно произведения и объединения. По теореме Клини решением системы X = φ(X) является наименьшая неподвижная точка, определяемая как m 0 X m, при условии, что рекурсия реализуется через произведение и объединение

10 Запрещается рекурсия Y = Q(Subset(H(Y))) Z = Q(Set(H(Z))) A = Q(PRED(H(A), …: …) B = Q(PRED(…: H(B), …), где Q и H некоторые функционалы, представленные типовыми термами

11 Логическая и операционная семантика Логика программы набор предикатов {L p } на значениях переменных для разных точек p программы 1. Предикат L p (z) истинен, когда исполнение программы находится в точке p. 2. Если предикат L p (z) истинен на некотором наборе значений z=z 0, то существует исполнение с такими значениями переменных в точке p. Язык программирования называется предикатным, если логика любой конструкции Z этого языка может быть определена единственным предикатом LS(Z), истинным после исполнения Z. Функция LS называется логической семантикой языка.

12 Структура программы на языке CCP Программа набор определений предикатов Определение A K предикат A, оператор K параллельный оператор, оператор суперпозиции, условный оператор Вызов предиката (d 1, d 2, …, d n : e 1, e 2, …, e m )(3.1) φ имя предиката или переменной предикатного типа, n 0, m > 0, d 1, d 2, …, d n имена переменных аргументы вызова, e 1, e 2, …, e m результаты вызова Вычисление предиката Вызов φ(d: e), где d = d 1, d 2, …, d n, e = e 1, e 2, …, e m – наборы переменных n = 0 – вызов предикта соответствует константе Значение φ(d) φ(d: b), где b переменная логического типа Определение предиката A(x: y) K(x: y)(3.2) A имя предиката; набор x аргументы предиката, набор y результаты предиката, K(x: y) – оператор. Предикат – определяемый, базисный, значение переменной. Тип данных определяет набор базисных предикатов со значениями типа Система типов определяет совокупность всех базисных предикатов

13 Логическая семантика: LS(S k ) = L k LS( (d: e)) (d, e) LS(A(x: y) K(x: y)) A(x, y) LS(K(x: y)) Операционная семантика: метапрограмма Метаязык. Память – набор секций. Секция памяти – набор переменных и их значений: аргументы, результаты, локалы. s[a] – значение переменной с именем a в секции s s[x] – набор значений для набора имен x в секции s s[a] := v – оператор присваивания значения v переменной a в секции s s[x] := w – групповое присваивание набора значений w набору переменных x в секции s s = newSect(A) – создание в памяти новой секции s для определения предиката с именем A runCall(s, (d: e)) – исполнение вызова (d: e) runStat(s, K(x: y)) – исполнение оператора K(x: y) правой части

14 H(x: y) есть вызов предиката или оператор. RUN(H, x, y) существует исполнение H(x: y) для значений набора x, завершающееся значениями набора y. Свойство согласованности Cons(H) x y (LS(H(x: y)) y (RUN(H, x, y) & eq(y, y))) (3.11) eq(y, y) каждое значение набора y тождественно соответствующему значению из y Значение x примитивного типа тождественно x x = x Значение предикатного типа тождественно предикаты тождественны, т.е. истинна формула (d: e)(d: e) Значение x произведения или объединения тождественно x тождественны компоненты x и x

15 Вызов предиката Вызов A(z: u)(3.12) A(x: y) K(x: y) (3.13) q текущая секция Процедура runCall(q, A(z: u)) абстрактного процессора: s = newSect(A); (3.14) s[x] := q[z]; runStat(s, K(x: y)); q[u] := s[y]; Свойства: x = z & u = y(3.15) Лемма 3.2. Пусть имеется определение (3.13) для предиката A. Тогда Cons(K) Cons(A). Доказательство проводится для вызова A(z: u). Пусть истинно Cons(K). Докажем истинность Cons(A). Зафиксируем значения наборов z и u. Пусть истинно A(z: u).

16 Пусть истинно A(z: u). Тогда в соответствии с определением A(x: y) K(x: y) истинна формула K(z: u). Из этого следует, что существует исполнение K(z: u) для набора z, которое завершается получением набора u. При завершении исполнения тела (3.14) в соответствии с (3.15) справедливы равенства x = z и u = y. Поэтому существует исполнение K(x: y), завершающееся получением y. Тогда исполнение последовательности (3.14), а значит и исполнение A(z: u), завершается получением значений набора u, что доказывает первую часть свойства Cons(A). Пусть исполнение A(z: u) для набора z завершается получением набора u. Тогда завершается исполнение тела (3.14), в частности, исполнение K(x: y) завершается получением y. Поскольку в соответствии с (3.15) реализуется x = z и u = y, то исполнение K(z: u) завешается вычислением набора u. Из Cons(K) следует, что K(z: u) истинно. Тогда из определения A(x: y) K(x: y) следует истинность A(z: u), что доказывает вторую часть свойства Cons(A).

17 Оператор суперпозиции A(x: y) B(x: z); C(z: y)(3.16) LS(B(x: z); C(z: y)) z. (B(x, z) & C(z, y))(3.17) Процедура runStat(s, K(x: y)) абстрактного процессора: runCall(s, B(x: z)); (3.18) runCall(s, C(z: y)) z набор локальных переменных секции s Лемма 3.3 Cons(B) & Cons(C) Cons(H), где H обозначает B(x: z); C(z: y). Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения x и y. Пусть истинна H(x: y), т.е. истинна правая часть (3.17). Для некоторого z будут истинны B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует, что исполнение B(x: z) завершается получением набора z, а исполнение C(z: y) вычислением набора y. Поэтому исполнение операторов (3.18), а значит и H(x: y), завершается вычислением y. Это доказывает первую часть истинности Cons(H).

18 Допустим, исполнение H(x: y) завершается вычислением y. Докажем истинность H(x: y). Исполнение пары операторов (3.18) завершается вычислением y. В частности, завершается первый оператор runCall(s, B(x: z)). Тогда существует некоторый набор z, являющийся результатом исполнения. Таким образом, для некоторого z исполняются вызовы B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует истинность B(x: z) и C(z: y). Следовательно, истинна правая часть (3.18) и H(x: y).

19 Параллельный оператор A(x: y, z) B(x: y) || C(x: z)(3.19) x, y и z произвольные непересекающиеся наборы переменных, причем x может быть пустым. Если B или C есть имя переменной предикатного типа, то это имя входит в набор x. Логическая семантика параллельного оператора: LS(B(x: y) || C(x: z)) B(x, y) & C(x, z) Процедура runStat(s, K(x: y)) абстрактного процессора: runCall(s, B(x: y)) || runCall(s, C(x: z)) Лемма 3.4. Cons(B) & Cons(C) Cons(H), где H обозначает B(x: y) || C(x: z).

20 Условный оператор A(b, x: y) if (b) B(x: y) else C(x: y) (3.20) LS(if (b) B(x: y) else C(x: y)) (b B(x, y)) ( b C(x, y)) (3.21) Процедура runStat(s, K(x: y)) абстрактного процессора: if (s[b]) runCall(s, B(x: y)) else runCall(s, C(x: y)) (3.22) Лемма 3.5. Cons(B) & Cons(C) Cons(H), где H(b, x: y) обозначает if (b) B(x: y) else C(x: y). Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения b, x и y. Пусть истинна H(b, x: y). Тогда в соответствии с (3.21) истинны формулы b B(x, y) и b C(x, y). Рассмотрим случай, когда значение b истинно. Тогда истинна формула B(x, y). Из Cons(B) следует, что исполнение вызова B(x: y) завершается получением набора y. Поэтому исполнение оператора (3.22), а значит и H(b, x: y), завершается вычислением y. Это доказывает первую часть свойства Cons(H) для истинного значения b. Доказательство в случае ложного значения b проводится аналогично.

21 Допустим, исполнение H(b, x: y) завершается вычислением y, т.е. исполнение оператора (3.22) завершается вычислением y. Докажем истинность H(b, x: y). Пусть b истинно. Тогда исполнение вызова B(x: y) завершается получением набора y. Из Cons(B) следует истинность B(x: y). Тогда истинны формулы b B(x, y) и b C(x, y), поскольку b истинно. Следовательно, истинна правая часть (3.21) и H(b, x: y). Доказательство истинности H(b, x: y) в случае ложного значения b проводится аналогично.

22 Конструктор предиката Базисный предикат ConsPred(x, B: A), x набор переменных, B имя предиката, A имя переменной предикатного типа. B не ConsPred и не ConsArray LS(ConsPred(x, B: A)) y z. (LS(A(y: z)) LS(B(x, y: z))) (3.23) Процедура runCall(s, ConsPred(x, B: A)) абстрактного процессора: s[A] := newDef(s[x], B) (3.24) A x (y: z) =(x ~ : t); B(t, y: z) (3.25) x ~ = s[x] значение набора x, A x новое имя предиката Лемма 3.6. Cons(ConsPred). Доказательство. Зафиксируем значения x = x 0 и A = A 0. Пусть истинно ConsPred(x, B: A). Докажем, что исполнение ConsPred(x, B: A) завершается значением A = A x, тождественным A 0, т.е. A x A 0. Из истинности ConsPred(x, B: A) следует истинность правой части (3.23). Тогда истинна формула A 0 (y: z) B(x 0, y: z), однозначно определяющая предикат A 0. Рассмотрим исполнение вызова ConsPred(x, B: A), т.е. оператора (3.24). Получаем A = A x, где A x определяется формулой (3.25). Поскольку x ~ = s[x] = x 0, то: A x (y: z) =(x 0 : t); B(t, y: z) t = x 0 & B(t, y: z) B(x 0, y: z) (3.26) Таким образом, A = A x A 0, что доказывает первую половину леммы.

23 Допустим, исполнение ConsPred(x, B: A) завершается вычислением A = A 0 при x = x 0. Докажем истинность ConsPred(x, B: A), т.е. истинность правой части (3.23). Из (3.24) следует A = A x, и далее A 0 = A x. Из тождества (3.26) следует A 0 (y: z) B(x 0, y: z). Поскольку A = A 0 и x = x 0, получаем истинность правой части (3.23). Лемма 3.7. Пусть имеется вызов ConsPred(x, B: A), причем Cons(B) истинно. Тогда истинно Cons(A). Доказательство. Значением переменной A является A x с определением (3.25). Поскольку свойство Cons истинно для оператора =(x ~ : t), то по лемме 3.3 оно реализуется также для правой части (3.25). Далее, по лемме 3.2 истинно Cons(A x ), а значит и Cons(A).

24 Конструктор массива Базисный предикат ConsArray(x, B: A), x набор переменных, B имя предиката, A имя переменной предикатного типа. B не ConsPred и не ConsArray LS(ConsArray(x, B: A)) y z. (LS(A(y: z)) LS(B(x, y: z))) (3.27) Кодирование массива A(y: z) A ~ [y] = z (3.28) Процедура runCall(s, ConsArray(x, B: A)) абстрактного процессора: s[A] = newArray(Y, Z); // Y, Z - списки типов y, z (3.29) forAll y Y do runCall(s, B(x, y: s[A][y])) end S(y: z) F(y). Тогда forAll y Y do S(y: z) end y Y. F(y) (3.30) Лемма 3.8. Cons(A). Доказательство непосредственно следует из соотношения (3.28). Лемма 3.9. Допустим, предикат B(x, y: z) определяет однозначную всюду определенную функцию по x и y, т.е. истинно условие: x y Y !z B(x, y: z) (3.31) Тогда Cons(B) Cons(ConsArray)

25 Доказательство. Пусть истинно Cons(B). Зафиксируем x. В соответствии с (3.30) после исполнение оператора forAll из (3.29) будет истинной формула: y Y. B(x, y: A ~ [y]). Пусть z тот единственный набор, для которого истинно B(x, y: z) в соотношении (3.31). Тогда A ~ [y] = z. Из (3.28) следует истинность A(y: z). В итоге, после исполнения тела forAll будет истинно y Y. B(x, y: z) & A(y: z). Поскольку z единственно для B(x, y: z) и A(y: z), то будет истинным y Y. B(x, y: z) A(y: z). Дальнейшее доказательство очевидно. Допустим, в секции s исполняется вызов предиката A(u: v), где A является переменной предикатного типа, а значением A является массив. Секция s содержит переменную A и наборы u и v. Исполнение вызова A(u: v) реализуется следующим оператором: s[v] := s[A] [u] Для исполнения вызова A(u: v) принято обозначение runCall(s, A(u: v)).

26 Определение предиката. В правой части оператор суперпозиции, параллельный оператор или условный оператор. Первичные конструкции вызовы предикатов. Имя предиката: имя базисного предиката; имя предиката, имеющего определение в программе; аргумент предиката имя переменной предикатного типа; в правой части определения предиката встречается данный вызов; имя переменной предикатного типа, являющейся результатом вызова ConsPred или ConsArray, находящегося в правой части того же определения, что и данный вызов. Программа замкнутый набор определений предикатов вызываемые предикаты либо базисные, либо имеют определение в программе. Программа на языке CCP

27 Исполнение программы: исполнение вызова A(z: u) s = newSect(z, u); (3.32) input(s[z]); runCall(s, A(z: u)); output(s[u]) Предикаты в качестве параметров предикатов Генератор CONS(x, B: A) CONS есть ConsPred или ConsArray Ограничение 1: B не переменная предикатного типа. Пусть имеется CONS(y, C: B). Тогда CONS(y, C: B) G(y : B, F), где G(y : B, F) CONS(y, C: B) || CONS(y, H: F) H(y, x: A) CONS(y, x, C: A) Если B передается аргументом некоторого вызова, то необходимо дополнительным параметром передать F. Наконец, мы можем заменить генератор CONS(x, B: A) эквивалентным вызовом F(x: A).