Наименьшая фиксированная точка, наибольшая фиксированная точка

В CPO (который мы интерпретируем как тип) любая возрастающая цепочка имеет наименьшую верхнюю границу .

Вот пример, который должен передать интуицию, почему в области CPO совпадают наименьшие и наибольшие неподвижные точки. Рассмотрим следующий функтор, злоупотребляя нотацией списка для краткости:

data ListF a x = [] | a : x

Его наибольшая фиксированная точка - это тип списков Haskell (возможно, бесконечный, возможно, частичный). А как насчет его наименее фиксированной точки? В нем должны быть следующие элементы (Fix конструкторы опущены):

0 : _|_
0 : 1 : _|_
0 : 1 : 2 : _|_
...

И они образуют возрастающую цепочку, поэтому должна быть минимальная верхняя граница, которая должна быть бесконечным списком натуральных целых чисел 0 : 1 : 2 : .... Таким образом, наименьшая фиксированная точка ListF содержит бесконечные списки и, следовательно, совпадает с наибольшей фиксированной точкой.

Как было указано в комментариях, утверждение о том, что наибольшая фиксированная точка задается типом [], может нуждаться в пояснении. Например, не станет ли какой-нибудь CPO "BigList" списков, проиндексированных большими порядковыми числами, еще большей фиксированной точкой?

Сначала можно показать, что [] удовлетворяет определению окончательной ListF-коалгебры. Тогда свойство финальных коалгебр состоит в том, что они единственны с точностью до изоморфизма. Следовательно, списки, проиндексированные более крупными порядковыми числами, приведут к неизоморфному CPO, так что это не может быть окончательной коалгеброй.

Я мог бы остановиться на этом, но подождите, разве BigList не является еще большей фиксированной точкой ListF? Мой вывод состоит в том, чтобы списать эту проблему на плохую терминологию, и формально мы должны обсуждать только «окончательные коалгебры», а не «наибольшие фиксированные точки».

В зависимости от того, как вы определяете «фиксированную точку» функтора в CPO и понятия (предварительного) порядка между CPO, вы можете обнаружить, что BigList является фиксированной точкой ListF, что она больше, чем [], что вы столкнетесь с множеством -теоретические парадоксы при достижении «величайшей фиксированной точки», и что в конечном итоге для практиков Haskell нет ничего ценного в этом способе формализации «величайшей фиксированной точки», потому что вы действительно хотели хороших свойств конечной коалгебры.

(Мне было бы интересно узнать о прямом способе определения «фиксированной точки», исключающей BigList как единицу.)

Так что вместо этого термин «наибольшая фиксированная точка» может быть синонимом «окончательной коалгебры». Некоторая интуиция переносится (к «фиксированным точкам» обычно можно подойти с помощью итераций), некоторые - нет (это не «величайший» в теоретико-множественном смысле).