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

В теории порядка , разделе математики , наименьшая фиксированная точка ( lfp или LFP , иногда также наименьшая фиксированная точка ) функции , из частично упорядоченного набора (для краткости «poset») сама по себе является фиксированной точкой которая меньше каждой другая фиксированная точка, в соответствии с порядком частичного множества. Функция не обязательно должна иметь наименьшую фиксированную точку, но если она есть, то наименьшая фиксированная точка уникальна.

Примеры

При обычном порядке действительных чисел наименьшая неподвижная точка действительной функции f ( x ) = x ² есть x = 0 (поскольку единственная другая неподвижная точка — это 1 и 0 <1). Напротив, f ( x ) = x + 1 вообще не имеет фиксированных точек, поэтому не имеет ни одной минимальной, а f ( x ) = x имеет бесконечно много неподвижных точек, но не имеет ни одной минимальной.

Позволять $G=(V,A)$ быть ориентированным графом и $v$ быть вершиной. Множество вершин , доступных из $v$ можно определить как наименьшую неподвижную точку функции $f:\wp (V)\to \wp (V)$ , определяемый как $f(X)=\{v\}\cup \{x\in V:{\text{ for some }}w\in X{\text{ there is an arc from }}w{\text{ to }}x\}.$ Множество вершин, которые совместно доступны из $v$ определяется аналогичной наименьшей неподвижной точкой. Сильно связная компонента $v$ является пересечением этих двух наименьших неподвижных точек.

Позволять $G=(V,\Sigma ,R,S_{0})$ быть контекстно-свободной грамматикой . Набор $E$ символов, которые создают пустую строку $\varepsilon$ может быть получена как наименьшая неподвижная точка функции $f:\wp (V)\to \wp (V)$ , определяемый как $f(X)=\{S\in V:\;S\in X{\text{ or }}(S\to \varepsilon )\in R{\text{ or }}(S\to S^{1}\dots S^{n})\in R{\text{ and }}S^{i}\in X{\text{, for all }}i\}$ , где $\wp (V)$ обозначает мощности набор $V$ .

Приложения

Многие теоремы о неподвижной точке дают алгоритмы поиска наименьшей неподвижной точки. Наименьшие фиксированные точки часто обладают желаемыми свойствами, которых нет у произвольных фиксированных точек.

Денотационная семантика

Частичный заказ на

\mathbb {Z} _{\bot }

В информатике подход денотационной семантики использует наименьшие фиксированные точки для получения из данного текста программы соответствующей математической функции, называемой ее семантикой. Для этого искусственный математический объект, $\bot$ , обозначает исключительное значение «неопределено». Учитывая, например, тип данных программы int, его математический аналог определяется как $\mathbb {Z} _{\bot }=\mathbb {Z} \cup \{\bot \};$ его делают частично упорядоченным набором, определяя $\bot \sqsubset n$ для каждого $n\in \mathbb {Z}$ и позволяя любым двум разным членам $n,m\in \mathbb {Z}$ быть несравненным в отношении $\sqsubset$ , см. картинку.

Семантика определения программы int f(int n){...} это некоторая математическая функция $f:\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }.$ Если определение программы f не завершается для некоторого ввода n, это можно выразить математически как $f(n)=\bot .$ Множество всех математических функций делается частично упорядоченным путем определения $f\sqsubseteq g$ если для каждого $n,$ отношение $f(n)\sqsubseteq g(n)$ имеет место, то есть, если $f(n)$ менее определен или равен $g(n).$ Например, семантика выражения x+x/x менее определен, чем у x+1, поскольку первое, а не второе, отображает $0$ к $\bot ,$ и они согласны в обратном.

Учитывая некоторый текст программы f, его математический аналог получается как наименьшая неподвижная точка некоторого отображения функций в функции, которое можно получить путем «перевода» f. Например, C определение

int fact(int n) { if (n == 0) return 1; else return n * fact(n-1); }

переводится в отображение

F:(\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot })\to (\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }),

определяется как

(F(f))(n)={\begin{cases}1&{\text{if }}n=0,\\n\cdot f(n-1)&{\text{if }}n\neq \bot {\text{ and }}n\neq 0,\\\bot &{\text{if }}n=\bot .\\\end{cases}}

Отображение $F$ определяется нерекурсивным способом, хотя fact было определено рекурсивно. При определенных ограничениях (см. теорему Клини о неподвижной точке ), которые соблюдены в примере, $F$ обязательно имеет наименьшую неподвижную точку, $\operatorname {fact}$ , то есть $(F(\operatorname {fact} ))(n)=\operatorname {fact} (n)$ для всех $n\in \mathbb {Z} _{\bot }$ . ^[1] Можно показать, что

\operatorname {fact} (n)={\begin{cases}n!&{\text{if }}n\geq 0,\\\bot &{\text{if }}n<0{\text{ or }}n=\bot .\end{cases}}

Большая фиксированная точка $F$ это, например, функция $\operatorname {fact} _{0},$ определяется

