5.Индукционно правило на Скот.

Правилото на Скот е мошно средство за док. на св/ства на минималните неподвижни точки на компактните оператори. Счита се използването на рекурсията в програмирането е нежелано и опасно по две причини. Първо , рекурсивните програми са трудни за верификация и второ те са твърде неефективни. Всъшност и двете двърдения са напълно погрешни. Сега ще покажем как можем да се справим с първият проблем. Нека Г е компактен оператор от тип (n,n) и f е минималната неподвижна точка на Г. От теоремата на кнастер-Тарски следва че f =U f ^k , където f ₀ = € и f _k+1 =Г(f _k). Нека Р е някакъво свойство на n-местните частични ф-ции, което желаем за f . Да предположим че сме доказали Р(€) и " F_n (Р(g)Р(Г(g))). Оттук с индукцията по к получаваме Р(f _k) за всяко к. Дали е вярно Р(f)?.Следващият пример показва че отговора е не . Нека Г е от тип (1,1) и Г(g)=kх.if х =0 then 1 else g(х - 1)*х. Оператора Г е очевидно компактен. Нека f ₀ } f ₁ }... са апроксиациите на минималната неподвижна точка на Г . С индукцията по к може да се покаже че f _k = kх .if х<к then х! else € (х), откъдето следва че минималната неподвижна точка f=U f _k на Г е kх.х!. Нека Р е свойство на n-местните частични ф-ции. Казваме че Р е непрекъснато ако при всеки избор на монотомнно растяща редица f ₀ } f ₁ }... } f _k }...,такава че Р(f _k) за всяко к е в сила Р(U f _k). Нека n 1. Да разгледаме свойството Р определено чрез формулата Р(f) "yхy(!f(yхy)^I(yхy)O(yхy,f(yхy))), където I(yхy) и O(yхy,у) са произволни предикати в множ. на естествените числа. Свойството от този вид се нарича условие за частична коректност.Условията за частична коректност са по-слаби от условията за тотална коректност, който са от вида Р(f) Џђ"yхy(I(yхy) !f(yхy)^O(yхy,f(yхy))), и утвърждават че при всеки изход удовлетворяващи предиката I, програмата завършва с изход който удовлетворява предиката О. Правилото на Скот е удобно за доказване на частична коректност но е неприложимо при доказване на тотална коректност. Нека Р е условие за частична коректност. Тогава свойството Р е непрекъснато.Условията за частична и тотална коректност са на пръв поглед най-важното което бихме желали да покажем за една програма. От друга страна за да формулираме такива условия трябва да имаме ясна хипотеза за ф-циията която се пресмята от програмата което при сложни или твърди общо зададени програми невинаги е възможно. В такъв случай обикновенно се доказват някой по-общи свойства които без да специфицират докрай входно-изходната релация се оказват полезни при нейния анализ. Ако Г₁ и Г₂ са непрекъснати оператори то свойството Р(g) Џђ Г₁ (g) } Г₂ (g) е непрекъснато. Ако Р₁ и Р₂ са непрекъснати свойства то и свойството Р определено чрез еквивалентността Р(g) Џђ Р₁ (g)^ Р₂ (g), е непрекъснато. Нека Г е непрекъснат оператор от тип (n,n) и Р е непрекъснато свойство. Нека предположим че Р(€) и " g(Р(g)Р(Г(g))). Тогава Р е в сила за минималната неподвижна точка на Г.В литературата са известни многобройни варианти на правилото на Скот.Повечето от тях се основават на конструкцията на минималната неподвижна точка която се дава от теоремата на Кнастер-Тарски.