Лекции по семантика на езиците за програмиране

Четени през летния семестър на учебната 2003/2004 година. Лектор тогава беше професор Иван Сосков. Използвал съм само мои записки от лекции, както и учебника Теория на програмите на Сосков и Дичев. Изрично отбелязвам, че темата схеми на програми не е довършена – само са дадени дефинициите на синтаксиса и семантиката на итеративните и рекурсивните схеми. Трябва да се включат още превода на итеративни схеми в рекурсивни (чрез опашкови функции) и евентуално примера на Патерсън и Хюит (който обикновено не се предава, тъй като времето не достига).

Добре е да имате инсталиран MathType, за да нямате проблеми при разчитането. От този линк http://www.dessci.com/en/dl/MTW6.exe може да изтеглете trial версия за един месец.

Въведение
С N ще означаваме множеството на естествените числа,

N = { 0, 1, 2, … }. С N^k, k > 0, ще означаваме k-тата декартова

степен на N, N¹ = N. С N^w означаваме множеството от всички безкрайни редици от естествени числа. За краткост наредената k-торка x₁, x₂, …, x_k или безкрайната редица x₁, x₂, … ще означаваме с x, като размерът ще се разбира от контекста.

В курса често ще разискваме функции, които са дефинирани в N^k, k > 0 и приемат стойности в N – наричаме ги функции на k аргумента. Задаваме ги чрез техните графики, които представляват (k+1)-местни релации над N, т.е. подмножества на N^k+1. Нека G  N^k+1.

Тогава G задава функция на k аргумента, ако е изпълнено следното условие: ако (x, y)  G и (x, y)  G, то y = y.

Ако допълнително е изпълнено: за всяко x  N^k съществува y  N, такова че (x, y)  G, казваме че G задава тотална функция. Ако това условие не е изпълнено, казваме че функцията е частична. Нека G задава функция f на k аргумента. Записваме G = G_f.

Ще записваме f (x)  y, ако (x, y)  G_f.

Дефинираме Dom (f) = { x  N^k | съществува y  N, така че (x, y)  G_f }.

Дефинираме Ran (f) = { y  N | съществува x  N^k, така че (x, y)  G_f }.

Ще означаваме !f (x), ако x  Dom (f), т.е. съществува y  N,

такова че f (x)  y. Ако x  Dom (f) ще означаваме !f (x).

За да подчертаем, че f е частична функция на k аргумента

записваме f : N^k  N.

С ! означаваме функцията, която не е дефинирана никъде.

Нека f и g са функции (на различен, възможно безкраен брой аргументи).

Означаваме f (x₁)  g (x₂), ако за всяко y  N, f (x₁)  y  g (x₂)  y.

Лесно се вижда, че това означава следното:

-смятането на Чърч. Ако f : N^k  N е частична функция

записваме f = x.f (x).
Пространството F_n. Теорема на Кнастер-Тарски. Правило на Скот.
С F_n, n > 0 означаваме множеството на всички частични функции на

n аргумента. В множеството F_n въвеждаме частична наредба:

(f, g  F_n) f  g  G_f  G_g  за всяко x  Nⁿ, y  N имаме

f (x)  y  g (x)  y. Ако f  g, казваме че f е подфункция на g или, че g е продължение на f. Въведената наредба не е линейна – всеки две различни тотални функции са несравними. Наредбата притежава единствен минимален елемент – функцията !, която се продължава до всяка функция. Също така, наредбата притежава безброй много (дори неизброимо много) максимални елементи – това са всички тотални функции, които не могат да бъдат продължавани.

ако за всяка f  X имаме, че f  g. Казваме, че g  F_n е точна горна граница на X, ако за всяка горна граница g на X имаме, че g  g.

Естествено, ако X притежава точна горна граница, то тя е единствена.
Нека { f_k} е редица от функции, f_k  F_n. Казваме, че редицата е монотонно растяща, ако f_k  f_k+1 за всяко k  N.
Твърдение: Нека { f_k} е монотонно растяща редица от

функции, f_k  F_n. Дефинираме функцията g по следния начин:

(x  Nⁿ, y  N) g (x)  y  съществува k  N, такова че f_k (x)  y.

Тогава g е добре дефинирана n-местна функция, която е точна горна граница на { f_k }.

Доказателство: нека x  Nⁿ, y₁, y₂  N и g (x)  y₁, g (x)  y₂. Тогава съществуват k₁, k₂  N, такива че (x)  y₁ и (x)  y₂.

Нека за определеност k₁  k₂. Тогава   y₁ = y₂.

Получихме, че g е добре определена функция.

Нека k  N и f_k (x)  y, x  Nⁿ, y  N. Тогава по определение g (x)  y 

f_k  g за всяко k  N  g е горна граница на { f_k}.

Нека h  F_n е произволна горна граница на { f_k}.

Нека x  Nⁿ, y  N и g (x)  y. Тогава съществува k  N, такова че

f_k (x)  y, но f_k  h  h (x)  y. Така g  h. Твърдението е доказано.

Нека  е частична функция. Казваме, че  е крайна функция, ако

Тогава съществува m  N, такова че   f_m.

Доказателство: ако Dom () = , твърдението е очевидно.

