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

Непрекъснати свойства

• Казваме, че свойството P(f) за функции е непрекъснато, ако за произволна монотонно растяща редица от функции $$f_0\subseteq f_1\subseteq\ldots\subseteq f_n\subseteq\ldots$$, ако свойството е вярно за всеки член на редицата, то то е вярно и за точната й горна граница, т.е. $$(\forall n)(P(f_n)) \Rightarrow P(\bigcup f_n)$$.
• Казваме, че свойството P е условие от тип частична коректност, ако то е от вида $$(\forall x,y)(I(x) \& !f(x)\simeq y \Rightarrow O(x,y))$$. I наричаме входно условие, а O - изходно условие.
• Казваме, че свойството P е условие от тип тотална коректност, ако то е от вида $$(\forall x,y)(I(x) \Rightarrow !f(x)\simeq y \& O(x,y))$$.
• Стр. 190 / Зад. 1 - всяко условие от тип частична коректност е непрекъснато
• Стр. 190 / Зад. 2 - всяко условие от тип тотална коректност е непрекъснато
• Стр. 191 / Зад. 4 - конюнкция на непрекъснати условия е непрекъснато
• Стр. 191 / Зад. 5 - Ако $$\Gamma_1$$ и $$\Gamma_2$$ са непрекъснати оператори, то условията $$\Gamma_1(f)\subseteq\Gamma_2(f)$$ и $$\Gamma_1(f) = \Gamma_2(f)$$ са непрекъснати.

Правило на Скот (за $$\mu$$-индукция)

Нека P(f) е свойства за функции и $$\Gamma$$ е компактен оператор. Правилото на Скот гласи, че ако:

1. P($$\emptyset$$)
2. ($$\forall$$ f)(P(f) => P($$\Gamma$$(f)))
3. P е непрекъснато

то P(f) е вярно за най-малката неподвижна точка на оператора.

Задачи

• Стр. 191 / Зад. 6
• Стр. 192 / Зад. 7
• Стр. 193 / Зад. 12