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

А₁ A₂ⁱ C₂ⁱ ‡ g f₁ } f_i b ₁ ,.., b _n a₁ ,.., a_n a₁ f₁ } b ‡ a_к a₁ }₁a₂}₁... }₁a_к }₁... h= g⁰ f h а¹ g А₃ А₂ А₁ f yхy N В Nⁿ N ⁿ " $ x ^k F _mk N ⁿ c₁ (yхy, y vy) v¹ ,..., v^к € x₁

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

Свойството Р наричаме непрекъснато ако при всеки избор на монотонно растяща редица _b₀ _, _b ₁ _,...от елементи на А е в сила импликацията "r(Р(_b_r _)Р(_b_r _)).Нека f_i :А А_i ,i=1,,k,са непрекъснати изображения и yаy= a₁ ,.., a_к е минималното решение на системата f_i (Х₁ ,.., Х_к )= Х_i , i=1,...,к.Нека Р е непрекъснато свойство Р(), където е минималният елемент на А ,и при всеки избор на _b _ А е в сила импликацията Р(_b_)Р(f₁ (_b_),..., f_к (_b_)) .Тогава Р(_а_).Нека g₁ и g₂ са непрекъснати изображения на А в А.Тогава свойството

Р(_b_)=

Tt, ako g1(_b_) } g2 (_b_), Ff в противен случай |

е непрекъснато.Конюнкция на непрекъснати свойства е непрекъснато свойство.Нека разгледаме рекурсивната програма R:

c₀ (Х₁,..., Х_n ,F₁^m1 ,, F_k^mk ), where

F_i^mi (Х₁,..., Х_mi )= c_i (Х₁ ,, Х_mi , F₁^m1 ,, F_k^mk),i=1,..,k.

В зависимост от начина на предаване на параметрите имаме две семантики D_v (R) и D_n (R) на R.Да вземем например едно условие за частична коректност Р:{tt,ff} от вида Р(f) " yаy(! f (yаy)^I(yаy)О(yаy, f_i(yаy))).Да предположим първо че желаем да покажем Р за D_v (R).За целта разглеждаме свойството Р_{1 :} F{tt,ff}, дефинирано с еквивалентността Р₁ (yx y) " yаy(! c₀ (yаy,yx y)^(yаy)О(yаy,c₀ (yаy,yx y))).

Свойството Р₁ е непрекъснато.

Нека _x₀_,_x₁_,... е монотонно растяща редица от елементи F с точна горна граница yx y и нека Р₁ приема стойност tt за всеки член на редицата.Да фиксираме елементът yаy на N ⁿ и да предположим че (yаy) и ! c₀ (yаy, yx y).Намираме член _x_к_ на редицата такъв че c₀ (yаy yx y ) c₀ (yаy,_x_к_).Тъй като Р₁ (_x_к_)=tt имаме О(yаy,c₀ (yаy,_x_к_)),откъдето веднага следва и О(yаy,c₀ (yаy,_x_)).Нека yvy= v₁ ,..., v_к е минимално решение на системата съответно на R в F.От дефиницията на D_v (R) веднага следва че Р(D_v (R)) Р₁ (yvy).За да покажем верността на Р(D_v (R)) можем да използваме правилото на Скот приложено за условието Р₁ и системата съответно на R в областта F.При прилагането на това правило понякога се налага усилим Р₁ ,добавяйки допълнителни условия за частична коректност описващи свойствата на функциите v₁ ,..., v_к .Проблемът за намиране на подходящи допълнителни условия е сходен с този за намиране на подходящ инвариант на цикъл при използването на метода на Флойд за доказателство на коректност на блок-схеми.НЕка R₁ е рекурсивната програма:

F₁ (Х) where

F₁ (Х)=if Х=0 then 1 else F₁ (Х-1)+ F₂ (Х-1)

F₂ (Х)= if Х=0 then 0 else F₂ (Х+1).

Ще покажем че "а(!D_v (R₁)(а) D_v (R)(а) 1).

Разглеждаме условията Р₁ (x₁ , x₂) "а(!x₁ (а) x₁(а) 1),

Р₂ (x₁ , x₂)Ј "а(!x2 (а)ђ x2(а) 0).