Нека Dom () = { x₀, x₁, …, x_r }, x_i  Nⁿ. Нека  (x_i)  y_i, i = 0, 1, …, r.

Да означим g = . Имаме, че   g  g (x_i)  y_i, i = 0, 1, …, r 

за всяко i  { 0, 1, …, r } съществува k_i  N, такова че (x_i)  y_i.

Нека m = max (k₀, k₁, …, k_r). Тогава  f_m, i = 1, 2, …, r  f_m (x_i)  y_i за всяко i = 0, 1, …, r    f_m.
Ще казваме, че Г e оператор, ако Г e тотално изображение на във . Означаваме Г :  .
Нека Г : F_n  F_m е оператор. Ще казваме, че Г е компактен оператор, ако за всяка функция f  F_n, x  N^m, y  N имаме, че

Г (f) (x)  y  съществува крайна   f, такава че Г () (x)  y.

Интуитивно, за да изчислим Г (f) (x) за дадено x използваме само краен брой стойности на f.

Нека Г : F₁  F₁ е дефиниран с

Ако f е тотална функция, то Г (f) (x)  0 за всяко x  N, но за всяка крайна   f имаме, че Г (f) (x)  1 за всяко x  N, тъй като крайните функции не са тотални.

Тогава Г₁ (f) = Г₂ (f) за всяка f  F_n .

Доказателство: нека f  F_n , x  N^m, y  N. Тогава Г₁ (f) (x)  y  съществува крайна   f, такава че Г₁ () (x)  y 

съществува крайна   f, такава че Г₂ () (x)  y, тъй като Г₁ () = Г₂ ()  Г₂ (f) (x)  y. Така Г₁ (f) = Г₂ (f).

ако за всеки f, g  F_n имаме f  g  Г (f)  Г (g).

Доказателство: нека Г : F_n  F_m е компактен оператор.

Нека f, g  F_n и f  g. Нека x  N^m, y  N и Г (f) (x)  y. Тогава съществува

крайна   f, такава че Г () (x)  y, но f  g    g,  е крайна и

ако за всяка монотонно растяща редица { f_k}, f_k  F_n имаме,

че Г ( ) е точна горна граница на { }.

Твърдение: Всеки непрекъснат оператор е монотонен.

Доказателство: нека Г : F_n  F_m е непрекъснат оператор.

Нека f, g  F_n и f  g. Разглеждаме редицата f, g, g, …, g, ….

Очевидно тази редица е монотонна и нейната точна горна граница е g.

Тогава Г (g) е точна горна граница на { Г (f), Г (g) }  Г (f)  Г (g).
Така, ако Г е непрекъснат оператор, то за всяка монотонно растяща редица { f_k} имаме, че { Г (f_k)} също е монотонно растяща и

Г ( ) = .
Твърдение: Всеки компактен оператор е непрекъснат.

Доказателство: нека Г : F_n  F_m е компактен оператор. Нека { f_k } е монотонно растяща редица. Полагаме g = . Трябва да покажем,

че Г (g) е точна горна граница на { Г (f_k)}. Тъй като g е горна граница на

{ f_k}, то за всяко k  N имаме, че f_k  g. От по-предното твърдение имаме, че Г е монотонен оператор  Г (f_k)  Г (g) за всяко k  N 

Ще покажем, че Г (g)  h. Нека x  N^m, y  N и Г (g) (x)  y.

Тогава съществува крайна   g, такава че Г () (x)  y.

Имаме, че   g =  съществува m  N, такова че   f_m 

граница на { Г (f_k)}.

Доказателство: нека Г : F_n  F_m е непрекъснат оператор.

Нека f  F_n. Нека _k е ограничението на функцията f върху

[0, k] x [0, k] x … x [0, k]. Ясно е, че { _k} е монотонно растяща от крайни функции и = f. Тъй като Г е непрекъснат оператор, то

от по-горе получаваме, че Г (f) = .

Нека x  N^m, y  N и Г (f) (x)  y. Тогава съществува k  N,

такова че Г (_k)(x)  y и _k е крайна функция.

Обратно, нека   f е крайна функция и Г ()(x)  y.

Тогава Г (f) (x)  y, тъй като Г e монотонен оператор.

Така Г е компактен оператор.

Казваме, че f  F_n е неподвижна точка за Г, ако Г (f) = f.

Казваме, че f  F_n е квазинеподвижна точка за Г, ако Г (f)  f.

Oчевидно всяка неподвижна точка за Г е и квазинеподвижна за Г.

Казваме, че f  F_n е най-малка неподвижна точка за Г,

ако f е неподвижна точка за Г и за всяка неподвижна точка

g на Г имаме, че f  g. Ясно е, че ако един оператор притежава

най-малка неподвижна точка, то тя е единствена.

Аналогично се дефинира най-малка квазинеподвижна точка за Г.

Естествено, ако Г притежава най-малка квазинеподвижна точка, то тя е единствена. Освен това, ако f е най-малка квазинеподвижна точка за Г и g e най-малка неподвижна точка за Г, то f  g, тъй като g е квазинеподвижна за Г. Обратното в общия случай не е изпълнено.

Вярно е, обаче, следното
Твърдение: Нека Г : F_n  F_n е монотонен оператор. Нека f  F_n е

