Лекции по семантика на езиците за програмиране
Изтегляне 3.6 Mb.
|
Теорема: При въведените означения, Г е непрекъснато изображение на във . Доказателство: първо ще покажем, че Г е монотонно изображение. Нека , , , a Nn, b N и Г ()(a) b. Тогава (a, ) b и от твърдението за монотонност получаваме (a, ) b, т.е. Г ()(a) b Г () Г (). Така Г е монотонно изображение. Нека 0 1 … n …е монотонно растяща редица от елементи на F. Тъй като Г е монотонно, достатъчно е да покажем, че Г ( ) = . За всяко a Nn, b N имаме Г ( )(а) b (a, ) b съществува n N, такова че (a, n) b съществува n N, такова че Г (n) (a) b ( )(а) b. Така Г ( ) = . Нека R е програма от вида 0 (X1, …, Xn, , , …, ), where (X1, …, ) = i (X1, …, , , , …, ), i = 1, 2, …, k. Нека Гi : F , Гi = , i = 1, 2, …, k. Разглеждаме системата за изображенията Г1, Г2, …, Гk: Г1 (1, 2, …, k) = 1 Г2 (1, 2, …, k) = 2 … Гk (1, 2, …, k) = k Тъй като Г1, Г2, …, Гk са непрекъснати изображения (предната теорема), то системата притежава най-малко решение = (1, 2, …, k). При това е и най-малко квазирешение. Функцията DV (R) : Nn N, дефинирана с DV (R)(а) 0 (а, ) за всяко
за Г1, Г2, …, Гk, което е и най-малко квазирешение на тази система. Твърдение: Нека (F) е функционален терм, c е константа и R c. Тогава () c. Доказателство: провеждаме пълна индукция по дължината на извода
Разглеждаме случаи в зависимост от вида на . Нека е константа, = d. Имаме R c. От лемата за извода получаваме d = c. Тогава () d = c. Нека е основна операция, = f (1, 2, …, l). Имаме R c с дължина на извода k. От лемата за извода съществуват константи c1, c2, …, cl, такива че R j cj, j = 1, 2, …, l с дължина на извода по-малка от k и f (c1, c2, …, cl) = c. От индукционното предположение имаме j () cj, j = 1, 2, …, l. Тогава () f (1 (), 2 (), …, l ()) f (c1, c2, …, cl) = c. Нека е условен терм, = if then 1 else 2. Имаме R c с дължина на извода k. От лемата за извода R tt и R 1 c или R ff и R 2 c, при това тези изводи са с дължина по-малка от k. Нека R tt и R 1 c. От индукционното предположение имаме () tt, 1 () c () c. Случаят R ff и R 2 c се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ). Имаме R c с дължина на извода k, така че от лемата за извода съществуват константи c1, c2, …, , такива че R j cj, j = 1, 2, …, ni с дължини на изводите по-малки от k и
по-малка от k. От индукционното предположение имаме j () cj, j = 1, 2, …, ni и i (X/c, F)() c. От лемата за съгласуване на заместване и стойност получаваме i (c, ) c. Имаме () i (1 (), 2 (), …, ()) i (c) Гi ()(c) i (c, ) c. Използвали сме, че е решение на системата за Г1, Г2, …, Гk.
Доказателство: нека ОV (R)(a) b. Тогава R 0 (X/a, F) b. От предното твърдение получаваме 0 (X/a, F)() b. Прилагаме лемата за съгласуване на заместване и стойност и получаваме 0 (a, ) b
Функцията i e добре дефинирана от еднозначността на опростяването по стойност. Това се вижда и от следното: i (a1, a2, …, ) b R i (X1/a1, X2/a2, …, / , F) b i (X/a, F)() b (горното твърдение) i (a, ) b (лемата за съгласуваност на заместване и стойност) Гi ()(a) b i (a) b ( е решение на системата за Г1, Г2, …, Гk). Така i i за всяко i = 1, 2, …, k. Лема: Нека (F) е функционален терм и () b. Тогава R b. Доказателство: индукция по построението на . Нека е константа, = d. Имаме () b d = b R b. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Имаме () b съществуват b1, b2, …, bl, такива че 1 () b1, 2 () b2, …, l () bl и f (b1, b2, …, bl) = b. От индукционното предположение R j bj, j = 1, 2, …, l. Освен това f (b1, b2, …, bl) = b R b. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Имаме () b. Тогава () tt и 1 () b или () ff и 2 () b. Нека () tt и 1 () b. От индукционното предположение получаваме R tt и R 1 b. Тогава R b. Случаят () ff и 2 () b се разглежда абсолютно аналогично.
b1, b2, …, , такива че 1 () b1, 2 () b2, …, () bi и i (b1, b2, …, ) b. От индукционното предположение
R i (X1/b1, X2/b2, …, / , F) b. От правилото за предаване по стойност получаваме R b. Следствие: е квазирешение на системата за Г1, Г2, …, Гk. Доказателство: нека Гi ()(a) b. Тогава i (a, ) b. От лемата за съгласуване на заместване и стойност получаваме i (X/a, F)() b и от предната лема R i (X/a, F) b. Съгласно дефиницията на i получаваме i (a) b. Така Гi () i, i = 1, 2, …, k е квазирешение на системата за Г1, Г2, …, Гk. Следствие: . Доказателство: тъй като е квазирешение на системата за Г1, Г2, …, Гk, а е най-малкото квазирешение на тази система, то .
Доказателство: нека DV (R)(а) b. Тогава 0 (a, ) b, и от твърдението за монотонност получаваме 0 (a, ) b. От лемата за съгласуване на заместване и стойност 0 (X/a, F)() b и от лемата по-горе получаваме R 0 (X/a, F) b, т.е. OV (R)(a) b. Така DV (R) OV (R). Kaто комбинираме теоремите за коректност и пълнота получаваме OV (R) = DV (R), с което показахме еквивалентността на операционната и денотационната семантика с предаване по стойност на рекурсивните програми. Рекурсивни програми. Денотационна семантика с предаване по име. Еквивалентност на операционната и денотационната семантика с предаване по име. Нека N е плоската област на Скот, базирана над множеството от естествените числа, т.е. N = (N { }, , ), N и наредбата е дефинирана с (x, y N) x y x = или x = y. Често ще използваме следните очевидни свойства: (x, y N) x y и y = x = , x y и x x = y. Ще покажем, че всяка монотонна редица в N има най-много два различни елемента. Действително, нека x0 x1 … xn …. Ако x0 = xn за всяко n N няма какво да доказваме. Нека x0 xm, m 1 и m е най-малкото такова. Тогава xm-1 xm и xm-1 xm xm-1 = . Имаме xm xm-1 = , xm xm+1 xm = xm+1. Индуктивно xm = xm+1 = xm+2 = …. Така редицата има два члена x0 = xm-1 = и xm . Означаваме Nk = N x N x …x N - декартовото произведение на k области на Скот N. Елементите на Nk ще означаваме с x, y, …, като размерността ще личи от контекста. Ще покажем, че всяка монотонна редица в Nk има най-много k+1 различни члена. Действително, нека x0 x1 … xn , xi = (xi1, xi2, …, xik). Да допуснем, например, че x0 x1 … xk+1. Тогава съществува s0, такова че , също = и = = …= . Аналогично, за j = 1, 2, …, k съществува sj, такова че , = и = = …= . Имаме, че s0, s1, …, sk са k+1 на брой и s0, s1, …, sk { 1, 2, …, k } съществуват i < j, такива че si = sj. Имаме = и , но si = sj - противоречие. С Fn ще означаваме множеството на всички непрекъснати изображения на Nn в N. Както знаем, Fn = (Fn, , ) е област на Скот, където (f, g Fn) f g f (x) g (x) за всяко x Nn, (x) = за всяко x Nn. Нека B е плоската област на Скот над множеството { tt, ff }. Формално релациите в B и N са различни, както и най-малките им елементи са различни, но ние ще ги означаваме по един и същ начин. Съвсем аналогично се вижда, че всяка монотонно растяща редица от елементи на B има най-много два различни елемента. Означаваме Bk = B x B x …x B - декартовото произведение на k области на Скот B. Аналогично на по-горе всяка монотонно растяща редица от елементи на Bk има най-много k+1 различни елемента. С Bn ще означаваме множеството на всички непрекъснати изображения на Bn в B. С Pn ще означаваме множеството на всички непрекъснати изображения на Nn в B. Естествено, Bn и Pn са области на Скот.
Нека всяка монотонно растяща редица на А1 има краен брой различни членове. Тогава всяко монотонно изображение f : A1 A2 е непрекъснато. Доказателство: нека f : A1 A2 е монотонно изображение и a0 1 a1 1 …1 аn 1 … е монотонно растяща редица от елементи на A1. По условие съществува m N, такова че am = am+1 = …. Очевидно е, че при това положение = am. Ще покажем, че f (am) е точна горна граница на редицата { f (an)}. Действително, an 1 am за всяко n N и f е монотонно f (an) 2 f (am) за всяко n N f (am) е горна граница на { f (an)}. Нека b е горна граница на { f (an)}. Тогава f (am) 2 b. Така f (am) = f ( ) е точна горна граница на { f (an)} и f е непрекъснато изображение.
f - монотонно }, Bn = { f | f : Bn B и f - монотонно }. Да напомним, че и трите множества Fn, Pn, Bn са области на Скот относно следната наредба: (, Fn (Pn, Bn)) (x) (x) за всяко x Nn (Bn).
Като пример, ако едно изображение f F1 е такова, че f () = , то f е монотонно. Ако f () и f е монотонно, то очевидно f (x) = f () за всяко x N, т.е. f е константно изображение.
Нека = . Тогава за всяко x Nn имаме:
Доказателство: за всяко x Nn имаме (x) = . Нека (x) = . Имаме k (x) (x) за всяко k N k (x) = (x) = за всяко k N. Нека k (x) = за всяко k N. Тогава е очевидно, че (x) = = . Нека (x) = a . Имаме, че (x) за всяко k N за всяко k N, k (x) = a или k (x) = . Ако допуснем, че k (x) = за всяко k N, то ще получим, че (x) = , което е противоречие. Така k (x) = а за някое k N. Нека k (x) = a за някое k N. Имаме (x) (x) = a. Нека f : Nn N (f : Nn B, f : Bn B). Казваме, че f е точна функция, ако за всеки x1, x2, …, xn Nn (Bn), { x1, x2, …, xn} f (x1, x2, …, xn) = .
Доказателство: нека x, y Nn (Bn) и x y. Ако x = y, то f (x) = f (y) f (x) f (y). Нека x y. Тогава съществува i { 1, 2, …, n}, такова че xi yi. От друга страна, xi yi xi = . Тъй като f е точна, то f (x) = f (x) f (y). Taка f е монотонна f е непрекъсната.
(f* : Nn B, f* : Bn B), дефинирана с: (x Nn (Bn)) f* (x1, x2, …, xn) = b, ако { x1, x2, …, xn} и f (x1, x2, …, xn) b; f* (x1, x2, …, xn) = , ако { x1, x2, …, xn} или ! f (x1, x2, …, xn). Очевидно е, че f* е точна функция, така че f* е непрекъсната. Лесно се вижда, че изображението, което съпоставя на всяка частична функция f нейното точно продължение f* е биекция между частичните функции и точните функции. При това, за всеки две частични функции f, g имаме f g f* g*.
Да означим F = x x …x . Нека a1, a2, …, an N, = (1, 2, …, k) F , i , i = 1, 2, …, k. Дефинираме индуктивно понятието стойност на терма в a1, …, an, 1, …, k, която записваме (a1, …, an, 1, …, k) или съкратено (a, ):
Тогава (a, ) = f* (1 (a, ), 2 (a, ), …, l (a, )), където f* е точното продължение на основната операция f.
(a, ) = 1 (a, ), ако (a, ) = tt; (a, ) = 2 (a, ), ако (a, ) = ff; (a, ) = , ако (а, ) = .
Тогава (a, ) = i (1 (a, ), 2 (a, ), …, (a, )). При тази дефиниция, всеки терм има стойност принадлежаща на N или B в зависимост от неговия тип. Каталог: uni uni -> Отчет за ибсф ра, ибсф ksf и ибсф 33 за средствата по набирателните сметки uni -> Условия и ред за приемане, отчитане и унищожаване на документи с фабрична номерация нормативна уредба uni -> "Икономиката е история на човешката трудова дейност." Маршал uni -> Програма за развитието на силите на мозъка. През 1978 г въз основа на разработените принципи той започва да обучава хора, а към 1980 г неговите лекции вече се ползват с колосален успех в цял свят Изтегляне 3.6 Mb. Сподели с приятели:
|