Толкование через наименьшую неподвижную точку

Наряду с индуктивным толкованием рекурсивное объявление функции

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)iN

f = suр{fi: i

 N},

где

f0(х) =

, fi+1 = [fi], т е. справедливо

fix

 = suр{i[f0]: i N},

причем

i обозначает i-кратную функциональную композицию функционала  с самим собой.

Содержание раздела

---

---