най-малка квазинеподвижна точка за Г. Тогава f е най-малка неподвижна точка за Г.

Доказателство: имаме, че Г (f)  f  (Г – монотонен) Г (Г (f))  Г (f) 

 Г (f) е квазинеподвижна точка за Г  f  Г (f). Така f е неподвижна точка за Г. Нека g  F_n е неподвижна точка за Г. Toгава g е квазинеподвижна точка за Г  f  g, тъй като f е най-малка квазинеподвижна точка за Г. Така f е най-малка неподвижна точка за Г.

Доказателство: с индукция по k дефинираме редицата от функции { f_k}.

База: f₀ = !.

Предположение: нека f_k е дефинирана, k  0.

Стъпка: тогава f_k+1 = Г (f_k).

С индукция по k ще покажем, че редицата { f_k} е монотонно растяща.

База: очевидно f₀  f₁, тъй като f₀ = !.

Предположение: нека f_k  f_k+1, k  0.

Стъпка: тъй като Г e компактен, то Г е монотонен  Г (f_k)  Г (f_k+1), т.е.

f_k+1  f_k+2.

Да означим f = .

Ще покажем, че f е най-малка квазинеподвижна точка за Г.

Имаме Г (f) = Г ( ) = =  = f. Използвали сме,

че Г е непрекъснат оператор, тъй като Г е компактен.

Така f е квазинеподвижна точка за Г.

Нека g  F_n e произволна квазинеподвижна точка за Г.

Ще покажем, че f  g. За целта с индукция по k ще покажем, че f_k  g.

База: f₀  g, тъй като f₀ = !.

Предположение: нека f_k  g, k  0.

Стъпка: тъй като Г e компактен оператор, то Г е монотонен 

Получихме, че g е горна граница на { f_k}, но f е точната горна граница

на { f_k}  f  g. Теоремата е доказана.
Тъй като всеки компактен оператор е монотонен, то от твърдението

по-горе получаваме, че всеки компактен оператор притежава най-малка неподвижна точка (която е и най-малка квазинеподвижна точка). Доказателството на теоремата на Кнастер-Тарски е конструктивно и дава метод за нейното намиране.

Нека P е някакво свойство на функциите от F_n, т.е. P : F_n  { true, false }.

Да предположим, че сме доказали P (!) и за всяка g  F_n, P (g)  P (Г (g)). С индукция по k ще покажем, че P (f_k) за всяко k  N.

База: при k = 0, f₀ = ! и P (f₀) вече е доказано.

Предположение: нека е доказано P (f_k).

Стъпка: имаме P (f_k)  P (Г (f_k)), P (f_k) е вярно  P (Г (f_k)), т.е. P (f_k+1).

С пример ще покажем, че това не е така. Разглеждаме операторът

Тривиално се проверява, че Г e компактен оператор.

С индукция по k ще покажем, че f_k = x. if x < k then x! else !.

База: при k = 0, f₀ = ! = x. if x < 0 then x! else !.

Предположение: нека f_k = x. if x < k then x! else !, k  0.

Стъпка: имаме f_k+1 = Г (f_k). Да означим g = x. if x < k+1 then x! else !.

Ако x = 0, то f_k+1 (0)  1 и g (0)  0! = 1, тъй като 0 < k+1.

Така f_k+1 (0)  g (0).

Ако 0 < x < k+1, то f_k+1 (x)  x * f_k (x-1) и x-1 < k  f_k (x-1)  (x-1)! 

f_k+1 (x)  x! и g (x)  x!, тъй като x < k+1. Така f_k (x)  g (x) за всяко x < k+1.

Ако x  k+1, то f_k+1 (x)  x * f_k (x-1) и x-1  k  ! f_k (x-1)  ! f_k+1 (x) и

! g (x), тъй като x  k+1. Така f_k (x)  g (x) за всяко x  k+1.

Окончателно f_k+1 (x)  g (x) за всяко x  N.
Оттук веднага получаваме, че f = = x. x! е най-малката неподвижна точка на Г.
Да дефинираме свойството P по следния начин:

P (g)  съществува x  N, такова че ! g (x).

Нека P (g). Тогава съществува x  N, такова че ! g (x). Имаме x+1 > 0 и

Въпреки това, не е вярно, че P (x. x!), тъй като x. x! е тотална функция.

P (f_k) за всяко k  N  P ( ).

Toгава P (f), където f е най-малката неподвижна точка на Г.

Доказателство: имаме f = , f₀ = !, f_k+1 = Г (f_k) за всяко k  N.

Вече показахме, че в такъв случай P (f_k) за всяко k  N, също { f_k} е монотонна редица и P е непрекъснато свойство. Така P ( ), т.е. P (f).

Ще дадем някои примери за непрекъснати свойства.
Свойство P от вида: P (f)  за всяко x  Nⁿ, (! f (x) и I (x))  O (x, f (x)), където I (x) и O (x, y) са произволни предикати над ествените числа се нарича условие за частична коректност. Идеята е, че предикатът I е условие за входните данни, а предикатът O е условие за

изходните данни. Ясно е, че P (!) е вярно при всеки избор на предикатите I, O.

Доказателство: нека P (f)  за всяко x  Nⁿ, (! f (x) и I (x))  O (x, f (x)).

