Введение
В математике фраза «полный частичный порядок» используется для обозначения как минимум трех схожих, но различных классов частично упорядоченных множеств, определяемых конкретными свойствами полноты. Полные частичные порядки играют центральную роль в теоретической информатике, в частности в денотационной семантике и теории областей.
Определения
Термин "полный частичный порядок", сокращенно cpo, имеет несколько возможных значений в зависимости от контекста. Частично упорядоченное множество является направленным полным частичным порядком (dcpo), если каждое его направленное подмножество имеет супремум. (Подмножество частичного порядка называется направленным, если оно не пусто и каждая пара его элементов имеет верхнюю грань в этом подмножестве.) В литературе dcpo иногда также называют up-полным частично упорядоченным множеством. Точечный направленный полный частичный порядок (точечный dcpo, иногда сокращенно cppo) — это dcpo с наименьшим элементом (обычно обозначаемым ⊥). Иными словами, точечный dcpo имеет супремум для каждого направленного или пустого подмножества. Термин "цепочечно полный частичный порядок" также используется, поскольку заостренные dcpo характеризуются как частично упорядоченные множества, в которых каждая цепочка имеет супремум. Связанным понятием является понятие ω-полного частичного порядка (ω cpo). Это частично упорядоченные множества, в которых каждая ω-цепочка имеет супремум, принадлежащий этому множеству. То же понятие можно распространить на другие кардинальности цепочек. Каждый dcpo является ω cpo, поскольку каждая ω-цепочка является направленным множеством, но обратное неверно. Однако каждый ω cpo с базисом также является dcpo (с тем же базисом). ω cpo (dcpo) с базисом также называют непрерывным ω cpo (или непрерывным dcpo). Важно отметить, что термин "полный частичный порядок" никогда не используется для обозначения частично упорядоченного множества, в котором все подмножества имеют супремумы; для этого понятия используется терминология "полная решетка". Требование существования направленных супремумов можно обосновать, рассматривая направленные множества как обобщенные последовательности аппроксимаций, а супремумы — как пределы соответствующих (приблизительных) вычислений. Эта интуиция, в контексте денотационной семантики, послужила мотивацией для развития теории доменов. Двойственное понятие направленного полного частичного порядка называется фильтрованным полным частичным порядком. Однако это понятие встречается в практике гораздо реже, поскольку обычно можно работать с двойственным порядком явно. По аналогии с завершением Дедекинда — Макнейла частично упорядоченного множества, каждое частично упорядоченное множество можно однозначно расширить до минимального dcpo. Существуют интересные теоремы, касающиеся множества дедуктивных систем, являющихся направленным полным частичным порядком. Также множество дедуктивных систем можно выбрать таким образом, чтобы оно имело наименьший элемент естественным образом (и, следовательно, могло быть заостренным dcpo), поскольку множество всех следствий пустого множества (то есть "множество логически доказуемых/логически валидных предложений") является (1) дедуктивной системой и (2) содержится во всех дедуктивных системах.
Характеристики
Упорядоченное множество является dcpo тогда и только тогда, когда каждая непустая цепь имеет супремум. Как следствие, упорядоченное множество является точечным dcpo тогда и только тогда, когда каждая (возможно пустая) цепь имеет супремум, то есть, если и только если оно является цепью-полным. Доказательства опираются на аксиому выбора. Альтернативно, упорядоченное множество является точечным dcpo тогда и только тогда, когда каждое самоотображение, сохраняющее порядок, имеет наименьшую неподвижную точку.