Толық ішінара реттелген жиын түрлері

Кіріспе

Математикада "толық бөлшектік рет" термині кем дегенде үш ұқсас, бірақ әртүрлі, жартылай реттелген жиынтар кластарын білдіру үшін қолданылады, олар нақты толықтық қасиеттерімен сипатталады. Толық бөлшектік реттер теориялық информатикада маңызды рөл атқарады: денотациялық семантика және домендер теориясында.

Анықтамалар

Толық ішінара рет термині, қысқартылған cpo, контекстке байланысты бірнеше мағынаға ие болуы мүмкін. Ішінара реттелген жиын, егер оның әрбір бағытталған кіші жиыны жоғары шекке ие болса, толық бағытталған ішінара рет (dcpo) деп аталады. (Ішінара реттің кіші жиыны, егер ол бос емес болса және кіші жиынның ішінде элементтердің әрбір жұбы үшін жоғарғы шек болса, бағытталған болып есептеледі.) Әдебиетте dcpo кейде «жоғарыдан толық позит» деп те аталады. Тік толық бағытталған ішінара рет (тік dcpo, кейде cppo деп қысқартылады) – ең кіші элементі бар dcpo (әдетте символымен белгіленеді). Басқаша айтқанда, тік dcpo-да әрбір бағытталған немесе бос кіші жиынның жоғары шегі болады. «Желілік толық ішінара рет» термині де қолданылады, себебі тік dcpo-лар позит ретінде сипатталады, онда әрбір тізбектің жоғары шегі болады. Бұған ұқсас түсінік – ω толық ішінара рет (ω cpo). Бұл позиттер, онда әрбір ω тізбегінің осы позитке тиесілі жоғары шегі болады. Осы түсінікті тізбектердің басқа кардиналдықтарына да қолдануға болады. Кез келген dcpo – ω cpo, себебі кез келген ω тізбегі бағытталған жиын, бірақ керісінше дұрыс емес. Дегенмен, негізі бар кез келген ω cpo сондай-ақ dcpo болып табылады (сол негізді пайдалана отырып). Негізі бар ω cpo (dcpo) сондай-ақ үздікес ω cpo (немесе үздікес dcpo) деп аталады. Ескеріңіз, толық ішінара рет ешқашан барлық кіші жиындары жоғары шекке ие позитты білдірмейді; осы түсінік үшін «толық тор» терминологиясы қолданылады. Бағытталған жоғары шектердің болуын талап етуге бағытталған жиындарды жалпыланған жуықтау тізбектері ретінде қарау және жоғары шектерді тиісті (жуықтау) есептеулердің лиміттері ретінде қарау себеп болады. Осы интуиция, денотациялық семантика контекстінде, домен теориясын дамытуға түрткіс болды. Бағытталған толық ішінара реттің қарама-қарсы түсінігі – сүзілген толық ішінара рет. Алайда, бұл түсінік практикада жиі кездеспейді, себебі әдетте екілік ретке нақты жұмыс істеуге болады. Дедекинд-МакНейл толықтыруына ұқсас, кез келген ішінара реттелген жиынды ең кіші dcpo-ға дейін бірегей түрде кеңейтуге болады. Дедуктивтік жүйелер жиынының бағытталған толық ішінара реттілік құратыны туралы қызықты теоремалар бар. Сондай-ақ, дедуктивтік жүйелер жиынын табиғи жолмен ең кіші элементі бар етіп таңдауға болады (осылайша ол тік dcpo-да болуы мүмкін), себебі бос жиынның барлық салдары жиыны (яғни «логикалық тұжырымдалған/логикалық жарамды сөйлемдер жиыны») (1) дедуктивтік жүйе (2) барлық дедуктивтік жүйелерге кіреді.

The term complete partial order, abbreviated cpo, has several possible meanings depending on context. A partially ordered set is a directed complete partial order (dcpo) if each of its directed subsets has a supremum. (A subset of a partial order is directed if it is non empty and every pair of elements has an upper bound in the subset.) In the literature, dcpos sometimes also appear under the label up complete poset. A pointed directed complete partial order (pointed dcpo, sometimes abbreviated cppo), is a dcpo with a least element (usually denoted ). Formulated differently, a pointed dcpo has a supremum for every directed or empty subset. The term chain complete partial order is also used, because of the characterization of pointed dcpos as posets in which every chain has a supremum. A related notion is that of ω complete partial order (ω cpo). These are posets in which every ω chain has a supremum that belongs to the poset. The same notion can be extended to other cardinalities of chains. Every dcpo is an ω cpo, since every ω chain is a directed set, but the converse is not true. However, every ω cpo with a basis is also a dcpo (with the same basis). An ω cpo (dcpo) with a basis is also called a continuous ω cpo (or continuous dcpo). Note that complete partial order is never used to mean a poset in which all subsets have suprema; the terminology complete lattice is used for this concept. Requiring the existence of directed suprema can be motivated by viewing directed sets as generalized approximation sequences and suprema as limits of the respective (approximative) computations. This intuition, in the context of denotational semantics, was the motivation behind the development of domain theory. The dual notion of a directed complete partial order is called a filtered complete partial order. However, this concept occurs far less frequently in practice, since one usually can work on the dual order explicitly. By analogy with the Dedekind–MacNeille completion of a partially ordered set, every partially ordered set can be extended uniquely to a minimal dcpo.). There are interesting theorems that concern a set of deductive systems being a directed complete partial ordering. Also, a set of deductive systems can be chosen to have a least element in a natural way (so that it can be also a pointed dcpo), because the set of all consequences of the empty set (i. e. “the set of the logically provable/logically valid sentences”) is (1) a deductive system (2) contained by all deductive systems.

Қасиеттері

Реттелген жиын DCPO болып табылады, егер және тек егер әрбір бос емес тізбектің жоғары шегі болса. Салдарынан, реттелген жиын нүктелік DCPO болып табылады, егер және тек егер әрбір (бос болуы мүмкін) тізбектің жоғары шегі болса, яғни егер және тек егер ол тізбектік толық болса. Дәлелдер таңдау аксиомасына сүйенеді. Балама ретінде, реттелген жиын нүктелік DCPO болып табылады, егер және тек егер оның әрбір ретті сақтайтын өзін-өзі бейнелеуі ең кіші бекітілген нүктеге ие болса.