Нека { f_k} е монотонно растяща редица от функции и P (f_k) за всяко k  N.

Нека f = . Нека I (x) и ! f (x), f (x)  y. Тогава съществува k  N, такова че f_k (x)  y, т.е. I (x) и ! f_k (x)  O (x, f_k (x)), т.е. О (x, y) 

 O (x, f (x)). Така доказахме P (f).
По аналогичен начин се показва, че всяко условие за тотална коректност е непрекъснато. Пропускаме доказателството, тъй като правилото на Скот не е приложимо за такива условия – ако P е условие за тотална коректност, то P (!) не е вярно (освен в тривиалния случай, когато няма входни данни, т.е. I  false).
Нека отново разгледаме компактният оператор Г : F₁  F₁,

Г (f)(x)  if x = 0 then 1 else x * f (x-1) за всеки f  F₁, 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 * (x-1)! = x!. Така P (Г (g)).

най-малката неподвижна точка на Г e x. x!.

Нека { g_k} е монотонно растяща редица, g = .

Нека f_k  g_k за всяко k  N. Тогава f  g.

Доказателство: имаме f_k  g_k  за всяко k  N, така че

Toгава свойството P, дефинирано с P (g)  Г₁ (g)  Г₂ (g) е непрекъснато.

Доказателство: нека { f_k} е монотонно растяща редица и

P (f_k) за всяко k  N, т.е. Г₁ (f_k)  Г₂ (f_k) за всяко k  N.

От лемата  . Нека f = .

Тогава Г₁ (f) = Г₁ ( ) =  = Г₂ ( ) = Г₂ (f).

Използвали сме, че Г₁ и Г₂ са непрекъснати оператори. Така P (f).
Като пример свойството P, дефинирано с P (g)  g  x. g (g (x)) е непрекъснато, тъй като Г₁ (g) = g и Г₂ (g)(x)  g (g (x)) са компактни оператори.
Твърдение: Нека P₁ и P₂ са непрекъснати свойства.

Тогава свойството P (g), дефинирано с P (g)  P₁ (g) и P₂ (g) е непрекъснато.

Доказателство: нека { f_k} е монотонно растяща редица от функции и

P (f_k) за всяко k  N. Тогава P₁ (f_k) за всяко k  N и

P₂ (f_k) за всяко k  N. Нека f = . От непрекъснатостта на P₁ и P₂ получаваме P₁ (f) и P₂ (f). С това показахме P (f).
Следствие: Нека Г₁ : F_m  F_n и Г₂ : F_m  F_n са компактни оператори.

Toгава свойството P, дефинирано с P (g)  Г₁ (g) = Г₂ (g) е непрекъснато.

Доказателство: Г₁ (g) = Г₂ (g)  Г₁ (g)  Г₂ (g) и Г₂ (g)  Г₁ (g). Прилагаме

предните две твърдения.

P (g), дефинирано с P (g)  P₁ (g) или P₂ (g) е непрекъснато.

Доказателство: нека { f_k} е монотонно растяща редица и P (f_k)

за всяко k  N, т.е. P₁ (f_k) или P₂ (f_k) за всяко k  N.

Нека N₁ = { k|P₁ (f_k) } и N₂ = { k|P₂ (f_k) }. Имаме N₁  N₂ = N, така че поне едно от N₁, N₂ е безкрайно. Нека, например, N₁ е безкрайно.

Нека h е биективна функция, такава че h : N  N₁ и за всеки x, y  N

x  y  h (x)  h (y). С други думи N₁ = { h (0), h (1), …, h (n), …} и

h (0) < h (1) < …< h (n) < …. Ясно е, че { } е монотонна редица.

Твърдим, че = . Имаме  , тъй като

за всяко k  N, h (k)  k  f_k  и можем да приложим лемата.

Също, ако (x)  y, то (x)  y  (x)  y, тъй като e член на редицата { f_k}. Така  . Тъй като P₁ е непрекъснато и P₁ ( ) за всяко k  N, то P₁ ( )  P₁ ( )  P₁ ( ) или P₂ ( ).

С това показахме P ( ).

Нека P : F₁  { true, false} е свойството, дефинирано с P (f)  f е тотална. Тогава P е непрекъснато. Действително, ако { f_k} е монотонно растяща редица от тотални функции, то всички функции в редицата съвпадат с точната горна граница на редицата, така че и тя е тотална.

От друга страна, отрицанието на P не е непрекъснато. Действително, нека f е произволна тотална функция. Нека _k е ограничението на f върху [0, k], k  N. Ясно е, че { _k} е монотонна редица и = f.

Oчевидно _k не е тотална за всяко k  N, но f е тотална функция.

Дефинираме оператор Г по следния начин:

Ще покажем, че за всяко x  N имаме f (x)  f (f (x)). За целта дефинираме свойство P по следния начин: P (g)  за всяко x  N, g (x)  f (g (x)).

Преди всичко, свойството P е непрекъснато, тъй като Г₁ (g) = g и

Г₂ (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)). Остава да приложим правилото на Скот.

Ще покажем, че за всеки 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 е непрекъснато свойство, тъй като Г₁ (g)(x, y)  h (g (x, y)) и

Нека 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, който е най-малък относно , т.е.

  a за всяко a  A. Нека, освен това, всяка монотонно растяща редица

