Денотационная семантика, доказывающие, что неподвижная точка результаты итераций в наименьшей неподвижной точки

Question

я работаю через в Haskell wikibook раздел на denotational semantics и я отчасти застрял на этом упражнении:

Докажите, что в неподвижной точке полученный с помощью итерации с фиксированной точкой, начиная с с , также является наименьшим, что меньше, чем любая другая фиксированная точка . (Подсказка: - это наименьший элемент нашего cpo и g - монотонный).

Если следующие утверждения определяют ядро ​​понятий, ведущих к осуществлению (я думаю):

где е является факторный функции и показана как неподвижная точка g, так как g непрерывна.

Я думаю, что в основном понимаю часть, где показано, что g (f) = f, но я действительно не знаю, что делать с упражнением. Из того, что я понимаю, факториальная функция f является наименее фиксированной точкой (наименее основанной на операторе ), но мне совершенно не ясно, что означает (интуитивно) сравнивать функции с , не говоря уже о том, как я найду фиксированные точки, отличные от наименее фиксированной точки, показанной в примере.

Я понимаю, что меньше, чем все остальное, и я понимаю, что поскольку g (x) монотонно, если я применяю его к двум вещам, где один меньше другого, результаты будут по-прежнему подчиняться этому упорядочению.

Я думаю, что я бы начал доказательство с помощью некоторой функции f 'и предположения . Если это так, то через монотонное свойство g можно показать, что . Если я тогда смогу показать, что g (f ') = g (f) или f' = f, я думаю, что доказательство завершено, но я не знаю, как это показать.

Answer 1

Позвольте x быть верхней/нижней границей последовательности bot, g(bot), g(g(bot)), .... Пусть y - любая фиксированная точка g (монотонная). Мы хотим доказать, что x <= y.

По индукции по количеству итераций легко видеть, что каждый элемент в последовательности равен <= y. Действительно, это тривиально выполняется для bot, и если z является <= y монотонностью, мы получаем g(z) <= g(y) = y.

Таким образом, y является верхней границей последовательности. Но x является наименее, поэтому x <= y. QED.