1. Булеви функции. Теорема на Пост-Яблонски за пълнота. Нека J2 = { 0, 1}. Всяка функция f : J2n  J

най-малка квазинеподвижна точка на 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 притежава най-малка квазинеподвижна точка.

Доказателство: Конструираме редица { 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 = 0, a₀ =   b.

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

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

Така a_n  b за всяко 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) = _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_i : A  A_i са непрекъснати изображения. Тогава системата от уравнения за f₁, f₂, …, f_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)) =

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.
Нека  (X₁, …, X_n, , , …, ) е терм.

Нека a₁, a₂, …, a_n  , ₁  , ₂  , …, _k  .

Дефинираме индуктивно понятието стойност на терма  в

a₁, …, a_n, ₁, …, _k, която записваме  (a₁, …, a_n, ₁, …, _k) или

съкратено  (a, ):

1. 
   Ако  = c, то  (a, )  c (съответно булева константа или естествено число).
   
2. 
   Ако  = X_i, то  (a, )  a_i.
   
3. 
   Нека  = f (₁, ₂, …, _l).
   

4. 
   Нека  = if  then ₁ else ₂. Тогава
   

 (a, )  ₂ (a, ), ако  (a, )  ff,

!  (a, ), ако !  (a, ).

5. 
   Нека  = (₁, ₂, …, ).
   

Нека  (X₁, …, X_n, , , …, ) e терм. Нека   F и

c₁, c₂, …, c_n са константи. Тогава  (c, )   (X/c, F)().

Доказателство: Индукция по построението на .

 (a, )  b   (a, )  b.

Доказателство: Индукция по построението на .
Твърдение (за компактност): Нека  (X, F) е терм.

За всеки а  ⁿ,   F и константа b от типа на  е изпълнено:

 (a, )  b  съществуват крайни подфункции   , такива че

 (a, )  b.

Доказателство: Индукция по построението на .

Ако  е константа или  = X_i, i  { 1, 2, …, n }, то можем да изберем

 = (!, !, …, !), където индексът показва броя на аргументите.

Нека  = f (₁, ₂, …, _l) и твърдението е изпълнено за термовете

₁, ₂, …, _l. Нека  (a, )  b. Тогава съществуват константи

c₁, c₂, …, c_l, такива че ₁ (a, )  c₁, ₂ (a, )  c₂, …, _l (a, )  c_l и

f (c₁, c₂, …, c_l) = b. От индукционното предположение съществуват крайни подфункции ₁  , ₂  , …, _l  , такива че

₁ (a, ₁)  c₁, ₂ (a, ₂)  c₂, …, _l (a, _l)  c_l.

Нека ₁ = (₁₁, ₁₂, …, _1k), _1j  _j, j = 1, 2, …, k.

Нека ₂ = (₂₁, ₂₂, …, _2k), _2j  _j, j = 1, 2, …, k.

…

Нека _l = (_l1, _l2, …, _lk), _lj  _j, j = 1, 2, …, k.

²  ₂, …, ^k = _1k  _2k  … _lk, ^k  _k. Нека  = (¹, ², …, ^k).

Тогава    и  са крайни функции. Ясно е, че _i  , i = 1, 2, …, l.

От монотонността получаваме ₁ (a, )  c₁, ₂ (a, )  c₂, …,

_l (a, )  c_l, също f (c₁, c₂, …, c_l) = b   (a, )  b.

Случаят  = if  then ₁ else ₂ се разглежда аналогично на предния случай.

Нека  = (₁, ₂, …, ) и твърдението е изпълнено за термовете ₁, ₂, …, . Нека  (a, )  b.

Тогава съществуват константи c₁, c₂, …, , такива че ₁ (a, )  c₁,

₂ (a, )  c₂, …, (а, )  и _i (c₁, c₂, …, )  b. От индукционното предположение съществуват крайни подфункции ₁  , ₂  , …,   , такива че ₁ (a, ₁)  c₁, ₂ (a, ₂)  c₂, …, (а,  )  .

Нека ₁ = (₁₁, ₁₂, …, _1k), _1j  _j, j = 1, 2, …, k.

Нека ₂ = (₂₁, ₂₂, …, _2k), _2j  _j, j = 1, 2, …, k.

…

Нека  = (, , …, ),   _j, j = 1, 2, …, k.

^k = _1k  _2k  … . Oтново ¹, ², …, ^k са крайни функции и

¹  ₁, ²  ₂, …, ^k  ₁. Нека ^i* = ⁱ  { (c₁, c₂, …, , b) }.

Тогава ^i* е крайна подфункция на _i, тъй като _i (c₁, c₂, …, )  b. Нека  = (¹, …, ^i-1, ^i*, ⁱ⁺¹, …, ^k). Тогава    и  са крайни функции. Естествено, ₁  , ₂  , …,    и от монотонността получаваме, че ₁ (a, )  c₁, ₂ (a, )  c₂, …, (а, )  .

Освен това, ^i* (c₁, c₂, …, )  b   (a, )  b.
Лема: Нека   F_n и  е крайна, { f_k} е монотонно растяща редица от елементи на F_n. Нека   . Тогава съществува m  , такова че   f_m.

Доказателство: Тривиална проверка.

Нека ₀  ₁  … _n  …е монотонно растяща редица от елементи на F. За всеки a  ⁿ и константа b от типа на  имаме

 (a, )  b  съществува n  , такова че  (a, _n)  b.

Доказателство: Нека съществува n  , такова че  (a, _n)  b.

Имаме _n  и от монотонността получаваме  (a, )  b.

Нека  (a, )  b. От твърдението за компактност съществуват крайни подфункции   , такива че  (a, )  b.

Нека  = (₁, ₂, …, _k).

Имаме = .

Тъй като   , то ₁  , ₂  , …, _k  .

Имаме, че ₁, ₂, …, _k са крайни функции и от лемата получаваме, че съществуват n₁, n₂, …, n_k, такива че ₁  , ₂  , …,

_k  . Нека n = max (n₁, n₂, …, n_k).

Тъй като редиците { }, { }, …, { } са монотонни, то ₁  , ₂  , …, _k     _n. Накрая от твърдението за монотонност получаваме  (a, _n)  b.

Дефинираме изображение Г_ : F  по следния начин:

Г_ (₁, ₂, …, _k)(a₁, a₂, …, a_n)   (a₁, …, a_n, ₁, …, _k) за всяко

(a₁, a₂, …, a_n)  ⁿ, (₁, ₂, …, _k)  F.

Доказателство: Непосредствено следствие от твърденията за монотонност и непрекъснатост.

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

Нека Г_i : F  , Г_i = , i = 1, 2, …, k.

Разглеждаме системата за изображенията Г₁, Г₂, …, Г_k:

Г₁ (₁, ₂, …, _k) = ₁

Г₂ (₁, ₂, …, _k) = ₂

…

Г_k (₁, ₂, …, _k) = _k

 = (₁, ₂, …, _k). При това  е и най-малко квазирешение.

Функцията D_V (R) : ⁿ  , дефинирана с D_V (R)(а)  ₀ (а, ) за всяко a  ⁿ, където  е точно това най-малко решение наричаме денотационна семантика на програмата R с предаване по стойност.
Сега ще покажем, че денотационната и операционната семантика съвпадат за всяка програма R.
По-долу с  ще означаваме най-малкото (квази)решение на системата за Г₁, Г₂, …, Г_k.