а₀  а₁  …  a_n  …има точна горна граница в A, т.е. съществува a  A, такова че a_n  a за всяко n  N и за всяко b  A, такова че a_n  b за всяко n  N имаме, че a  b. Естествено, точната горна граница a  А е единствена, означаваме a = . При тези предположения, наредената тройка (A, , ) наричаме област на Скот. Множеството А наричаме носител на областта на Скот. От самата дефиниция следва, че А е непразно (  A). Обикновено ще означаваме областта на Скот по същия начин, както носителя: А = (A, , ).

По-общо, ако B е произволно множество и F_n^B е множеството на

n-местните частични функции на B, т.е. F_n^B = { f | f : Bⁿ  B },

то F_n^B = (F_n^B, , !) е област на Скот. Естествено, F_n = F_n^N.

Всяка монотонна редица B₀  B₁  …  B_n  …има точна горна граница – обединението на множествата в редицата.

Ще проверим, че  действително е частична наредба.

Имаме 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.

Нека за всяко n  N имаме x_n = . Тогава  e точна горна граница на редицата { x_n}.

Нека съществува n  N, такова че x_n  . Тогава x_n = x_n+1. Оттук x_n+1  , така че x_n+1 = x_n+2. По индукция x_n = x_n+1 = …= x_n+k = …. Тогава x_n е точна граница на редицата { x_n}.

И така доказахме, че A = (A, , ) е област на Скот. Тя се нарича плоска област на Скот.

Тройката (N, , 0), където  е стандартната наредба в N не е област на Скот, тъй като редицата 0  1  2  …е монотонно растяща редица, която няма точна горна граница.

редици в A. Нека a_n  b_n за всяко n  N. Тогава  .

Доказателство: за всяко k  N е изпълнено a_k  b_k  , тъй като

е горна граница на { b_k}. Така е горна граница на { a_k} 

 , тъй като e точна горна граница на { a_k}.
Конструкции на области на Скот
Нека A₁ = (A₁, ₁, ₁), A₂ = (A₂, ₂, ₂), …, A_n = (A_n, _n, _n), n  2 са области на Скот. Означаваме A = A₁ x A₂ x … x A_n – декартовото произведение на множествата A₁, A₂, …, A_n.

В A въвеждаме релация  : за всеки a_i  A_i, b_i  A_i, i = 1, 2, …, n,

(a₁, a₂, …, a_n)  (b₁, b₂, …, b_n)  a₁ ₁ b₁ и a₂ ₂ b₂ и …и a_n _n b_n.

Очевидно е, че  е частична наредба в А, тъй като ₁, ₂, …, _n са частични наредби в A₁, A₂, …, A_n съответно. При това  = (₁, ₂, …, _n) е най-малък елемент в A относно .

i = 1, 2, …, n. Тогава (a₁, a₂, …, a_n)  A е точна горна граница на

редицата { (a_k¹, a_k², …, a_kⁿ) }.

Доказателство: преди всичко, за всяко i  { 1, 2, …, n } редицата { a_kⁱ} е монотонно растяща редица в A_i относно _i, така че елементът a_i е добре дефиниран. За всяко k  N имаме a_k¹ ₁ a₁, a_k² ₂ a₂, …, a_kⁿ _n a_n, така че

(a_k¹, a_k², …, a_kⁿ)  (a₁, a₂, …, a_n) за всяко k  N, т.е. (a₁, a₂, …, a_n) е горна граница на { (a_k¹, a_k², …, a_kⁿ) }. Нека (a_k¹, a_k², …, a_kⁿ)  (b₁, b₂, …, b_n) за всяко k  N. Тогава за всяко i  { 1, 2, …, n}, a_kⁱ _i b_i за всяко k  N, така че b_i е горна граница на { a_kⁱ}  a_i _i b_i. Така (a₁, a₂, …, a_n)  (b₁, b₂, …, b_n), т.е. (a₁, a₂, …, a_n) е точна горна граница на { (a_k¹, a_k², …, a_kⁿ) }.
И така показахме, че A = (A, , ) е област на Скот, където

A = A₁ x A₂ x … x A_n,  е дефинираната частична наредба,

 = (₁, ₂, …, _n). Тази област на Скот наричаме декартово произведение на областите на Скот A₁, A₂, …, A_n.
Нека A₁ = (A₁, ₁, ₁), A₂ = (A₂, ₂, ₂) са области на Скот.
Казваме, че изображението f : A₁  A₂ е непрекъснато, ако за всяка монотонно растяща редица a₀ ₁ a₁ ₁ …₁ a_n ₁ …от елементи на A₁ имаме, че f ( ) е точна горна граница на редицата { f (a_n)} в A₂.

Изрично отбелязваме, че непрекъснатите изображения са тотални, т.е. дефинирани за всеки елемент на A₁.

за всеки a, b  A₁ имаме a ₁ b  f (a) ₂ f (b).

Доказателство: нека a, b  A₁ и a ₁ b. Разглеждаме редицата

a, b, b, …, b, …от елементи на A₁. Естествено, тя е монотонна и очевидно има точна горна граница b. Тъй като f е непрекъснато изображение, то

