Семантика на езиците за програмиране 2005/06 - упражнения

Области на Скот

• Област на Скот наричаме тройката $$(A,\leq,\bot)$$, където
  1. А е произволно непразно множество
  2. $$\leq$$ е нестрога частична наредба в A (рефлексивна, транзитивна и антисиметрична релация)
  3. $$\bot$$ е най-малък елемента на A относно наредбата
  4. Всяка монотонно растяща редица a₀,a₁,... от елементи на A има точна горна граница (елемент, който е по-голям от всички елементи на редицата (горна граница) и най-малък от всички такива елементи (точна)).
• Областта на Скот описва алгебричните свойства, които са необходими за развиване на теорията на неподвижната точка
• Изображението f:A₁->A₂ в областите на Скот $$A_1 = (A_1,\leq_1,\bot_1)$$ и $$A_2 = (A_2,\leq_2,\bot_2)$$ наричаме монотонно, ако $$(\forall a,b\in A_1)(a\leq_1 b \Rightarrow f(a)\leq_2 f(b))$$.
• Изображението f:A₁->A₂ в областите на Скот $$A_1 = (A_1,\leq_1,\bot_1)$$ и $$A_2 = (A_2,\leq_2,\bot_2)$$ наричаме непрекъснато, ако за всяка монотонно растяща редица a₀,a₁,... от елементи на A₁ е изпълнено $$f(\bigcup_n(a_n)) = \bigcup_n(f(a_n))$$.
• Неподвижна точка на изображението f:A->A наричаме елемент $$a\in A$$, за който f(a) = a.
• (Теорема на Кнастер-Тарски) Всяко непрекъснато изображение в област на Скот има най-малка неподвижна точка.
• Намиране на неподвижна точка на непрекъснато изображение f:A->A се прави по принципно същния начин, както при $$\mathcal{F}_n$$:
  1. Строят се първите няколко члена на редицата a₀=$$\bot$$, a_n+1 = f(a_n).
  2. Прави се индукционно предположение за общия вид на a_n и се доказва, че a_n+1 е в същия вид.
  3. Неподвижната точка a_f на изображението f е точната горна граница на редицата a₀,a₁,...,a_n,...
• Индукционното правило на Скот може да се прилага за произволни области на Скот във следния вид: Ако P е свойство за елементи на областта на Скот A и f:A->A е непрекъснато изображение с най-малка неподвижна точка a_f и
  1. P($$\bot$$)
  2. ($$\forall$$a$$\in$$A)(P(a)=>P(f(a)))
  3. P е непрекъснато, т.е. за всяка монотонно растяща редица a₀,a₁,...,a_n,... ($$\forall$$n)(P(a_n)) => P($$\bigcup$$a_n)
  то P(a_f) е вярно.
  

Конструкции на области на Скот

• $$\mathcal{F}_n = (\mathcal{F}_n,\subseteq,\emptyset)$$ е област на Скот, където $$\mathcal{F}_n$$ е множеството на всички частични функции в естествените числа на n аргумента с частичната наредба "подфункция" и най-малък елемент никъде недефинираната функция.
• $$P(X) = (2^X,\subseteq,\emptyset)$$ е област на Скот за X - произволно множество.
• Ако $$A_1 = (A_1,\leq_1,\bot_1)$$ и $$A_2 = (A_2,\leq_2,\bot_2)$$ са области на Скот, то декартовото им произведение $$A_1\times A_2 = (A_1 \times A_2,\leq,(\bot_1,\bot_2))$$ е област на Скот, за $$(a_1,a_2)\leq(b_1,b_2) \Longleftrightarrow a_1\leq_1 b_1 \& a_2\leq_2 b_2$$ и $$\Omega(x) = \bot$$. Докажете, че всяка монотонно растяща редица има точна горна граница!
• Ако $$A = (A,\leq,\bot)$$ е област на Скот, а X е произволно множество, а B = { f:X->A } е множеството на всички тотални изображения от X в A, то (B,\subseteq,\Omega) е област на Скот, където $$f\subseteq g \Longleftrightarrow (\forall x\in X)(f(x)\leq g(x))$$. Докажете, че всяка монотонно растяща редица от изображения има точна горна граница!
• Ако $$A_1 = (A_1,\leq_1,\bot_1)$$ и $$A_2 = (A_2,\leq_2,\bot_2)$$ са области на Скот,а B = { f:A₁->A₂ } е множеството на всички непрекъснати тотални изображения от A₁ в A₂, то $$(B,\leq,\Omega)$$ е област на Скот, за $$\leq$$ и $$\Omega$$ дефинирани както в предната точка. Докажете, че всяка монотонно растяща редица има точна горна граница и тя също е непрекъснато изображение, т.е. е от B!

Плоски области на Скот

• Нека D е произволно (непразно) множество, а $$\bot\notin D$$. Нека $$D_\bot = D \cup \{\bot\}$$. Релацията $$\sqsubseteq$$ в $$D\bot$$ дефинирана по следния начин: $$a\sqsubseteq b \Longleftrightarrow a = \bot \vee a = b$$ наричаме плоска наредба в $$D_\bot$$. Специалният елемент $$\bot$$ има смисъл на недефинираност.
• Всяка монотонна растяща редица в $$D_\bot$$ се състои от най-много два различни елемента. По-точно - всички монотонно растящи редици с плоска наредба изглеждат по следния начин:
  1. $$\bot,\bot,...$$
  2. a,a,...
  3. $$\bot,\bot,...,\bot,a,a,...$$
• Тогава всяка монотонно растяща редица в плоска наредба има точна горна граница и тя е този елемент на редицата, който се повтаря безкрайно много пъти от едно място нататък.
• Така получения обект $$(D_\bot,\sqsubseteq,\bot)$$ наричаме плоска област на Скот
• Едно изображение f в плоски области на Скот наричаме точно, ако $$f(\bot) = \bot$$.
• Ако едно изображение в плоска област на Скот е монотонно, то е константно или точно (или и двете)
• Непрекъснатите изображения в плоски области на Скот са точно монотонните изображения
• Множеството $$\mathcal{F}'$$ състоящо се от всички точни тотални изображения $$f:N_\bot\rightarrow N_\bot$$ е област на Скот. Докажете го! Докажете, че тази област на Скот е изоморфна на $$\mathcal{F}$$.
• Множеството $$\mathcal{F}_n^\bot = \{ f:N^n_\bot \rightarrow N_\bot \}$$ от всички тотални функции на n аргумента в плоската област на Скот $$N_\bot$$ е област на Скот. Докажете го!
• Областта на Скот $$\mathcal{F}_n^\bot$$ позволява разглеждането на функции, които дават резултат дори ако някои от аргументите им са недефинирани. Посочете реални примери за това явление от езиците за програмиране!

Задачи

• Стр. 203 / Зад. 10 - намерете точната горна граница на дадените редици
• Стр. 203 / Зад. 11 - кои множества имат точни горни граници?
• Стр. 206 / Зад. 22 - кои функции са монотонни и/или точни?