Теорема Клини о неподвижной точке - Kleene fixed-point theorem

Вычисление наименьшей фиксированной точки f ( x ) = 1 / 10 x ² + atan ( x ) +1, используя теорему Клини в вещественном интервале [0,7] с обычным порядком

В математических областях порядка и решетка теории , то теорема Клини о неподвижной точке , названной в честь американского математика Клини , утверждает следующее:

Теорема Клини о неподвижной точке. Предположим, что это направленно-полный частичный порядок (dcpo) с наименьшим элементом, и пусть это непрерывная по Скотту (и, следовательно, монотонная ) функция . Тогда имеет наименьшую неподвижную точку , которая является верхней гранью восходящей цепочки Клини ${\ displaystyle (L, \ sqsubseteq)}$${\ displaystyle f: L \ to L}$${\ displaystyle f}$${\ displaystyle f.}$

По возрастанию клиниевская цепь из F представляет собой цепь

${\ Displaystyle \ бот \ sqsubseteq е (\ бот) \ sqsubseteq е (е (\ бот)) \ sqsubseteq \ cdots \ sqsubseteq f ^ {n} (\ бот) \ sqsubseteq \ cdots}$

полученный переборе е на наименьшего элемента ⊥ из L . Выраженная в формуле, теорема утверждает, что

${\ displaystyle {\ textrm {lfp}} (е) = \ sup \ left (\ left \ {f ^ {n} (\ bot) \ mid n \ in \ mathbb {N} \ right \} \ right)}$

где обозначает наименьшую неподвижную точку. ${\ displaystyle {\ textrm {lfp}}}$

Хотя теорема Тарского о неподвижной точке не рассматривает, как неподвижные точки могут быть вычислены путем итерации f из некоторого начального числа (также это относится к монотонным функциям на полных решетках ), этот результат часто приписывается Альфреду Тарски, который доказывает его для аддитивных функций. Теорема о неподвижной точке может быть расширена до монотонных функций с помощью трансфинитных итераций.

Доказательство

Сначала мы должны показать, что восходящая цепочка Клини существует в . Чтобы показать это, мы докажем следующее: ${\ displaystyle f}$${\ displaystyle L}$

Лемма. Если это DCPO с наименьшим элементом и непрерывно по Скотту, то ${\ displaystyle L}$${\ displaystyle f: L \ to L}$${\ Displaystyle е ^ {п} (\ бот) \ sqsubseteq е ^ {п + 1} (\ бот), п \ в \ mathbb {N} _ {0}}$

Доказательство. Воспользуемся индукцией:

• Предположим, что n = 0. Тогда, поскольку - наименьший элемент. ${\ Displaystyle е ^ {0} (\ бот) = \ бот \ sqsubseteq е ^ {1} (\ бот),}$${\ displaystyle \ bot}$
• Предположим, что n> 0. Тогда мы должны это показать . Переставляя, мы получаем . По предположению индукции мы знаем, что это верно, и поскольку f монотонен (свойство непрерывных по Скотту функций), результат также верен. ${\ Displaystyle е ^ {п} (\ бот) \ sqsubseteq е ^ {п + 1} (\ бот)}$${\ Displaystyle е (е ^ {п-1} (\ бот)) \ sqsubseteq е (е ^ {п} (\ бот))}$${\ Displaystyle е ^ {п-1} (\ бот) \ sqsubseteq е ^ {п} (\ бот)}$

Следствием леммы является следующая направленная ω-цепь:

${\ displaystyle \ mathbb {M} = \ {\ bot, f (\ bot), f (f (\ bot)), \ ldots \}.}$

Из определения dcpo следует, что он имеет супремум, назовите его. Теперь остается показать, что это наименьшая неподвижная точка. ${\ Displaystyle \ mathbb {M}}$${\ displaystyle m.}$${\ displaystyle m}$

Во- первых, мы покажем , что является фиксированной точкой, т.е. . Потому что это Скотт-непрерывен , , то есть . Кроме того , так и потому , что не имеет никакого влияния в определении супремуму мы имеем: . Отсюда следует, что , делая фиксированную точку . ${\ displaystyle m}$${\ Displaystyle f (m) = m}$${\ displaystyle f}$${\ Displaystyle е (\ sup (\ mathbb {M})) = \ sup (е (\ mathbb {M}))}$${\ Displaystyle е (м) = \ sup (е (\ mathbb {M}))}$${\ Displaystyle \ mathbb {M} = е (\ mathbb {M}) \ чашка \ {\ bot \}}$${\ displaystyle \ bot}$${\ Displaystyle \ sup (е (\ mathbb {M})) = \ sup (\ mathbb {M})}$${\ Displaystyle f (m) = m}$${\ displaystyle m}$${\ displaystyle f}$

Доказательство того, что на самом деле наименьшая фиксированная точка, может быть выполнено, показав, что любой элемент в меньше, чем любая фиксированная точка (потому что по свойству supremum , если все элементы набора меньше, чем элемент, то также меньше чем тот же элемент ). Это делается по индукции: Предположим, что это некоторая неподвижная точка . Докажем теперь индукцией по этому . База индукции, очевидно, верна: так как является наименьшим элементом . В качестве предположения индукции мы можем предположить, что . Теперь мы делаем шаг индукции: исходя из предположения индукции и монотонности (опять же, подразумеваемой непрерывностью по Скотту ), мы можем сделать следующий вывод: теперь, исходя из предположения, что это неподвижная точка, мы знаем, что и из что мы получаем ${\ displaystyle m}$${\ Displaystyle \ mathbb {M}}$${\ displaystyle f}$${\ Displaystyle D \ substeq L}$${\ displaystyle L}$${\ Displaystyle \ sup (D)}$${\ displaystyle L}$${\ displaystyle k}$${\ displaystyle f}$${\ displaystyle i}$${\ Displaystyle \ forall я \ в \ mathbb {N}: е ^ {я} (\ бот) \ sqsubseteq k}$${\ Displaystyle (я = 0)}$${\ displaystyle f ^ {0} (\ bot) = \ bot \ sqsubseteq k,}$${\ displaystyle \ bot}$${\ displaystyle L}$${\ Displaystyle е ^ {я} (\ бот) \ sqsubseteq k}$${\ displaystyle f}$${\ displaystyle f}$${\ displaystyle f ^ {i} (\ bot) \ sqsubseteq k ~ \ подразумевает ~ f ^ {i + 1} (\ bot) \ sqsubseteq f (k).}$${\ displaystyle k}$${\ displaystyle f,}$${\ Displaystyle е (к) = к,}$${\ Displaystyle е ^ {я + 1} (\ бот) \ sqsubseteq к.}$

Смотрите также

• Другие теоремы о неподвижной точке

Рекомендации