f (b) е точна граница на { f (a), f (b)}  f (a) ₂ f (b).

a₀ ₁ a₁ ₁ …₁ a_n ₁ …е монотонно растяща редица в A₁, то

f (a₀) ₂ f (a₁) ₂ …₂ f (a_n) ₂ …е монотонно растяща редица в A₂ и

f ( ) = .

Действително, за произволна монотонна редица a₀ ₁ a₁ ₁ …от елементи на A₁ имаме, че f ( ) = b и редицата { f (a_n)} има единствен елемент b, така че тя има точна горна граница b = f ( ).

В частност, изображението  : A₁  A₂, дефинирано с  (а) = ₂ за всяко

a  A₁ е непрекъснато.

В множеството (A₁  A₂) въвеждаме релация : за всеки f, g  (A₁  A₂),

f  g  f (a) ₂ g (a) за всяко a  A₁. Ясно е, че  е частична наредба в

(A₁  A₂), тъй като ₂ е частична наредба в A₂.

Очевидно е, че изображението   (A₁  A₂), което дефинирахме по-горе е най-малък елемент на (A₁  A₂).

Ще покажем, че всяка монотонно растяща редица от елементи на

(A₁  A₂) притежава точна горна граница.
Нека f₀  f₁  …  f_n  …е монотонно растяща редица от елементи на

(A₁  A₂). Тогава за всяко фиксирано a  A₁ редицата

f₀ (a) ₂ f₁ (a) ₂ …₂ f_n (a) ₂ …е монотонна. Да положим h (a) = .

Очевидно е, че h : A₁  A₂ е добре определено изображение, тъй като точната горна граница на редицата { f_n (a)} е единствена.

Доказателство: нека a₀ ₁ a₁ ₁ …₁ a_k ₁ …е монотонно растяща редица от елементи на A₁. Трябва да покажем, че h ( ) e точна горна граница на редицата { h (a_k) } в A₂.

Имаме h ( ) = . Използвали сме, че f_n е непрекъснато изображение за всяко n  N.

За всяко s  N, h (a_s) = ₂ = h ( ).

Използвали сме, че f_n (a_s) ₂ и лемата от по-горе.

Така h ( ) e горна граница на редицата { h (a_k)}. Нека b е горна граница на редицата { h (a_k)}, т.е. за всяко k  N, h (a_k) ₂ b.

Имаме h (a_k) = за всяко k  N  f_n (a_k) ₂ h (a_k), h (a_k) ₂ b за всеки k, n  N, т.е. f_n (a_k) ₂ b за всеки k, n  N. Тогава за всяко n  N

b е горна граница на редицата f_n (a₀) ₂ f_n (a₁) ₂ … 

 за всяко n  N, ₂ b  ₂ b, т.е. h ( ) ₂ b.

Така h ( ) e точна горна граница на редицата { h (a_k)}.

{ f_n} в областта (A₁  A₂).

Доказателство: за всяко a  A₁ имаме f_n (a) ₂ = h (a)  f_n  h за всяко n  N. Нека h₁  (A₁  A₂) и f_n  h₁ за всяко n  N. Нека a  A₁.

За всяко n  N имаме f_n (a) ₂ h₁ (a)  ₂ h₁ (a), т.е. h (a) ₂ h₁ (a). Така h  h₁. Окончателно, h е точна горна граница на редицата { f_n}.

И така доказахме, че (A₁  A₂) = ( (A₁  A₂), ,  ) е област на Скот.
Свойства на непрекъснатите изображения
Нека A₁ = (A₁, ₁, ₁), A₂ = (A₂, ₂, ₂), A₃ = (A₃, ₃, ₃) са области на Скот.
Твърдение: Некa f : A₁  A₂ и g : A₂  A₃ са непрекъснати изображения.

Тогава композицията h : A₁  A₃, дефинирана с h (a) = g (f (a))

за всяко a  A₁ е непрекъснато изображение.

Доказателство: нека a₀ ₁ a₁ ₁ … е монотонно растяща редица в A₁.

За всяко n  N имаме a_n ₁  f (a_n) ₂ f ( ), тъй като f е монотонно  g (f (a_n)) ₃ g (f ( )), тъй като g е монотонно.

Така h (a_n) ₃ h ( ) за всяко n  N, т.е. h ( ) e горна граница на

редицата { h (a_n) }. Нека b  A₃ е горна граница на { h (a_n) }, т.е. h (a_n) ₃ b за всяко n  N. Тогава g (f (a_n)) ₃ b за всяко n  N  ₃ b 

g ( ) ₃ b, тъй като { f (a_n)} е монотонна в A₂  g (f ( )) ₃ b, тъй като { a_n} е монотонна в A₁  h ( ) ₃ b. Окончателно, h ( ) e точна горна граница на редицата { h (a_n)}.

Дефинираме изображение f₁ x f₂ x …f_n : A  A₁ x A₂ x … A_n,

(f₁ x f₂ x …f_n)(a) = (f₁ (a), f₂ (a), …, f_n (a)) за всяко a  A. Твърдим, че

f₁ x f₂ x …x f_n е непрекъснато.

Доказателство: преди всичко, A₁ x A₂ x …x A_n е декартовото произведение на области на Скот, което дефинирахме по-горе.