\operatorname {fact} _{0}(n)={\begin{cases}n!&{\text{if }}n\geq 0,\\0&{\text{if }}n<0,\\\bot &{\text{if }}n=\bot ,\end{cases}}

однако эта функция неправильно отражает поведение приведенного выше текста программы для отрицательных $n;$ например, звонок fact(-1) вообще не завершится, не говоря уже о возврате 0. Только наименее фиксированная точка, $\operatorname {fact} ,$ может разумно использоваться в качестве семантики математической программы.

Описательная сложность

Иммерман ^[2]^[3] и был ^[4] независимо показал описательной сложности результат , заключающийся в том, что вычислимые за полиномиальное время свойства линейно упорядоченных структур можно определить в FO(LFP) , то есть в логике первого порядка с оператором наименьшей фиксированной точки. размер структуры Однако FO(LFP) слишком слаб, чтобы выразить все свойства неупорядоченных структур с полиномиальным временем (например, четный ).

Наибольшие неподвижные точки

Наибольшую фиксированную точку функции можно определить аналогично наименьшей фиксированной точке, как фиксированную точку, которая больше любой другой фиксированной точки в соответствии с порядком частичного регулирования. В информатике наибольшие фиксированные точки используются гораздо реже, чем наименьшие фиксированные точки. В частности, частично упорядоченные множества, обнаруженные в теории предметных областей, обычно не имеют наибольшего элемента, следовательно, для данной функции может существовать несколько взаимно несравнимых максимальных фиксированных точек, а наибольшая неподвижная точка этой функции может не существовать. Чтобы решить эту проблему, оптимальная фиксированная точка была определена как наиболее определенная фиксированная точка, совместимая со всеми другими фиксированными точками. Оптимальная фиксированная точка всегда существует и является наибольшей фиксированной точкой, если наибольшая фиксированная точка существует. Оптимальная фиксированная точка позволяет формально изучать рекурсивные и корекурсивные функции, которые не сходятся с наименьшей фиксированной точкой. ^[5] К сожалению, хотя теорема Клини о рекурсии показывает, что наименьшая неподвижная точка эффективно вычислима, оптимальная неподвижная точка вычислимой функции может быть невычислимой функцией. ^[6]

См. также

Примечания

^ CA Гюнтер; Д.С. Скотт (1990). «Семантические домены». Ян ван Леувен (ред.). Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 633–674. ISBN 0-444-88074-7 . Здесь: стр. 636–638.
^ Н. Иммерман, Реляционные запросы, вычислимые за полиномиальное время, Information and Control 68 (1–3) (1986) 86–104.
^ Иммерман, Нил (1982). «Реляционные запросы, вычисляемые за полиномиальное время». STOC '82: Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений . стр. 147–152. дои : 10.1145/800070.802187 . Пересмотренная версия в Information and Control , 68 (1986), 86–104.
^ Варди, Моше Ю. (1982). «Сложность реляционных языков запросов». STOC '82: Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений . стр. 137–146. дои : 10.1145/800070.802186 .
^ Шаргеро, Артур (2010). «Оптимальный комбинатор с фиксированной точкой» (PDF) . Интерактивное доказательство теорем . 6172 : 195–210. дои : 10.1007/978-3-642-14052-5_15 . Проверено 30 октября 2021 г.
^ Шамир, Ади (октябрь 1976 г.). Неподвижные точки рекурсивных определений (кандидатская диссертация). Институт науки Вейцмана. OCLC 884951223 . Здесь: Пример 12.1, стр. 12.2–3.

Ссылки

Иммерман, Нил . Описательная сложность , 1999, Springer-Verlag.
Либкин Леонид . Элементы теории конечных моделей , 2004, Springer.

[1] CA Гюнтер; Д.С. Скотт (1990). «Семантические домены». Ян ван Леувен (ред.). Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 633–674. ISBN 0-444-88074-7 . Здесь: стр. 636–638.

[2] Н. Иммерман, Реляционные запросы, вычислимые за полиномиальное время, Information and Control 68 (1–3) (1986) 86–104.

[3] Иммерман, Нил (1982). «Реляционные запросы, вычисляемые за полиномиальное время». STOC '82: Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений . стр. 147–152. дои : 10.1145/800070.802187 . Пересмотренная версия в Information and Control , 68 (1986), 86–104.

[4] Варди, Моше Ю. (1982). «Сложность реляционных языков запросов». STOC '82: Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений . стр. 137–146. дои : 10.1145/800070.802186 .

[5] Шаргеро, Артур (2010). «Оптимальный комбинатор с фиксированной точкой» (PDF) . Интерактивное доказательство теорем . 6172 : 195–210. дои : 10.1007/978-3-642-14052-5_15 . Проверено 30 октября 2021 г.

[6] Шамир, Ади (октябрь 1976 г.). Неподвижные точки рекурсивных определений (кандидатская диссертация). Институт науки Вейцмана. OCLC 884951223 . Здесь: Пример 12.1, стр. 12.2–3.

[1]

[2]

[3]

[4]

[5]

[6]