Теорема: При въведените означения, Г е непрекъснато изображение на във .
Доказателство: първо ще покажем, че Г е монотонно изображение.
Нека , , , 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 (а, ) за всяко
a Nn, където е точно това най-малко решение наричаме денотационна семантика на програмата R с предаване по стойност.
Сега ще покажем, че денотационната и операционната семантика съвпадат за всяка програма R.
По-долу с ще означаваме най-малкото решение на системата
за Г1, Г2, …, Гk, което е и най-малко квазирешение на тази система.
Твърдение: Нека (F) е функционален терм, c е константа и R c.
Тогава () c.
Доказателство: провеждаме пълна индукция по дължината на извода
R c. Нека R c с дължина на извода k и твърдението е изпълнено за изводи R c с дължини по-малки от k.
Разглеждаме случаи в зависимост от вида на .
Нека е константа, = 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 и
R i (X1/c1, X2/c2, …, / , F) c с дължина на извода
по-малка от 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) DV (R).
Доказателство: нека ОV (R)(a) b. Тогава R 0 (X/a, F) b.
От предното твърдение получаваме 0 (X/a, F)() b. Прилагаме лемата за съгласуване на заместване и стойност и получаваме 0 (a, ) b
DV (R)(a) b. Така ОV (R) DV (R).
За всяко i { 1, 2, …, k } дефинираме функцията i : N по следния начин: i (a1, a2, …, ) b R i (X1/a1, X2/a2, …, / , F) 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 се разглежда абсолютно аналогично.
Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме () b съществуват
b1, b2, …, , такива че 1 () b1, 2 () b2, …, () bi и
i (b1, b2, …, ) b. От индукционното предположение
R j bj, j = 1, 2, …, ni. Освен това 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) OV (R).
Доказателство: нека 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 са области на Скот.
Твърдение: Нека A1 (A1, 1, 1), А2 (А2, 2, 2) са области на Скот.
Нека всяка монотонно растяща редица на А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 е непрекъснато изображение.
От горното твърдение и от разглежданията преди това получаваме, че
Fn = { f | f : Nn N и f - монотонно }, Pn = { f | f : Nn B и
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 е константно изображение.
Твърдение: Нека { k} е монотонно растяща редица от елементи на Fn.
Нека = . Тогава за всяко x Nn имаме:
-
(x) = за всяко k N имаме k (x) = ;
-
ако a , то (x) = a съществува k N, такова че k (x) = a.
Доказателство: за всяко 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) = .
Твърдение: Ако f е точна, то f е непрекъсната.
Доказателство: нека 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 N, f : Nn { tt, ff} или f : { tt, ff}n { tt, ff}.
Точно продължение на f наричаме функцията f* : Nn N
(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*.
Нека (X1, …, Xn, , , …, ) е терм.
Да означим 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, ):
-
Нека е константа, = c. Тогава (a, ) = c.
-
Нека е променлива, = Xi, i { 1, 2, …, n}. Тогава (a, ) = ai.
-
Нека е основна операция, = f (1, 2, …, l).
Тогава (a, ) = f* (1 (a, ), 2 (a, ), …, l (a, )), където f* е точното продължение на основната операция f.
-
Нека е условен терм, = if then 1 else 2. Тогава
(a, ) = 1 (a, ), ако (a, ) = tt;
(a, ) = 2 (a, ), ако (a, ) = ff;
(a, ) = , ако (а, ) = .
-
Нека e обръщение към функция, = (1, 2, …, ).
Тогава (a, ) = i (1 (a, ), 2 (a, ), …, (a, )).
При тази дефиниция, всеки терм има стойност принадлежаща
на N или B в зависимост от неговия тип.
Сподели с приятели: |