Нека a₀  a₁  …е монотонна редица от елементи на A. За всяко i  N

имаме (f₁ x f₂ x …f_n)(a_i) = (f₁ (a_i), f₂ (a_i), …, f_n (a_i)) 

 (f₁ ( ), f₂ ( ), …, f_n ( )) = (f₁ x f₂ x …f_n)( ). Използвали сме, че f₁, …, f_n са монотонни. Така (f₁ x f₂ x …f_n)( ) е горна граница на

редицата { (f₁ x f₂ x …f_n)(a_i) }. Нека b = (b₁, b₂, …, b_n)  A₁ x A₂ x …x A_n е горна граница на тази редица, т.е. (f₁ x f₂ x …f_n)(a_i)  b за всяко i  N.

Тогава за всяко k  N имаме f₁ (a_k) ₁ b₁, f₂ (a_k) ₂ b₂, …, f_n (a_k) _n b_n 

 f₁ ( ) ₁ b₁, f₂ ( ) ₂ b₂, …, f_n ( ) _n b_n, тъй като f₁, …, f_n са непрекъснати. Така (f₁ ( ), f₂ ( ), …, f_n ( ))  b, т.е.

(f₁ x f₂ x …f_n)( )  b и (f₁ x f₂ x …f_n)( ) е точна горна граница на редицата { (f₁ x f₂ x …f_n)(a_i) }.
Нека 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.

Доказателство: конструираме редица { a_n} от елементи на A с

индукция по n.

База: при n = 0, a₀ = .

Предположение: нека е дефинирано a_n, n  0.

Стъпка: тогава a_n+1 = f (a_n).

Твърдим, че редицата { a_n} е монотонна. Ще покажем това с

индукция по n.

База: при n = 0, a₀ =   a₁.

Предположение: нека a_n  a_n+1, n  0.

Стъпка: тъй като f е монотонно, то f (a_n)  f (a_n+1), т.е. a_n+1  a_n+2.

Нека a = . Твърдим, че a е най-малка квазинеподвижна точка на f.

Действително, f (a) = f ( ) = = .

Имаме  , тъй като е горна граница на редицата { a_n+1}.

Така f (a)  = a  a е квазинеподвижна точка на f.

Нека b  A е квазинеподвижна точка на f, т.е. f (b)  b.

С индукция по n ще покажем, че a_n  b за всяко n  N.

База: при n = 0, a₀ =   b.

Предположение: нека a_n  b, n  0.

Стъпка: тогава a_n+1 = f (a_n)  f (b)  b. Използвали сме, че f е монотонно.

Така a_n  b за всяко n  N  a =  b.

Окончателно, a  A е най-малка квазинеподвижна точка на f.

най-малка квазинеподвижна точка.

Нека A_i = (A_i, _i, _i), i = 1, 2, …, n са области на Скот.

Да означим А = A₁ x A₂ x …x A_n, A = (A, , (₁, ₂, …, _n)).

Нека f_i : A  A_i, i = 1, 2, …, n са тотални изображения.

Съвпкупността от формалните равенства

f₁ (₁, ₂, …, _n) = ₁

f₂ (₁, ₂, …, _n) = ₂

…

f₃ (₁, ₂, …, _n) = _n

Казваме, че (a₁, a₂, …, a_n)  A е решение на системата, ако

f_i (a₁, a₂, …, a_n) = a_i за всяко i = 1, 2, …, n.

Казваме, че (a₁, a₂, …, a_n)  A е най-малко решение на системата,

ако (a₁, a₂, …, a_n) е решение на системата и за всяко решение

(b₁, b₂, …, b_n)  A на системата имаме (a₁, a₂, …, a_n)  (b₁, b₂, …, b_n).

Естествено, ако системата има най-малко решение, то е единствено.

Казваме, че (a₁, a₂, …, a_n)  A е квазирешение на системата, ако

f_i (a₁, a₂, …, a_n) _i a_i за всяко i = 1, 2, …, n.

Казваме, че (a₁, a₂, …, a_n)  A е най-малко квазирешение на системата,

ако (a₁, a₂, …, a_n) е квазирешение на системата и за всяко квазирешение

(b₁, b₂, …, b_n)  A на системата имаме (a₁, a₂, …, a_n)  (b₁, b₂, …, b_n).

Естествено, ако системата има най-малко квазирешение,

то е единствено.

Доказателство: да означим f = f₁ x f₂ x …x f_n. Тогава f : A  A и f е непрекъснато изображение, тъй като f₁, f₂, …, f_n са непрекъснати.

От теоремата на Кнастер-Тарски f притежава най-малка неподвижна точка, която е и най-малка квазинеподвижна точка. Да я означим с

(a₁, a₂, …, a_n)  A. Ще покажем, че (a₁, a₂, …, a_n) е най-малко решение на системата. Имаме f (a₁, a₂, …, a_n) = (f₁ (a₁, …, a_n), f₂ (a₁, …, a_n),

…, f_n (a₁, a₂, …, a_n)) = (a₁, a₂, …, a_n), така че f_i (a₁, …, a_n) = a_i за всяко

i = 1, 2, …, n. Така (a₁, …, a_n) е решение на системата. Нека (b₁, …, b_n)  A е решение на системата, т.е. f_i (b₁, …, b_n) = b_i за всяко i = 1, 2, …, n.

