Кіріспе
Бір мезгілдегі шектеулер логикасы бағдарламалауы – шектеулер логикасы бағдарламалауының бір түрі, ол негізінен шектеулерді қанағаттандыру мәселелерін шешуден гөрі (немесе оған қосымша) бір мезгілдегі процестерді бағдарламалауға бағытталған. Шектеулер логикасы бағдарламалаудағы мақсаттар бір мезгілде бағаланады; демек, бір мезгілдегі процесс интерпретатордың мақсатты бағалауы арқылы бағдарламаланады. Синтаксистік тұрғыдан бір мезгілдегі шектеулер логикасы бағдарламалары бір мезгілдегі емес бағдарламаларға ұқсас, бірақ баптарда күзетшілер болады, олар кейбір жағдайларда баптың қолданылуын шектейтін шарттар. Семантикалық тұрғыдан бір мезгілдегі шектеулер логикасы бағдарламалауы, бір мезгілдегі емес нұсқаларынан өзгеше, себебі мақсатты бағалаудың мақсаты проблемаға шешім табу емес, бір мезгілдегі процесті іске асыру болып табылады. Ең маңыздысы, бұл айырмашылық интерпретатордың бірнеше бап қолданылған кезде қалай әрекет ететініне әсер етеді: бір мезгілдегі емес шектеулер логикасы бағдарламалауы барлық баптарды рекурсивті түрде тексерсе, бір мезгілдегі шектеулер логикасы бағдарламалауы тек біреуін таңдайды. Бұл интерпретатордың бағытталғандығының ең айқын көрінісі, ол бұрын жасаған таңдауын ешқашан қайта қарамайды. Бұның басқа да салдары бар, мысалы, бағалау толығымен сәтсіз аяқталмаса да, дәлелдеуге келмейтін мақсаттың болуы мүмкін, сондай-ақ мақсатты және баптың басын салыстырудың ерекше тәсілі. Шектеулерді басқару ережелерін бір мезгілдегі шектеулер логикасын бағдарламалаудың бір түрі деп қарастыруға болады, бірақ олар бір мезгілдегі процестерді емес, шектеулерді жеңілдетуші немесе шешушіні бағдарламалау үшін қолданылады.
Сипаттама
Шектеу логикалық бағдарламалауда ағымдағы мақсаттағы мақсаттар тізбектей бағаланады, көбінесе LIFO тәртібімен, яғни жаңа мақсаттар бірінші бағаланады. Логикалық бағдарламалаудың параллельдік нұсқасы мақсаттарды параллель бағалауға мүмкіндік береді: әрбір мақсат жеке процесспен бағаланады және процестер бір мезгілде орындалады. Бұл процестер шектеулер сақтағышы арқылы өзара әрекеттеседі: бір процесс шектеулер сақтағышына шектеу қоса алады, ал екіншісі сақтағыштағы шектеудің салдары бар-жоғын тексереді. Шектеуді сақтағышқа қосу әдеттегі шектеу логикалық бағдарламалаудағыдай жүзеге асырылады. Шектеудің салдары бар-жоғын тексеру шарттардың күзетшілері арқылы жасалады. Күзетшілер синтаксистік кеңейтуді қажет етеді: параллельді шектеу логикалық бағдарламалау шарты H : G | B түрінде жазылады, мұнда G – шарттың күзетшісі деп аталатын шектеу. Дерексіз айтқанда, осы шарттың жаңа нұсқасы тек қана күзетші шектеуі сақтағышта болған жағдайда ғана, мақсаттағы литералды ауыстыру үшін қолданылуы мүмкін, бұл үшін литерал мен шарт басының теңдеуі сақтағышқа қосылады. Бұл ереженің нақты анықтамасы күрделірек және төменде келтіріледі. Бір мезгілдегі емес және бір мезгілдегі шектеу логикалық бағдарламалау арасындағы басты айырмашылық – біріншісі іздеуге, ал екіншісі параллельді процестерді іске асыруға бағытталған. Бұл айырмашылық таңдауларды кері қайтару мүмкіндігіне, процестердің тоқтауына рұқсат етілмеуіне және мақсаттар мен шарттардың бас жағының теңестірілу жолына әсер етеді. Қалыпты және бір мезгілдегі шектеу логикалық бағдарламалау арасындағы бірінші семантикалық айырмашылық – мақсатты дәлелдеу үшін бірнеше шарт қолданылатын жағдайға қатысты. Бір мезгілдегі емес логикалық бағдарламалау мақсатты қайта жазу кезінде барлық мүмкін шарттарды тексереді: егер мақсатты шарттың жаңа нұсқасының денесімен алмастыру арқылы дәлелдеуге болмаса, басқа шарт дәлелденіп, егер бар болса, қолданылады. Себебі мақсатты дәлелдеу – басты міндет, сондықтан мақсатты дәлелдеудің барлық мүмкін жолдары тексеріледі. Ал бір мезгілдегі шектеу логикалық бағдарламалау параллельді процестерді бағдарламалауға бағытталған. Жалпы, параллельді бағдарламалауда процесс таңдау жасаса, бұл таңдауты кері қайтаруға болмайды. Шектеу логикалық бағдарламалаудың параллельдік нұсқасы процестерге таңдау жасауға мүмкіндік береді, бірақ олар жасағаннан кейін оған міндеттеме алады. Техникалық тұрғыдан алғанда, егер мақсаттағы литералды қайта жазу үшін бірнеше шарт қолданылатын болса, бір мезгілдегі емес нұсқа барлық шарттарды тізбектеп тексереді, ал бір мезгілдегі нұсқа бір ғана кездейсоқ шартты таңдайды: бір мезгілдегі емес нұсқадан айырмашылығы, басқа шарттар ешқашан тексерілмейді. Көптеген таңдауларды басқарудың осы екі әдісі «қандай екенін білмейтін детерминизм» және «қанағаттандыратын детерминизм» деп аталады. Мақсаттағы литералды қайта жазу кезінде қарастырылатын шарттар – шектеу сақтағышының және литералдың шарт басымен теңдеуінің бірігісінен шығатын күзетшісі бар шарттар ғана. Күзетшілер қандай шарттарды мүлдем қарастыруға болмайтынын анықтайды. Бұл, әсіресе, бір мезгілдегі шектеу логикалық бағдарламалаудың бір ғана шартқа міндеттемесін ескере отырып маңызды: шартты бір рет таңдағаннан кейін, бұл таңдау ешқашан қайта қарастырылмайды. Күзетшілер болмаса, интерпретатор литералды қайта жазу үшін «жаман» шартты таңдауы мүмкін, ал басқа «жақсы» шарттар бар. Бір мезгілдегі емес бағдарламалауда бұл кем маңызды, өйткені интерпретатор әрқашан барлық мүмкіндіктерді тексереді. Бір мезгілдегі бағдарламалауда интерпретатор басқаларын сынамай-ақ бір ғана мүмкіндікке міндеттенеді. Бір мезгілдегі емес және бір мезгілдегі нұсқалар арасындағы айырмашылықтың екінші салдары – бір мезгілдегі шектеу логикалық бағдарламалау процестердің тоқтамай жұмыс істеуіне мүмкіндік беру үшін арнайы жасалған. Тоқтамайтын процестер жалпы алғанда, параллельді өңдеуде жиі кездеседі; шектеу логикалық бағдарламалаудың параллельдік нұсқасы оларды сәтсіздік шартын пайдаланбай іске асырады: егер мақсатты қайта жазу үшін ешқандай шарт қолданылмаса, осы мақсатты бағалау процесі тоқтатылады, бұл бүкіл бағалауды бір мезгілдегі емес шектеу логикалық бағдарламалаудағыдай сәтсіздікке ұшыратады. Нәтижесінде, мақсатты бағалау процесі тоқтатылуы мүмкін, өйткені жалғастыру үшін ешқандай шарт жоқ, бірақ сонымен бірге басқа процестер жұмысын жалғастырады. Әр түрлі мақсаттарды шешетін процестердің синхрондалуы күзетшілерді пайдалану арқылы жүзеге асырылады. Егер мақсатты қайта жазу мүмкін болмаса, өйткені қолданылатын барлық шарттардың күзетшісі шектеу сақтағышында болмайды, осы мақсатты шешетін процесс күзетшінің кемінде бір қолданылатын шарттың салдары болуы үшін басқа процестердің қажетті шектеулерді қосуын күтеді. Бұл синхрондалу өлі тұруға бейім: егер барлық мақсаттар тоқтатылса, жаңа шектеулер қосылмайды және демек, ешқандай мақсат ешқашан тоқтатылмайды. Бір мезгілдегі және бір мезгілдегі емес логикалық бағдарламалау арасындағы үшінші айырмашылық – мақсатты шарттың жаңа нұсқасының басымен теңестіру жолында. Операциялық тұрғыдан алғанда, бұл шарт басының айнымалыларын мақсатқа тең болатындай терминдермен теңестіруге болатынын тексеру арқылы жасалады. Бұл ереже шектеу логикалық бағдарламалаудағы сәйкес ережеден айырмашылығы, ол тек айнымалы=термин түріндегі шектеулерді қосуға рұқсат береді, мұнда айнымалы шарт басының бірі болады. Бұл шектеу мақсат пен шарт басын әртүрлі қарастыратын бағыттылықтың бір түрі ретінде қарастырылуы мүмкін. Нақты айтқанда, шарттың жаңа нұсқасы H: G|B мақсатты A қайта жазу үшін қолданылатындығын анықтайтын ереже мынадай: Біріншіден, A мен H бірдей предикатқа ие екені тексеріледі. Екіншіден, қазіргі шектеу сақтағышында берілген A мен H теңестірілуіне болатындығы тексеріледі; қалыпты логикалық бағдарламалаудан айырмашылығы, бұл шарт басының айнымалысы тек терминге тең болатын бір жақты біріктіру арқылы жасалады. Үшіншіден, күзетші шектеу сақтағышынан және екінші қадамда жасалған теңдеулерден шығарылатындығы тексеріледі; күзетші шарт басында көрсетілмеген айнымалыларды қамтуы мүмкін: бұл айнымалылар экзистенциалды түрде түсіндіріледі. Шарттың жаңа нұсқасының мақсатты ауыстыруға қолданылуын шешу әдісін былай қысқаша түсіндіруге болады: қазіргі шектеу сақтағышы шарт басының айнымалыларының және күзетшінің бағалануы бар екенін көрсетеді, сонда шарт басы мақсатқа тең болады және күзетші салдары бар. Іс жүзінде, салдарды тексеру толық емес әдіспен жүзеге асырылуы мүмкін. Параллельді логикалық бағдарламалаудың синтаксисі мен семантикасына қосымша – атомдық хабарлау. Интерпретатор шартты қолданғанда, оның күзетшісі шектеу сақтағышына қосылады. Алайда, дене шектеулері де қосылады. Осы шартқа міндеттеме бергендіктен, интерпретатор дене шектеулері сақтағышпен қайшы болса да кері қайтпайды. Бұл жағдайды атомдық хабарлауды пайдалану арқылы болдырмауға болады, ол шартта «екінші күзетші» түрін қамтитын нұсқа болып табылады, ол тек тұрақтандыру үшін тексеріледі. Мұндай шарт H : G:D | B түрінде жазылады. Бұл шарт тек қана G шектеу сақтағышынан шығарылатын болса және D онымен үйлесімді болса ғана литералды қайта жазу үшін қолданылады. Бұл жағдайда G және D екеуі де шектеу сақтағышына қосылады.
clause: contrary to the non concurrent version, the other clauses will never be tried. These two different ways for handling multiple choices are often called "don't know nondeterminism" and "don't care nondeterminism". When rewriting a literal in the goal, the only considered clauses are those whose guard is entailed by the union of the constraint store and the equation of the literal with the clause head. The guards provide a way for telling which clauses are not to be considered at all. This is particularly important given the commitment to a single clause of concurrent constraint logic programming: once a clause has been chosen, this choice will be never reconsidered. Without guards, the interpreter could choose a "wrong" clause to rewrite a literal, while other "good" clauses exist. In non concurrent programming, this is less important, as the interpreter always tries all possibilities. In concurrent programming, the interpreter commits to a single possibility without trying the other ones. A second effect of the difference between the non concurrent and the concurrent version is that concurrent constraint logic programming is specifically designed to allow processes to run without terminating. Non terminating processes are common in general in concurrent processing; the concurrent version of constraint logic programming implements them by not using the condition of failure: if no clause is applicable for rewriting a goal, the process evaluating this goal stops instead of making the whole evaluation fail like in non concurrent constraint logic programming. As a result, the process evaluating a goal may be stopped because no clause is available to proceed, but at the same time the other processes keep running. Synchronization among processes that are solving different goals is achieved via the use of guards. If a goal cannot be rewritten because all clauses that could be used have a guard that is not entailed by the constraint store, the process solving this goal is blocked until the other processes add the constraints that are necessary to entail the guard of at least one of the applicable clauses. This synchronization is subject to deadlocks: if all goals are blocked, no new constraints will be added and therefore no goal will ever be unblocked. A third effect of the difference between concurrent and non concurrent logic programming is in the way a goal is equated to the head of a fresh variant of a clause. Operationally, this is done by checking whether the variables in the head can be equated to terms in such a way the head is equal to the goal. This rule differs from the corresponding rule for constraint logic programming in that it only allows adding constraints in the form variable=term, where the variable is one of the head. This limitation can be seen as a form of directionality, in that the goal and the clause head are treated differently. Precisely, the rule telling whether a fresh variant H: G|B of a clause can be used to rewrite a goal A is as follows. First, it is checked whether A and H have the same predicate. Second, it is checked whether there exists a way for equating with given the current constraint store; contrary to regular logic programming, this is done under one sided unification, which only allows a variable of the head to be equal to a term. Third, the guard is checked for entailment from the constraint store and the equations generated in the second step; the guard may contain variables that are not mentioned in the clause head: these variables are interpreted existentially. This method for deciding the applicability of a fresh variant of a clause for replacing a goal can be compactly expressed as follows: the current constraint store entails that there exists an evaluation of the variables of the head and the guard such that the head is equal to the goal and the guard is entailed. In practice, entailment may be checked with an incomplete method. An extension to the syntax and semantics of concurrent logic programming is the atomic tell. When the interpreter uses a clause, its guard is added to the constraint store. However, also added are the constraints of the body. Due to commitment to this clause, the interpreter does not backtrack if the constraints of the body are inconsistent with the store. This condition can be avoided by the use of atomic tell, which is a variant in which the clause contain a sort of "second guard" that is only checked for consistency. Such a clause is written H : G:D|B. This clause is used to rewrite a literal only if G is entailed by the constraint store and D is consistent with it. In this case, both G and D are added to the constraint store.
Тарих
Бір мезгілдегі шектеулі логикалық бағдарламалауды зерттеу 1980 жылдардың соңында басталды, осы кезде Майкл Дж. Махер бір мезгілдегі логикалық бағдарламалау принциптерінің бір бөлігін шектеулі логикалық бағдарламалаумен біріктірді. Кейіннен, Мартин Ринард және Виджай А. Сарасват сияқты түрлі авторлар бір мезгілдегі шектеулі логикалық бағдарламалаудың теориялық қасиеттерін зерттеді.