Полный частичный заказ

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

• 1 Определения
• 2 Примеры
• 3 Свойства
• 4 Непрерывные функции и фиксированные точки
• 5 См. Также
• 6 Примечания
• 7 Ссылки

A полный частичный порядок сокращенный cpo может, в зависимости от контекста, обратитесь к любому из следующих понятий.

• Частично упорядоченный набор является направленным-полным частичным порядком (dcpo ), если каждое из его направленных подмножеств имеет супремум. Подмножество частичного порядка считается направленным, если оно не пусто и каждая пара элементов имеет верхнюю границу в подмножестве. В литературе dcpos иногда также встречается под меткой up-complete poset .

• Частично упорядоченный набор - это направленный-полный частичный порядок с точками, если это dcpo с наименьшим элементом. Иногда их сокращают cppo s.

• Частично упорядоченный набор - это ω-полный частичный порядок (ω-cpo ), если это такой набор, в котором каждая ω-цепь (x 1≤x2≤x3≤x4≤...) имеет супремум, который принадлежит нижележащему набору чугуна. Каждый dcpo является ω-cpo, поскольку каждая ω-цепь является направленным множеством, но обратное неверно. Однако каждый ω-cpo с базисом также является dcpo (с тем же базисом). Ω-cpo (dcpo) с базисом также называется непрерывным ω-cpo (непрерывным dcpo).

Обратите внимание, что полный частичный порядок никогда не используется для обозначения poset, в котором все подмножества имеют верхнюю границу ; для этого понятия используется терминология полная решетка.

Требование существования направленных супремумов может быть мотивировано просмотром направленных множеств как обобщенных аппроксимационных последовательностей и супремумов как пределов соответствующих (аппроксимативных) вычислений. Эта интуиция в контексте денотационной семантики была мотивацией развития теории предметной области.

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

• Каждый конечный ч.у.м. направлен полным.
• Все полные решетки также направлены полными.
• Для любого ч.у. набор, набор все непустые фильтры, упорядоченные по включению подмножества, являются dcpo. Вместе с пустым фильтром также указывается. Если в заказе двоичный код соответствует, то эта конструкция (включая пустой фильтр) фактически дает полную решетку.
• Набор всех частичных функций на некотором заданном наборе S можно упорядочить, определяя f ≤ g для функций f и g тогда и только тогда, когда g расширяет f, то есть если область определения f является подмножеством области определения g и значения f и g согласованы на всех входах, для которых обе функции определены. (Эквивалентно, f ≤ g тогда и только тогда, когда f ⊆ g, где f и g отождествлены с их соответствующими графиками.) Этот порядок является заостренным dcpo, где наименьшим элементом является нигде не определенная функция (с пустой домен). Фактически, ≤ также является ограниченно полным. Этот пример также демонстрирует, почему не всегда естественно иметь самый большой элемент.
• Порядок специализации любого трезвого пространства - это dcpo.
• Давайте использовать термин «дедуктивная система » как набор предложений, замкнутых по следствию (для определения понятия следствия воспользуемся, например, алгебраическим подходом Альфреда Тарского ). Есть интересные теоремы, которые касаются набора дедуктивных систем, являющихся направленно-полным частичным упорядочением. Кроме того, набор дедуктивных систем может быть выбран так, чтобы иметь наименьший элемент естественным образом (так, чтобы он также мог быть заостренным dcpo), потому что набор всех следствий пустого набора (то есть «набор логически доказуемых / логически правильные предложения ») является (1) дедуктивной системой (2), содержащейся во всех дедуктивных системах.

Упорядоченное множество P является указанным dcpo тогда и только тогда, когда каждая цепочка имеет верхнюю грань в P, т. Е. P является полной цепочкой. В качестве альтернативы упорядоченный набор P является заостренным dcpo тогда и только тогда, когда каждое сохраняющее порядок собственное отображение P имеет как минимум фиксированную точку. Каждое множество S можно превратить в заостренный dcpo, добавив наименьший элемент ⊥ и введя плоский порядок с ⊥ ≤ s и s ≤ s для каждого s ∈ S и никаких других отношений порядка.

Функция f между двумя dcpos P и Q называется (Скотт) непрерывной, если она отображает направленные множества к направленным множествам, сохраняя при этом их супрему:

• $f\; (D)\; \subseteq \; Q\; \{\backslash \; displaystyle\; f\; (D)\; \backslash \; substeq\; Q\}$направлено для каждого направленного $D\; \subseteq \; P\; \{\backslash \; displaystyle\; D\; \backslash \; subteq\; P\}$.
• $f\; (sup\; D)\; =\; sup\; f\; (D)\; \{\backslash \; displaystyle\; f\; (\backslash \; sup\; D)\; =\; \backslash \; sup\; f\; (D)\}$для каждого направленного $D\; \subseteq \; P\; \{\; \backslash \; displaystyle\; D\; \backslash \; substeq\; P\}$.

Обратите внимание, что каждая непрерывная функция между dcpos является монотонной функцией. Это понятие непрерывности эквивалентно топологической непрерывности, индуцированной топологией Скотта.

. Множество всех непрерывных функций между двумя dcpos P и Q обозначается [P → Q]. Оборудованный точечным порядком, это снова dcpo, и cpo, если Q является cpo. Таким образом, полные частичные порядки с непрерывными по Скотту отображениями образуют декартову замкнутую категорию.

. Каждое сохраняющее порядок отображение себя f cpo (P, ⊥) имеет наименьшую неподвижную точку. Если f непрерывно, то эта неподвижная точка равна верхней грани итераций (⊥, f (⊥), f (f (⊥)),… f (⊥),…) из ⊥ ( см. также теорему Клини о неподвижной точке ).

Направленная полнота по-разному связана с другими понятиями полноты, такими как полнота цепи. Сама по себе направленная полнота является довольно основным свойством, которое часто встречается в других теоретико-порядковых исследованиях, использующих, например, алгебраические позы и топологию Скотта.

1. ^Абрамский S, Габбай Д.М., Майбаум Т.С. (1994). Справочник по логике в компьютерных науках, том 3. Oxford: Clarendon Press. Prop 2.2.14, pp. 20. ISBN 9780198537625.
2. ^Тарский, Альфред: Bizonyítás és igazság / Válogatott tanulmányok. Gondolat, Budapest, 1990. (Название означает: Доказательство и истина / Избранные статьи.)
3. ^Стэнли Н. Беррис и Х.П. Санкаппанавар: Курс универсальной алгебры
4. ^См. Онлайн на стр. 24 упражнения 5–6 из §5 в BurSan: UnivAlg. Или, на бумаге, см. Tar: BizIg.
5. ^Марковский, Джордж (1976), «Цепно-полные множества и направленные множества с приложениями», Algebra Universalis, 6 (1): 53– 68, doi : 10.1007 / bf02485815, MR 0398913.
6. ^Барендрегт, Хенк, Лямбда-исчисление, его синтаксис и семантика Архивировано 23 августа 2004 г. в Wayback Machine, Северная Голландия (1984)
7. ^См. теорема Кнастера – Тарского ; Основы проверки программ, 2-е издание, Жак Лоэккс и Курт Сибер, John Wiley Sons, ISBN 0-471-91282-4, Глава 4; теорема Кнастера – Тарского, сформулированная над cpo, дается для доказательства в виде упражнения 4.3-5 на стр. 90.

• Davey, B.A.; Пристли, Х.А. (2002). Введение в решетки и порядок (Второе изд.). Издательство Кембриджского университета. ISBN 0-521-78451-4.