Тогава f (b₁, …, b_n) = (b₁, …, b_n), така че (b₁, …, b_n) е неподвижна

точка на f  (a₁, …, a_n)  (b₁, …, b_n).

Аналогично, като се използва, че (a₁, …, a_n) е най-малка квазинеподвижна точка на f се показва, че (a₁, …, a_n) е

най-малко квазирешение на системата за f₁, …, f_n.

Имаме, че (a₁, …, a_n) = , където d₀ = (₁, ₂, …, _n), d_k+1 = f (d_k),

d_k  A за всяко k  N. Да означим а_i⁰ = _i, i = 1, 2, …, n, за всяко k  N (индуктивно) a_i^k+1 = f_i (a₁^k, a₂^k, …, a_n^k), i = 1, 2, …, n.

Твърдим, че d_k = (a₁^k, a₂^k, …, a_n^k) за всяко k  N.

База: при k = 0, d₀ = (₁, ₂, …, _n) = (a₁⁰, a₂⁰, …, a_n⁰).

Предположение: нека d_k = (a₁^k, a₂^k, …, a_n^k), k  0.

Стъпка: тогава d_k+1 = f (d_k) = (f₁ x f₂ x …x f_n)(a₁^k, a₂^k, …, a_n^k) =

= (f₁ (a₁^k, a₂^k, …, a_n^k), f₂ (a₁^k, a₂^k, …, a_n^k), …, f_n (a₁^k, a₂^k, …, a_n^k)) =

= (a₁^k+1, a₂^k+1, …, a_n^k+1).

Сега получаваме (a₁, …, a_n) = =

= , т.е. a_i = , i = 1, 2, …, n.

Използвали сме твърдението за точна горна граница на монотонна редица в декартово произведение на области на Скот.

два типа данни: Nat и Bool. Nat са естествените числа, в Bool има две стойности tt - истина и ff - лъжа. Ще считаме, че разполагаме с определен набор от основни операции oт следните видове:

1. 
   операции f : Natⁿ  Nat, n  1, например събиране (+),
   

1. 
   операции f : Natⁿ  Bool, n  1, например равенство (=), различните видове неравенства (<, <=, >, >=) и т.н.;
   
2. 
   операции f : Boolⁿ  Bool, n  1, например конюнкция (&), дизюнкция (), отрицание () и т.н.
   

Синтактичните елементи на езика са следните:

1. 
   константи от тип Nat и Bool за означаване на елементи
   

1. 
   символи за основните операции;
   
2. 
   обектови променливи, които ще означаваме с главните букви
   

1. 
   функционални променливи, които ще означаваме с F_kⁿ, където k е индекс; променливата F_kⁿ ще приема стойност частична функция, n указва броят на аргументите на функцията;
   
2. 
   точки, запетаи, скоби, чрез които ще постигаме еднозначен синтактичен анализ.
   

Дефинираме индуктивно понятието терм от тип Nat.

База:

1. 
   Всяка константа от тип Nat е терм от тип Nat.
   
2. 
   Всяка обектова променлива е терм от тип Nat.
   

Стъпка:

1. 
   Ако f : Natⁿ  Nat е основна операция, то f (₁, ₂, …, _n) е терм от тип Nat.
   
2. 
   Ако F_kⁿ е функционална променлива, то F_kⁿ (₁, ₂, …, _n) е терм от тип Nat. Тези термове от тип Nat наричаме обръщения към функции.
   

Дефинираме индуктивно понятието терм от тип Bool.

База:

1. 
   Всяка константа от тип Bool е терм от тип Bool.
   
2. 
   Ако f : Natⁿ  Bool е основна операция и ₁, ₂, …, _n са термове от тип Nat, то f (₁, ₂, …, _n) е терм от тип Bool.
   

Стъпка:

1. 
   Ако f : Boolⁿ  Bool е основна операция, то f (₁, ₂, …, _n) е терм от тип Bool.
   

Дефинираме понятието условен терм. Нека  е терм от тип Bool,

₁, ₂ са термове от тип Nat. Тогава if  then ₁ else ₂ е условен терм.
По-нататък, под терм ще разбираме кой да е от трите вида термове.
Ясно е, че ако  е терм, то в  участват краен брой обектови и функционални променливи. Ще използваме означението

 (X₁, …, X_n, , , …, ) за да укажем, че обектовите променливи на  са сред X₁, …, X_n, а функционалните променливи на  са сред

Означаваме с  (X₁/₁, X₂/₂, …, X_n/_n, F) термът, който се получава от  чрез едновременно заместване на всяка от обектовите променливи

X₁, …, X_n с термовете ₁, …, _n съответно. Понякога ще използваме съкратен запис  (X/, F).
Термове, в които не участват обектови променливи ще наричаме функционални термове. Естествено, в горните означения, ако термовете ₁, …, _n са функционални, то  (X/, F) също е функционален терм.
Термове, в които не участват никакви променливи ще наричаме основни термове.
Програма е синтактичен обект R от следния вид:

₀ (X₁, …, X_n, , , …, ), where

…

(X₁, …, ) = _k (X₁, …, , , , …, )

Тук ₀ е терм от тип Nat, който наричаме