Лекции по семантика на езиците за програмиране
Писани са от мен, Иван Димитров Георгиев (вече завършил) студент по информатика, електронната ми поща е ivandg@yahoo.com.
Четени през летния семестър на учебната 2003/2004 година. Лектор тогава беше професор Иван Сосков. Използвал съм само мои записки от лекции, както и учебника Теория на програмите на Сосков и Дичев. Изрично отбелязвам, че темата схеми на програми не е довършена – само са дадени дефинициите на синтаксиса и семантиката на итеративните и рекурсивните схеми. Трябва да се включат още превода на итеративни схеми в рекурсивни (чрез опашкови функции) и евентуално примера на Патерсън и Хюит (който обикновено не се предава, тъй като времето не достига).
Добре е да имате инсталиран MathType, за да нямате проблеми при разчитането. От този линк http://www.dessci.com/en/dl/MTW6.exe може да изтеглете trial версия за един месец.
Въведение
С N ще означаваме множеството на естествените числа,
N = { 0, 1, 2, … }. С Nk, k > 0, ще означаваме k-тата декартова
степен на N, N1 = N. С Nw означаваме множеството от всички безкрайни редици от естествени числа. За краткост наредената k-торка x1, x2, …, xk или безкрайната редица x1, x2, … ще означаваме с x, като размерът ще се разбира от контекста.
В курса често ще разискваме функции, които са дефинирани в Nk, k > 0 и приемат стойности в N – наричаме ги функции на k аргумента. Задаваме ги чрез техните графики, които представляват (k+1)-местни релации над N, т.е. подмножества на Nk+1. Нека G Nk+1.
Тогава G задава функция на k аргумента, ако е изпълнено следното условие: ако (x, y) G и (x, y) G, то y = y.
Ако допълнително е изпълнено: за всяко x Nk съществува y N, такова че (x, y) G, казваме че G задава тотална функция. Ако това условие не е изпълнено, казваме че функцията е частична. Нека G задава функция f на k аргумента. Записваме G = Gf.
Ще записваме f (x) y, ако (x, y) Gf.
Дефинираме Dom (f) = { x Nk | съществува y N, така че (x, y) Gf }.
Дефинираме Ran (f) = { y N | съществува x Nk, така че (x, y) Gf }.
Ще означаваме !f (x), ако x Dom (f), т.е. съществува y N,
такова че f (x) y. Ако x Dom (f) ще означаваме !f (x).
За да подчертаем, че f е частична функция на k аргумента
записваме f : Nk N.
С ! означаваме функцията, която не е дефинирана никъде.
Нека f и g са функции (на различен, възможно безкраен брой аргументи).
Означаваме f (x1) g (x2), ако за всяко y N, f (x1) y g (x2) y.
Лесно се вижда, че това означава следното:
x1 Dom (f), x2 Dom (g) и f (x1) = g (x2) или x1 Dom (f), x2 Dom (g).
Често ще използваме следното означение за функция, което идва от
-смятането на Чърч. Ако f : Nk N е частична функция
записваме f = x.f (x).
Пространството Fn. Теорема на Кнастер-Тарски. Правило на Скот.
С Fn, n > 0 означаваме множеството на всички частични функции на
n аргумента. В множеството Fn въвеждаме частична наредба:
(f, g Fn) f g Gf Gg за всяко x Nn, y N имаме
f (x) y g (x) y. Ако f g, казваме че f е подфункция на g или, че g е продължение на f. Въведената наредба не е линейна – всеки две различни тотални функции са несравними. Наредбата притежава единствен минимален елемент – функцията !, която се продължава до всяка функция. Също така, наредбата притежава безброй много (дори неизброимо много) максимални елементи – това са всички тотални функции, които не могат да бъдат продължавани.
Нека X Fn . Казваме, че g Fn е горна граница на X,
ако за всяка f X имаме, че f g. Казваме, че g Fn е точна горна граница на X, ако за всяка горна граница g на X имаме, че g g.
Естествено, ако X притежава точна горна граница, то тя е единствена.
Нека { fk} е редица от функции, fk Fn. Казваме, че редицата е монотонно растяща, ако fk fk+1 за всяко k N.
Твърдение: Нека { fk} е монотонно растяща редица от
функции, fk Fn. Дефинираме функцията g по следния начин:
(x Nn, y N) g (x) y съществува k N, такова че fk (x) y.
Тогава g е добре дефинирана n-местна функция, която е точна горна граница на { fk }.
Доказателство: нека x Nn, y1, y2 N и g (x) y1, g (x) y2. Тогава съществуват k1, k2 N, такива че (x) y1 и (x) y2.
Нека за определеност k1 k2. Тогава y1 = y2.
Получихме, че g е добре определена функция.
Нека k N и fk (x) y, x Nn, y N. Тогава по определение g (x) y
fk g за всяко k N g е горна граница на { fk}.
Нека h Fn е произволна горна граница на { fk}.
Нека x Nn, y N и g (x) y. Тогава съществува k N, такова че
fk (x) y, но fk h h (x) y. Така g h. Твърдението е доказано.
Графиката на функцията g от твърдението получихме като обединение на графиките на функциите f0, f1, …, fk, …. Това ни дава основание да означаваме g = .
Нека е частична функция. Казваме, че е крайна функция, ако
Dom () е крайно множество G е крайно множество. Обикновено крайните функции ще означаваме с .
Твърдение: Нека е крайна n-местна функция. Нека { fk} е монотонно растяща редица. Нека .
Тогава съществува m N, такова че fm.
Доказателство: ако Dom () = , твърдението е очевидно.
Нека Dom () = { x0, x1, …, xr }, xi Nn. Нека (xi) yi, i = 0, 1, …, r.
Да означим g = . Имаме, че g g (xi) yi, i = 0, 1, …, r
за всяко i { 0, 1, …, r } съществува ki N, такова че (xi) yi.
Нека m = max (k0, k1, …, kr). Тогава fm, i = 1, 2, …, r fm (xi) yi за всяко i = 0, 1, …, r fm.
Ще казваме, че Г e оператор, ако Г e тотално изображение на във . Означаваме Г : .
Нека Г : Fn Fm е оператор. Ще казваме, че Г е компактен оператор, ако за всяка функция f Fn, x Nm, y N имаме, че
Г (f) (x) y съществува крайна f, такава че Г () (x) y.
Интуитивно, за да изчислим Г (f) (x) за дадено x използваме само краен брой стойности на f.
Ще дадем пример за некомпактен оператор.
Нека Г : F1 F1 е дефиниран с
Г (f) (x) 0 за всяко x N, ако f е тотална;
Г (f) (x) 1 за всяко x N, ако f не е тотална.
Ако f е тотална функция, то Г (f) (x) 0 за всяко x N, но за всяка крайна f имаме, че Г (f) (x) 1 за всяко x N, тъй като крайните функции не са тотални.
Твърдение: Нека Г1 : Fn Fm, Г2 : Fn Fm са два компактни оператора и за всяка крайна Fn имаме, че Г1 () = Г2 ().
Тогава Г1 (f) = Г2 (f) за всяка f Fn .
Доказателство: нека f Fn , x Nm, y N. Тогава Г1 (f) (x) y съществува крайна f, такава че Г1 () (x) y
съществува крайна f, такава че Г2 () (x) y, тъй като Г1 () = Г2 () Г2 (f) (x) y. Така Г1 (f) = Г2 (f).
Казваме, че Г : Fn Fm е монотонен оператор,
ако за всеки f, g Fn имаме f g Г (f) Г (g).
Твърдение: Всеки компактен оператор е монотонен.
Доказателство: нека Г : Fn Fm е компактен оператор.
Нека f, g Fn и f g. Нека x Nm, y N и Г (f) (x) y. Тогава съществува
крайна f, такава че Г () (x) y, но f g g, е крайна и
Г () (x) y Г (g) (x) y. Така Г (f) Г (g) Г e монотонен оператор.
Казваме, че Г : Fn Fm е непрекъснат оператор,
ако за всяка монотонно растяща редица { fk}, fk Fn имаме,
че Г ( ) е точна горна граница на { }.
Твърдение: Всеки непрекъснат оператор е монотонен.
Доказателство: нека Г : Fn Fm е непрекъснат оператор.
Нека f, g Fn и f g. Разглеждаме редицата f, g, g, …, g, ….
Очевидно тази редица е монотонна и нейната точна горна граница е g.
Тогава Г (g) е точна горна граница на { Г (f), Г (g) } Г (f) Г (g).
Така, ако Г е непрекъснат оператор, то за всяка монотонно растяща редица { fk} имаме, че { Г (fk)} също е монотонно растяща и
Г ( ) = .
Твърдение: Всеки компактен оператор е непрекъснат.
Доказателство: нека Г : Fn Fm е компактен оператор. Нека { fk } е монотонно растяща редица. Полагаме g = . Трябва да покажем,
че Г (g) е точна горна граница на { Г (fk)}. Тъй като g е горна граница на
{ fk}, то за всяко k N имаме, че fk g. От по-предното твърдение имаме, че Г е монотонен оператор Г (fk) Г (g) за всяко k N
Г (g) е горна граница на { Г (fk)}. Нека h е горна граница на { Г (fk)}.
Ще покажем, че Г (g) h. Нека x Nm, y N и Г (g) (x) y.
Тогава съществува крайна g, такава че Г () (x) y.
Имаме, че g = съществува m N, такова че fm
Г (fm) (x) y h (x) y. Така Г (g) h и Г (g) e точна горна
граница на { Г (fk)}.
Твърдение: Всеки непрекъснат оператор е компактен.
Доказателство: нека Г : Fn Fm е непрекъснат оператор.
Нека f Fn. Нека k е ограничението на функцията f върху
[0, k] x [0, k] x … x [0, k]. Ясно е, че { k} е монотонно растяща от крайни функции и = f. Тъй като Г е непрекъснат оператор, то
от по-горе получаваме, че Г (f) = .
Нека x Nm, y N и Г (f) (x) y. Тогава съществува k N,
такова че Г (k)(x) y и k е крайна функция.
Обратно, нека f е крайна функция и Г ()(x) y.
Тогава Г (f) (x) y, тъй като Г e монотонен оператор.
Така Г е компактен оператор.
Нека Г : Fn Fn е оператор.
Казваме, че f Fn е неподвижна точка за Г, ако Г (f) = f.
Казваме, че f Fn е квазинеподвижна точка за Г, ако Г (f) f.
Oчевидно всяка неподвижна точка за Г е и квазинеподвижна за Г.
Казваме, че f Fn е най-малка неподвижна точка за Г,
ако f е неподвижна точка за Г и за всяка неподвижна точка
g на Г имаме, че f g. Ясно е, че ако един оператор притежава
най-малка неподвижна точка, то тя е единствена.
Аналогично се дефинира най-малка квазинеподвижна точка за Г.
Естествено, ако Г притежава най-малка квазинеподвижна точка, то тя е единствена. Освен това, ако f е най-малка квазинеподвижна точка за Г и g e най-малка неподвижна точка за Г, то f g, тъй като g е квазинеподвижна за Г. Обратното в общия случай не е изпълнено.
Вярно е, обаче, следното
Твърдение: Нека Г : Fn Fn е монотонен оператор. Нека f Fn е
най-малка квазинеподвижна точка за Г. Тогава f е най-малка неподвижна точка за Г.
Доказателство: имаме, че Г (f) f (Г – монотонен) Г (Г (f)) Г (f)
Г (f) е квазинеподвижна точка за Г f Г (f). Така f е неподвижна точка за Г. Нека g Fn е неподвижна точка за Г. Toгава g е квазинеподвижна точка за Г f g, тъй като f е най-малка квазинеподвижна точка за Г. Така f е най-малка неподвижна точка за Г.
Теорема (Кнастер-Тарски): Нека Г : Fn Fn е компактен оператор. Тогава Г притежава най-малка квазинеподвижна точка.
Доказателство: с индукция по k дефинираме редицата от функции { fk}.
База: f0 = !.
Предположение: нека fk е дефинирана, k 0.
Стъпка: тогава fk+1 = Г (fk).
С индукция по k ще покажем, че редицата { fk} е монотонно растяща.
База: очевидно f0 f1, тъй като f0 = !.
Предположение: нека fk fk+1, k 0.
Стъпка: тъй като Г e компактен, то Г е монотонен Г (fk) Г (fk+1), т.е.
fk+1 fk+2.
Да означим f = .
Ще покажем, че f е най-малка квазинеподвижна точка за Г.
Имаме Г (f) = Г ( ) = = = f. Използвали сме,
че Г е непрекъснат оператор, тъй като Г е компактен.
Така f е квазинеподвижна точка за Г.
Нека g Fn e произволна квазинеподвижна точка за Г.
Ще покажем, че f g. За целта с индукция по k ще покажем, че fk g.
База: f0 g, тъй като f0 = !.
Предположение: нека fk g, k 0.
Стъпка: тъй като Г e компактен оператор, то Г е монотонен
Г (fk) Г (g) g, тъй като g е квазинеподвижна точка.
Получихме, че g е горна граница на { fk}, но f е точната горна граница
на { fk} f g. Теоремата е доказана.
Тъй като всеки компактен оператор е монотонен, то от твърдението
по-горе получаваме, че всеки компактен оператор притежава най-малка неподвижна точка (която е и най-малка квазинеподвижна точка). Доказателството на теоремата на Кнастер-Тарски е конструктивно и дава метод за нейното намиране.
Правило на Скот
Нека Г : Fn Fn e компактен оператор и f Fn е най-малката неподвижна точка на Г, f = , f0 = !, fk+1 = Г (fk).
Нека P е някакво свойство на функциите от Fn, т.е. P : Fn { true, false }.
Да предположим, че сме доказали P (!) и за всяка g Fn, P (g) P (Г (g)). С индукция по k ще покажем, че P (fk) за всяко k N.
База: при k = 0, f0 = ! и P (f0) вече е доказано.
Предположение: нека е доказано P (fk).
Стъпка: имаме P (fk) P (Г (fk)), P (fk) е вярно P (Г (fk)), т.е. P (fk+1).
Въпросът е дали оттук следва верността на P (f), т.е. P ( ).
С пример ще покажем, че това не е така. Разглеждаме операторът
Г : F1 F1, дефиниран с
Г (f)(x) if x = 0 then 1 else x * f (x-1) за всеки f F1, x N.
Тривиално се проверява, че Г e компактен оператор.
С индукция по k ще покажем, че fk = x. if x < k then x! else !.
База: при k = 0, f0 = ! = x. if x < 0 then x! else !.
Предположение: нека fk = x. if x < k then x! else !, k 0.
Стъпка: имаме fk+1 = Г (fk). Да означим g = x. if x < k+1 then x! else !.
Ако x = 0, то fk+1 (0) 1 и g (0) 0! = 1, тъй като 0 < k+1.
Така fk+1 (0) g (0).
Ако 0 < x < k+1, то fk+1 (x) x * fk (x-1) и x-1 < k fk (x-1) (x-1)!
fk+1 (x) x! и g (x) x!, тъй като x < k+1. Така fk (x) g (x) за всяко x < k+1.
Ако x k+1, то fk+1 (x) x * fk (x-1) и x-1 k ! fk (x-1) ! fk+1 (x) и
! g (x), тъй като x k+1. Така fk (x) g (x) за всяко x k+1.
Окончателно fk+1 (x) g (x) за всяко x N.
Оттук веднага получаваме, че f = = x. x! е най-малката неподвижна точка на Г.
Да дефинираме свойството P по следния начин:
P (g) съществува x N, такова че ! g (x).
Очевидно е, че P (!). Ще покажем, че за всяка g F1, P (g) P (Г (g)).
Нека P (g). Тогава съществува x N, такова че ! g (x). Имаме x+1 > 0 и
Г (g)(x+1) (x+1) * g (x) ! Г (g)(x+1). Така P (Г (g)).
Въпреки това, не е вярно, че P (x. x!), тъй като x. x! е тотална функция.
Този пример показва, че трябва да наложим някакво ограничение на свойството P.
Казваме, че P : Fn { true, false } е непрекъснато, ако за всяка монотонно растяща редица от функции { fk}, fk Fn,
P (fk) за всяко k N P ( ).
Теорема (правило на Скот): Нека P е непрекъснато свойство, Г e компактен оператор. Нека P (!) и за всякa g Fn, P (g) P (Г (g)).
Toгава P (f), където f е най-малката неподвижна точка на Г.
Доказателство: имаме f = , f0 = !, fk+1 = Г (fk) за всяко k N.
Вече показахме, че в такъв случай P (fk) за всяко k N, също { fk} е монотонна редица и P е непрекъснато свойство. Така P ( ), т.е. P (f).
Ще дадем някои примери за непрекъснати свойства.
Свойство P от вида: P (f) за всяко x Nn, (! f (x) и I (x)) O (x, f (x)), където I (x) и O (x, y) са произволни предикати над ествените числа се нарича условие за частична коректност. Идеята е, че предикатът I е условие за входните данни, а предикатът O е условие за
изходните данни. Ясно е, че P (!) е вярно при всеки избор на предикатите I, O.
Свойство P от вида: P (f) за всяко x Nn, I (x) (! f (x) и O (x, f (x))), където I, O имат същия смисъл се нарича условие за тотална коректност. Ясно е, че P (!) е вярно I (x) false при всеки избор на O.
При фиксирани I, O условието за тотална коректност влече условието за частична коректност, тъй като то предполага резултат от изчислението на функцията.
Теорема: Всяко условие за частична коректност е непрекъснато.
Доказателство: нека P (f) за всяко x Nn, (! f (x) и I (x)) O (x, f (x)).
Нека { fk} е монотонно растяща редица от функции и P (fk) за всяко k N.
Нека f = . Нека I (x) и ! f (x), f (x) y. Тогава съществува k N, такова че fk (x) y, т.е. I (x) и ! fk (x) O (x, fk (x)), т.е. О (x, y)
O (x, f (x)). Така доказахме P (f).
По аналогичен начин се показва, че всяко условие за тотална коректност е непрекъснато. Пропускаме доказателството, тъй като правилото на Скот не е приложимо за такива условия – ако P е условие за тотална коректност, то P (!) не е вярно (освен в тривиалния случай, когато няма входни данни, т.е. I false).
Нека отново разгледаме компактният оператор Г : F1 F1,
Г (f)(x) if x = 0 then 1 else x * f (x-1) за всеки f F1, x N.
Ще покажем, че за всяко x N, ! f (x) f (x) = x!, където f е най-малката неподвижната точка на Г. За целта дефинираме свойство P,
P (g) за всяко x N, ! g (x) g (x) = x!. Това е условие за частична коректност: I true, O (x, y) y = x!. Така правилото на Скот е приложимо.
Имаме P (!), тъй като P е условие за частична коректност.
Нека P (g), т.е. за всяко x N, ! g (x) g (x) = x!.
Нека ! Г (g) (x). Ако x = 0, то Г (g)(0) = 1 = 0!. Нека x 0. Тогава
Г (g)(x) x * g (x-1), ! Г (g)(x) ! g (x-1) g (x-1) = (x-1)!
Г (g)(x) = x * (x-1)! = x!. Така P (Г (g)).
Така получихме, че най-малката неподвижна точка на Г се продължава от x. x!. С тривиална индукция по x се показва, че всяка неподвижна точка на Г e тотална функция. Така още веднъж получихме, че
най-малката неподвижна точка на Г e x. x!.
Лема: Нека { fk} е монотонно растяща редица, f = .
Нека { gk} е монотонно растяща редица, g = .
Нека fk gk за всяко k N. Тогава f g.
Доказателство: имаме fk gk за всяко k N, така че
е горна граница на редицата { fk} тя продължава точната горна граница на { fk}, т.е. f = = g.
Твърдение: Нека Г1 : Fm Fn и Г2 : Fm Fn са компактни оператори.
Toгава свойството P, дефинирано с P (g) Г1 (g) Г2 (g) е непрекъснато.
Доказателство: нека { fk} е монотонно растяща редица и
P (fk) за всяко k N, т.е. Г1 (fk) Г2 (fk) за всяко k N.
От лемата . Нека f = .
Тогава Г1 (f) = Г1 ( ) = = Г2 ( ) = Г2 (f).
Използвали сме, че Г1 и Г2 са непрекъснати оператори. Така P (f).
Като пример свойството P, дефинирано с P (g) g x. g (g (x)) е непрекъснато, тъй като Г1 (g) = g и Г2 (g)(x) g (g (x)) са компактни оператори.
Твърдение: Нека P1 и P2 са непрекъснати свойства.
Тогава свойството P (g), дефинирано с P (g) P1 (g) и P2 (g) е непрекъснато.
Доказателство: нека { fk} е монотонно растяща редица от функции и
P (fk) за всяко k N. Тогава P1 (fk) за всяко k N и
P2 (fk) за всяко k N. Нека f = . От непрекъснатостта на P1 и P2 получаваме P1 (f) и P2 (f). С това показахме P (f).
Следствие: Нека Г1 : Fm Fn и Г2 : Fm Fn са компактни оператори.
Toгава свойството P, дефинирано с P (g) Г1 (g) = Г2 (g) е непрекъснато.
Доказателство: Г1 (g) = Г2 (g) Г1 (g) Г2 (g) и Г2 (g) Г1 (g). Прилагаме
предните две твърдения.
Твърдение: Нека P1 и P2 са непрекъснати свойства. Тогава свойството
P (g), дефинирано с P (g) P1 (g) или P2 (g) е непрекъснато.
Доказателство: нека { fk} е монотонно растяща редица и P (fk)
за всяко k N, т.е. P1 (fk) или P2 (fk) за всяко k N.
Нека N1 = { k|P1 (fk) } и N2 = { k|P2 (fk) }. Имаме N1 N2 = N, така че поне едно от N1, N2 е безкрайно. Нека, например, N1 е безкрайно.
Нека h е биективна функция, такава че h : N N1 и за всеки x, y N
x y h (x) h (y). С други думи N1 = { h (0), h (1), …, h (n), …} и
h (0) < h (1) < …< h (n) < …. Ясно е, че { } е монотонна редица.
Твърдим, че = . Имаме , тъй като
за всяко k N, h (k) k fk и можем да приложим лемата.
Също, ако (x) y, то (x) y (x) y, тъй като e член на редицата { fk}. Така . Тъй като P1 е непрекъснато и P1 ( ) за всяко k N, то P1 ( ) P1 ( ) P1 ( ) или P2 ( ).
С това показахме P ( ).
Ще проверим, че отрицание на непрекъснато свойство не винаги е непрекъснато.
Нека P : F1 { true, false} е свойството, дефинирано с P (f) f е тотална. Тогава P е непрекъснато. Действително, ако { fk} е монотонно растяща редица от тотални функции, то всички функции в редицата съвпадат с точната горна граница на редицата, така че и тя е тотална.
От друга страна, отрицанието на P не е непрекъснато. Действително, нека f е произволна тотална функция. Нека k е ограничението на f върху [0, k], k N. Ясно е, че { k} е монотонна редица и = f.
Oчевидно k не е тотална за всяко k N, но f е тотална функция.
Ще илюстрираме правилото на Скот в още някои примери.
Нека П : N { true, false } е тотален предикат, h F1 е тотална функция.
Дефинираме оператор Г по следния начин:
Г (g)(x) if П (x) then x else g (g (h (x))). Тривиално се проверява, че Г e компактен оператор. Нека f е най-малката неподвижна точка на Г.
Ще покажем, че за всяко x N имаме f (x) f (f (x)). За целта дефинираме свойство P по следния начин: P (g) за всяко x N, g (x) f (g (x)).
Преди всичко, свойството P е непрекъснато, тъй като Г1 (g) = g и
Г2 (g)(x) f (g (x)) са компактни оператори. Очевидно, P (!).
Нека P (g), т.е. g (x) f (g (x)). За всяко x N имаме
f (Г (g)(x)) f (if П (x) then x else g (g (h (x))))
if П (x) then f (x) else f (g (g (h (x)))).
Имаме f (x) if П (x) then x else f (f (h (x))) за всяко x N,
П (x) f (x) = x. Също, f (g (g (h (x)))) g (g (h (x))).
Така f (Г (g)(x)) if П (x) then x else g (g (h (x))) Г (g)(x).
С това показахме P (Г (g)). Остава да приложим правилото на Скот.
Нека П : N { true, false } е тотален предикат, h, k F1 са тотални функции. Дефинираме оператор Г по следния начин:
Г (g)(x, y) if П (x) then y else h (g (k (x), y)). Тривиално се проверява, че Г e компактен оператор. Нека f е най-малката неподвижна точка на Г.
Ще покажем, че за всеки x, y N имаме h (f (x, y)) f (x, h (y)).
За целта дефинираме свойство P по следния начин:
P (g) за всеки x, y N, h (g (x, y)) g (x, h (y)). Ясно е, че P е непрекъснато свойство, тъй като Г1 (g)(x, y) h (g (x, y)) и
Г2 (g)(x, y) g (x, h (y)) са компактни оператори. Очевидно, P (!).
Нека P (g), т.е. за всеки x, y N, h (g (x, y)) g (x, h (y)).
За всеки x, y N имаме Г (g)(x, h (y)) if П (x) then h (y) else
h (g (k (x), h (y))) h (if П (x) then y else g (k (x), h (y)))
h (if П (x) then y else h (g (k (x), y))) h (Г (g)(x, y)).
С това показахме P (Г (g)). Остава да приложим правилото на Скот.
Области на Скот. Непрекъснати изображения. Теорема на Кнастер-Тарски.
Нека A e произволно множество, в което е въведена частична наредба .
Нека съществува A, който е най-малък относно , т.е.
a за всяко a A. Нека, освен това, всяка монотонно растяща редица
а0 а1 … an …има точна горна граница в A, т.е. съществува a A, такова че an a за всяко n N и за всяко b A, такова че an b за всяко n N имаме, че a b. Естествено, точната горна граница a А е единствена, означаваме a = . При тези предположения, наредената тройка (A, , ) наричаме област на Скот. Множеството А наричаме носител на областта на Скот. От самата дефиниция следва, че А е непразно ( A). Обикновено ще означаваме областта на Скот по същия начин, както носителя: А = (A, , ).
Ще дадем някои примери за области на Скот.
Тройката Fn = (Fn, , !) е област на Скот, както показахме по-горе.
По-общо, ако B е произволно множество и FnB е множеството на
n-местните частични функции на B, т.е. FnB = { f | f : Bn B },
то FnB = (FnB, , !) е област на Скот. Естествено, Fn = FnN.
Нека B е произволно множество. Тогава P (B) = (P (B), , ) е област на Скот. Тук е обичайното включване на множества, е празното множество, което се включва във всяко подмножество на B.
Всяка монотонна редица B0 B1 … Bn …има точна горна граница – обединението на множествата в редицата.
Нека A0 е произволно множество, A0, A = A0 { }. Въвеждаме частична наредба в A: за всеки x, y A, x y x = или x = y.
Ще проверим, че действително е частична наредба.
Имаме x x за всяко x A, тъй като x = x.
Нека x, y A, x y и y x. Нека x . Toгава от x y получаваме x = y.
Нека x = . Имаме y x, т.е. y = = x или y = x.
Така x y и y x x = y.
Нека x, y, z A, x y и y z. Ако x = , то x z. Нека x . Tъй като
x y, то x = y. От друга страна y z, така че x z.
Така x y и y z x z.
Ясно е, че x за всяко x A, т.е. e най-малкият елемент на A.
Нека x0 x1 … xn … е монотонно растяща редица.
Нека за всяко n N имаме xn = . Тогава e точна горна граница на редицата { xn}.
Нека съществува n N, такова че xn . Тогава xn = xn+1. Оттук xn+1 , така че xn+1 = xn+2. По индукция xn = xn+1 = …= xn+k = …. Тогава xn е точна граница на редицата { xn}.
И така доказахме, че A = (A, , ) е област на Скот. Тя се нарича плоска област на Скот.
Ще дадем един отрицателен пример за област на Скот.
Тройката (N, , 0), където е стандартната наредба в N не е област на Скот, тъй като редицата 0 1 2 …е монотонно растяща редица, която няма точна горна граница.
Сега ще покажем една лема, която ще използваме по-долу.
Лема: Нека A = (A, , ) е област на Скот и { an}, { bn} са монотонни
редици в A. Нека an bn за всяко n N. Тогава .
Доказателство: за всяко k N е изпълнено ak bk , тъй като
е горна граница на { bk}. Така е горна граница на { ak}
, тъй като e точна горна граница на { ak}.
Конструкции на области на Скот
Нека A1 = (A1, 1, 1), A2 = (A2, 2, 2), …, An = (An, n, n), n 2 са области на Скот. Означаваме A = A1 x A2 x … x An – декартовото произведение на множествата A1, A2, …, An.
В A въвеждаме релация : за всеки ai Ai, bi Ai, i = 1, 2, …, n,
(a1, a2, …, an) (b1, b2, …, bn) a1 1 b1 и a2 2 b2 и …и an n bn.
Очевидно е, че е частична наредба в А, тъй като 1, 2, …, n са частични наредби в A1, A2, …, An съответно. При това = (1, 2, …, n) е най-малък елемент в A относно .
Твърдение: Нека { (ak1, ak2, …, akn) } е монотонно растяща редица от елементи на A. Нека ai Ai е точната горна граница на { aki},
i = 1, 2, …, n. Тогава (a1, a2, …, an) A е точна горна граница на
редицата { (ak1, ak2, …, akn) }.
Доказателство: преди всичко, за всяко i { 1, 2, …, n } редицата { aki} е монотонно растяща редица в Ai относно i, така че елементът ai е добре дефиниран. За всяко k N имаме ak1 1 a1, ak2 2 a2, …, akn n an, така че
(ak1, ak2, …, akn) (a1, a2, …, an) за всяко k N, т.е. (a1, a2, …, an) е горна граница на { (ak1, ak2, …, akn) }. Нека (ak1, ak2, …, akn) (b1, b2, …, bn) за всяко k N. Тогава за всяко i { 1, 2, …, n}, aki i bi за всяко k N, така че bi е горна граница на { aki} ai i bi. Така (a1, a2, …, an) (b1, b2, …, bn), т.е. (a1, a2, …, an) е точна горна граница на { (ak1, ak2, …, akn) }.
И така показахме, че A = (A, , ) е област на Скот, където
A = A1 x A2 x … x An, е дефинираната частична наредба,
= (1, 2, …, n). Тази област на Скот наричаме декартово произведение на областите на Скот A1, A2, …, An.
Нека A1 = (A1, 1, 1), A2 = (A2, 2, 2) са области на Скот.
Казваме, че изображението f : A1 A2 е непрекъснато, ако за всяка монотонно растяща редица a0 1 a1 1 …1 an 1 …от елементи на A1 имаме, че f ( ) е точна горна граница на редицата { f (an)} в A2.
Изрично отбелязваме, че непрекъснатите изображения са тотални, т.е. дефинирани за всеки елемент на A1.
Естествено, един оператор Г : Fn Fm е непрекъснато изображение на области на Скот Г e непрекъснат оператор (в смисъл на дефиницията от по-горе).
Казваме, че изображението f : A1 A2 е монотонно, ако
за всеки a, b A1 имаме a 1 b f (a) 2 f (b).
Твърдение: Всяко непрекъснато изображение f : A1 A2 е монотонно.
Доказателство: нека a, b A1 и a 1 b. Разглеждаме редицата
a, b, b, …, b, …от елементи на A1. Естествено, тя е монотонна и очевидно има точна горна граница b. Тъй като f е непрекъснато изображение, то
f (b) е точна граница на { f (a), f (b)} f (a) 2 f (b).
Така, ако f : A1 A2 е непрекъснато изображение и
a0 1 a1 1 …1 an 1 …е монотонно растяща редица в A1, то
f (a0) 2 f (a1) 2 …2 f (an) 2 …е монотонно растяща редица в A2 и
f ( ) = .
Означаваме с (A1 A2) множеството на всички непрекъснати изображения f : A1 A2. Ще покажем, че ако f е константно изображение, т.е. f (a) = b A2 за всяко a A1, то f е непрекъснато.
Действително, за произволна монотонна редица a0 1 a1 1 …от елементи на A1 имаме, че f ( ) = b и редицата { f (an)} има единствен елемент b, така че тя има точна горна граница b = f ( ).
В частност, изображението : A1 A2, дефинирано с (а) = 2 за всяко
a A1 е непрекъснато.
В множеството (A1 A2) въвеждаме релация : за всеки f, g (A1 A2),
f g f (a) 2 g (a) за всяко a A1. Ясно е, че е частична наредба в
(A1 A2), тъй като 2 е частична наредба в A2.
Очевидно е, че изображението (A1 A2), което дефинирахме по-горе е най-малък елемент на (A1 A2).
Ще покажем, че всяка монотонно растяща редица от елементи на
(A1 A2) притежава точна горна граница.
Нека f0 f1 … fn …е монотонно растяща редица от елементи на
(A1 A2). Тогава за всяко фиксирано a A1 редицата
f0 (a) 2 f1 (a) 2 …2 fn (a) 2 …е монотонна. Да положим h (a) = .
Очевидно е, че h : A1 A2 е добре определено изображение, тъй като точната горна граница на редицата { fn (a)} е единствена.
Твърдение: Дефинираното изображение h е непрекъснато.
Доказателство: нека a0 1 a1 1 …1 ak 1 …е монотонно растяща редица от елементи на A1. Трябва да покажем, че h ( ) e точна горна граница на редицата { h (ak) } в A2.
Имаме h ( ) = . Използвали сме, че fn е непрекъснато изображение за всяко n N.
За всяко s N, h (as) = 2 = h ( ).
Използвали сме, че fn (as) 2 и лемата от по-горе.
Така h ( ) e горна граница на редицата { h (ak)}. Нека b е горна граница на редицата { h (ak)}, т.е. за всяко k N, h (ak) 2 b.
Имаме h (ak) = за всяко k N fn (ak) 2 h (ak), h (ak) 2 b за всеки k, n N, т.е. fn (ak) 2 b за всеки k, n N. Тогава за всяко n N
b е горна граница на редицата fn (a0) 2 fn (a1) 2 …
за всяко n N, 2 b 2 b, т.е. h ( ) 2 b.
Така h ( ) e точна горна граница на редицата { h (ak)}.
Твърдение: Дефинираното изображение h е точна граница на редицата
{ fn} в областта (A1 A2).
Доказателство: за всяко a A1 имаме fn (a) 2 = h (a) fn h за всяко n N. Нека h1 (A1 A2) и fn h1 за всяко n N. Нека a A1.
За всяко n N имаме fn (a) 2 h1 (a) 2 h1 (a), т.е. h (a) 2 h1 (a). Така h h1. Окончателно, h е точна горна граница на редицата { fn}.
И така доказахме, че (A1 A2) = ( (A1 A2), , ) е област на Скот.
Свойства на непрекъснатите изображения
Нека A1 = (A1, 1, 1), A2 = (A2, 2, 2), A3 = (A3, 3, 3) са области на Скот.
Твърдение: Некa f : A1 A2 и g : A2 A3 са непрекъснати изображения.
Тогава композицията h : A1 A3, дефинирана с h (a) = g (f (a))
за всяко a A1 е непрекъснато изображение.
Доказателство: нека a0 1 a1 1 … е монотонно растяща редица в A1.
За всяко n N имаме an 1 f (an) 2 f ( ), тъй като f е монотонно g (f (an)) 3 g (f ( )), тъй като g е монотонно.
Така h (an) 3 h ( ) за всяко n N, т.е. h ( ) e горна граница на
редицата { h (an) }. Нека b A3 е горна граница на { h (an) }, т.е. h (an) 3 b за всяко n N. Тогава g (f (an)) 3 b за всяко n N 3 b
g ( ) 3 b, тъй като { f (an)} е монотонна в A2 g (f ( )) 3 b, тъй като { an} е монотонна в A1 h ( ) 3 b. Окончателно, h ( ) e точна горна граница на редицата { h (an)}.
Нека A = (A, , ), Ai = (Ai, i, i), i = 1, 2, …, n са области на Скот.
Твърдение: Нека fi : A Ai са непрекъснати изображения, i = 1, 2, …, n.
Дефинираме изображение f1 x f2 x …fn : A A1 x A2 x … An,
(f1 x f2 x …fn)(a) = (f1 (a), f2 (a), …, fn (a)) за всяко a A. Твърдим, че
f1 x f2 x …x fn е непрекъснато.
Доказателство: преди всичко, A1 x A2 x …x An е декартовото произведение на области на Скот, което дефинирахме по-горе.
Нека a0 a1 …е монотонна редица от елементи на A. За всяко i N
имаме (f1 x f2 x …fn)(ai) = (f1 (ai), f2 (ai), …, fn (ai))
(f1 ( ), f2 ( ), …, fn ( )) = (f1 x f2 x …fn)( ). Използвали сме, че f1, …, fn са монотонни. Така (f1 x f2 x …fn)( ) е горна граница на
редицата { (f1 x f2 x …fn)(ai) }. Нека b = (b1, b2, …, bn) A1 x A2 x …x An е горна граница на тази редица, т.е. (f1 x f2 x …fn)(ai) b за всяко i N.
Тогава за всяко k N имаме f1 (ak) 1 b1, f2 (ak) 2 b2, …, fn (ak) n bn
1 b1, 2 b2, …, n bn
f1 ( ) 1 b1, f2 ( ) 2 b2, …, fn ( ) n bn, тъй като f1, …, fn са непрекъснати. Така (f1 ( ), f2 ( ), …, fn ( )) b, т.е.
(f1 x f2 x …fn)( ) b и (f1 x f2 x …fn)( ) е точна горна граница на редицата { (f1 x f2 x …fn)(ai) }.
Нека A = (A, , ) e област на Скот и f : A A е тотално изображение.
Казваме, че a A е неподвижна точка на f, ако f (a) = a.
Казваме, че a A е най-малка неподвижна точка на f, ако f (a) = a и
за всяко b A, такова че f (b) = b имаме a b.
Естествено, ако f притежава най-малка неподвижна точка, тя е единствена.
Казваме, че a A е квазинеподвижна точка на f, ако f (a) a.
Казваме, че a A е най-малка квазинеподвижна точка на f,
ако f (a) a и за всяко b A, такова че f (b) b имаме a b.
Естествено, ако f притежава най-малка квазинеподвижна точка, тя е единствена. Освен това, ако a A е най-малка неподвижна точка на f и b A е най-малка квазинеподвижна точка на f, то b a. В общия случай обратното не е изпълнено. Вярно е, обаче, следното
Твърдение: Нека f : A A е монотонно изображение. Нека a A е
най-малка квазинеподвижна точка на f. Тогава a е най-малка неподвижна точка на f.
Доказателство: достатъчно е да покажем, че a е неподвижна точка на f.
Тъй като a е квазинеподвижна, то f (a) a. Tъй като f е монотонно, то
f (f (a)) f (a) f (a) е квазинеподвижна точка на f. Тъй като a е
най-малка квазинеподвижна точка на f, то a f (a). Така f (a) = a.
Теорема (Кнастер-Тарски): Нека f : A A е непрекъснато изображение. Тогава f притежава най-малка квазинеподвижна точка.
Доказателство: конструираме редица { an} от елементи на A с
индукция по n.
База: при n = 0, a0 = .
Предположение: нека е дефинирано an, n 0.
Стъпка: тогава an+1 = f (an).
Твърдим, че редицата { an} е монотонна. Ще покажем това с
индукция по n.
База: при n = 0, a0 = a1.
Предположение: нека an an+1, n 0.
Стъпка: тъй като f е монотонно, то f (an) f (an+1), т.е. an+1 an+2.
Нека a = . Твърдим, че a е най-малка квазинеподвижна точка на f.
Действително, f (a) = f ( ) = = .
Имаме , тъй като е горна граница на редицата { an+1}.
Така f (a) = a a е квазинеподвижна точка на f.
Нека b A е квазинеподвижна точка на f, т.е. f (b) b.
С индукция по n ще покажем, че an b за всяко n N.
База: при n = 0, a0 = b.
Предположение: нека an b, n 0.
Стъпка: тогава an+1 = f (an) f (b) b. Използвали сме, че f е монотонно.
Така an b за всяко n N a = b.
Окончателно, a A е най-малка квазинеподвижна точка на f.
От горното твърдение получаваме, че всяко непрекъснато изображение притежава най-малка неподвижна точка, която е същевременно
най-малка квазинеподвижна точка.
Ще докажем още едно обобщение на теоремата на Кнастер-Тарски.
Нека Ai = (Ai, i, i), i = 1, 2, …, n са области на Скот.
Да означим А = A1 x A2 x …x An, A = (A, , (1, 2, …, n)).
Нека fi : A Ai, i = 1, 2, …, n са тотални изображения.
Съвпкупността от формалните равенства
f1 (1, 2, …, n) = 1
f2 (1, 2, …, n) = 2
…
f3 (1, 2, …, n) = n
наричаме система от уравнения за изображенията f1, f2, …, fn.
Казваме, че (a1, a2, …, an) A е решение на системата, ако
fi (a1, a2, …, an) = ai за всяко i = 1, 2, …, n.
Казваме, че (a1, a2, …, an) A е най-малко решение на системата,
ако (a1, a2, …, an) е решение на системата и за всяко решение
(b1, b2, …, bn) A на системата имаме (a1, a2, …, an) (b1, b2, …, bn).
Естествено, ако системата има най-малко решение, то е единствено.
Казваме, че (a1, a2, …, an) A е квазирешение на системата, ако
fi (a1, a2, …, an) i ai за всяко i = 1, 2, …, n.
Казваме, че (a1, a2, …, an) A е най-малко квазирешение на системата,
ако (a1, a2, …, an) е квазирешение на системата и за всяко квазирешение
(b1, b2, …, bn) A на системата имаме (a1, a2, …, an) (b1, b2, …, bn).
Естествено, ако системата има най-малко квазирешение,
то е единствено.
Теорема: Нека fi : A Ai са непрекъснати изображения. Тогава системата от уравнения за f1, f2, …, fn притежава най-малко решение, което е и най-малко квазирешение.
Доказателство: да означим f = f1 x f2 x …x fn. Тогава f : A A и f е непрекъснато изображение, тъй като f1, f2, …, fn са непрекъснати.
От теоремата на Кнастер-Тарски f притежава най-малка неподвижна точка, която е и най-малка квазинеподвижна точка. Да я означим с
(a1, a2, …, an) A. Ще покажем, че (a1, a2, …, an) е най-малко решение на системата. Имаме f (a1, a2, …, an) = (f1 (a1, …, an), f2 (a1, …, an),
…, fn (a1, a2, …, an)) = (a1, a2, …, an), така че fi (a1, …, an) = ai за всяко
i = 1, 2, …, n. Така (a1, …, an) е решение на системата. Нека (b1, …, bn) A е решение на системата, т.е. fi (b1, …, bn) = bi за всяко i = 1, 2, …, n.
Тогава f (b1, …, bn) = (b1, …, bn), така че (b1, …, bn) е неподвижна
точка на f (a1, …, an) (b1, …, bn).
Аналогично, като се използва, че (a1, …, an) е най-малка квазинеподвижна точка на f се показва, че (a1, …, an) е
най-малко квазирешение на системата за f1, …, fn.
Ще използваме доказателството на теоремата на Кнастер-Тарски за да получим най-малкото решение (a1, …, an) в явен вид.
Имаме, че (a1, …, an) = , където d0 = (1, 2, …, n), dk+1 = f (dk),
dk A за всяко k N. Да означим аi0 = i, i = 1, 2, …, n, за всяко k N (индуктивно) aik+1 = fi (a1k, a2k, …, ank), i = 1, 2, …, n.
Твърдим, че dk = (a1k, a2k, …, ank) за всяко k N.
База: при k = 0, d0 = (1, 2, …, n) = (a10, a20, …, an0).
Предположение: нека dk = (a1k, a2k, …, ank), k 0.
Стъпка: тогава dk+1 = f (dk) = (f1 x f2 x …x fn)(a1k, a2k, …, ank) =
= (f1 (a1k, a2k, …, ank), f2 (a1k, a2k, …, ank), …, fn (a1k, a2k, …, ank)) =
= (a1k+1, a2k+1, …, ank+1).
Сега получаваме (a1, …, an) = =
= , т.е. ai = , i = 1, 2, …, n.
Използвали сме твърдението за точна горна граница на монотонна редица в декартово произведение на области на Скот.
Рекурсивни програми. Синтаксис и операционна семантика.
Ще считаме, че в нашия език за програмиране има само
два типа данни: Nat и Bool. Nat са естествените числа, в Bool има две стойности tt - истина и ff - лъжа. Ще считаме, че разполагаме с определен набор от основни операции oт следните видове:
-
операции f : Natn Nat, n 1, например събиране (+),
умножение (*) и т.н.;
-
операции f : Natn Bool, n 1, например равенство (=), различните видове неравенства (<, <=, >, >=) и т.н.;
-
операции f : Booln Bool, n 1, например конюнкция (&), дизюнкция (), отрицание () и т.н.
Синтактичните елементи на езика са следните:
-
константи от тип Nat и Bool за означаване на елементи
на Nat и Bool;
-
символи за основните операции;
-
обектови променливи, които ще означаваме с главните букви
X, Y, Z, …евентуално с индекси; тези променливи ще приемат стойности естествените числа от Nat;
-
функционални променливи, които ще означаваме с Fkn, където k е индекс; променливата Fkn ще приема стойност частична функция, n указва броят на аргументите на функцията;
-
точки, запетаи, скоби, чрез които ще постигаме еднозначен синтактичен анализ.
Дефинираме индуктивно понятието терм от тип Nat.
База:
-
Всяка константа от тип Nat е терм от тип Nat.
-
Всяка обектова променлива е терм от тип Nat.
Предположение: нека 1, 2, …, n са термове от тип Nat.
Стъпка:
-
Ако f : Natn Nat е основна операция, то f (1, 2, …, n) е терм от тип Nat.
-
Ако Fkn е функционална променлива, то Fkn (1, 2, …, n) е терм от тип Nat. Тези термове от тип Nat наричаме обръщения към функции.
Дефинираме индуктивно понятието терм от тип Bool.
База:
-
Всяка константа от тип Bool е терм от тип Bool.
-
Ако f : Natn Bool е основна операция и 1, 2, …, n са термове от тип Nat, то f (1, 2, …, n) е терм от тип Bool.
Предположение: нека 1, 2, …, n са термове от тип Bool.
Стъпка:
-
Ако f : Booln Bool е основна операция, то f (1, 2, …, n) е терм от тип Bool.
Дефинираме понятието условен терм. Нека е терм от тип Bool,
1, 2 са термове от тип Nat. Тогава if then 1 else 2 е условен терм.
По-нататък, под терм ще разбираме кой да е от трите вида термове.
Ясно е, че ако е терм, то в участват краен брой обектови и функционални променливи. Ще използваме означението
(X1, …, Xn, , , …, ) за да укажем, че обектовите променливи на са сред X1, …, Xn, а функционалните променливи на са сред
, , …, . Например, X+Y (X, Y, Z). Понякога ще използваме съкратен запис (X, F). Също, ще си позволяваме да изпускаме броя на аргументите за една функционална променлива, ако той не е съществен.
Нека 1, 2, …, n са термове от тип Nat, (X1, …, Xn, F) е терм.
Означаваме с (X1/1, X2/2, …, Xn/n, F) термът, който се получава от чрез едновременно заместване на всяка от обектовите променливи
X1, …, Xn с термовете 1, …, n съответно. Понякога ще използваме съкратен запис (X/, F).
Термове, в които не участват обектови променливи ще наричаме функционални термове. Естествено, в горните означения, ако термовете 1, …, n са функционални, то (X/, F) също е функционален терм.
Термове, в които не участват никакви променливи ще наричаме основни термове.
Програма е синтактичен обект R от следния вид:
0 (X1, …, Xn, , , …, ), where
(X1, …, ) = 1 (X1, …, , , , …, )
(X1, …, ) = 2 (X1, …, , , , …, )
…
(X1, …, ) = k (X1, …, , , , …, )
Тук 0 е терм от тип Nat, който наричаме
Сподели с приятели: |