Конспект установочных лекций по комплексному курсу Информатика, Теория информации
Толкование через наименьшую неподвижную точку
Наряду с индуктивным толкованием рекурсивное объявление функции
fct f = (m x) n: E
можно истолковывать через решение функционального уравнения
(*) f=
[f],
где
было определено выше, т.е. ищут отображение
f: М
N
с тем свойством, что для всех х
М справедливо
f(x) =
[f](х).
Тогда f называют неподвижной точкой
, а (*) - функциональным уравнением,
относящимся к рекурсивному объявлению f. То, что функциональное уравнение всегда обладает решением, будет показано ниже. Для этого понадобятся некоторые теоретические понятия упорядоченности. Функция
f: М
N
называется монотонной,
если для всех х1, х2
М имеет место
xl
x2 => f(xl)
f(х2).
Множество монотонных отображений обозначают через
[М
N].
Для произвольного функционала
не обеспечивается ни существования, ни однозначности неподвижной точки, т.е. решения функционального уравнения. Однако на основе структуры имеющегося ЯП справедливо, что функционал
является монотонным, т.е. для всех функций f и g имеет место
f
g =>
[f]
[g].
Для монотонного функционала
на вполне упорядоченном множестве с наименьшим элементом гарантируется существование неподвижной точки, т.е. решения приведенного выше уравнения (*). Отсюда всегда имеется однозначно определенная наименьшая неподвижная точка
.
Теорема (Knaster-Tarski). Если
- монотонное отображение на вполне упорядоченном множестве А с наименьшим элементом, то уравнение x =
[х] разрешимо и существует однозначно определенная наименьшая неподвижная точка для
.
Лемма Zorn'a. Пусть М - частично упорядоченное множество, которое для каждой цепи В
А содержит также sup В; тогда М обладает максимальным элементом.
Теорема Knaster-Tarski справедлива не только для рекурсивно определенных вычислительных предписаний, но также и для многих других областей информатики и математики.
Теорема (по Клини). Если
непрерывно, то наименьшая неподвижная точка
f для |
[f] совпадает с супремумом цепочки отображений (fi)i
N
f = suр{fi: i
N},
где
f0(х) =
, fi+1 =
[fi], т е. справедливо
fix
= suр{
i[f0]: i
N},
причем
i обозначает i-кратную функциональную композицию функционала
