Кіріспе
Тұрақты модель немесе жауаптар жиынтығы түсінігі, теріске шығару арқылы сәтсіздік принципі бар логикалық бағдарламаларға декларативтік семантиканы анықтау үшін қолданылады. Бұл, логикалық бағдарламалаудағы теріске шығарудың мағынасын түсіндірудің бірнеше стандартты тәсілдерінің бірі, бағдарламаны толықтыру және жақсы негізделген семантика сияқты. Тұрақты модель семантикасы жауаптар жиынтығын бағдарламалаудың негізі болып табылады.
answer set programming.
Монотонды емес логикаға қатынасы
Логикалық бағдарламалардағы жоққа шығарудың мәні монотонды емес ойлаудың екі теориясымен тығыз байланысты: автоэпистемиялық логика және әдепкі логика. Осы қатынастардың анықталуы тұрақты модель семантикасын ойлап табуға қадам болды. Автоэпистемиялық логиканың синтаксисі модальдық операторды пайдаланады, бұл шындық пен белгілі нәрсені ажыратуға мүмкіндік береді. Майкл Гельфонд [1987] ереженің денесіндегі жоққа шығаруды "белгілі емес" деп оқуды және жоққа шығаруы бар ережені автоэпистемиялық логиканың сәйкес формуласы ретінде түсінуді ұсынды. Тұрақты модель семантикасы негізгі нысанында автоэпистемиялық логикаға тікелей сілтемелерді болдырмайтын осы идеяның қайта формулировкасы ретінде қарастырылуы мүмкін. Әдепкі логикада әдепкі, тұжырымдамалық ережеге ұқсас, бірақ оның алғышарттары мен қорытындысынан өзгеше, негіздемелер деп аталатын формулалар тізімін қамтиды. Әдепкі, оның негіздемелері қазіргі уақытта белгілі нәрселермен үйлесімді деген болжаммен, қорытындысын шығару үшін қолданылуы мүмкін. Николь Бидуи және Кристин Фройдво [1987] ережелердің денелеріндегі жоққа шығарылған атомдарды негіздемелер ретінде қарастыруды ұсынды. Мысалы, ереже тұрақты деп есептегенде шығарылатын әдепкі ретінде түсіндірілуі мүмкін. Тұрақты модель семантикасы да осы идеяны қолданады, бірақ ол әдепкі логикасына тікелей сілтеме жасамайды.
can be understood as the default that allows us to derive from assuming that is consistent. The stable model semantics uses the same idea, but it does not explicitly refer to default logic.
Бірегей тұрақты моделі жоқ бағдарламалар
Теріс бағдарламада көптеген тұрақты модельдер болуы немесе тұрақты модельдердің жоқтығы мүмкін. Мысалы, бағдарлама екі тұрақты модельге ие, ал бір ережелі бағдарламада тұрақты модель жоқ. Егер тұрақты модель семантикасын теріске шығарудың алдында Prolog-тың мінез-құлқының сипаттамасы ретінде қарастырсақ, онда бірегей тұрақты модельсіз бағдарламалар қанағаттандырмайды: олар Prolog стиліндегі сұрақтарға жауап беру үшін нақты спецификацияны ұсынбайды. Мысалы, жоғарыдағы екі бағдарлама SLDNF шешімі олармен аяқталмайтындықтан Prolog бағдарламалары ретінде ақылға қонымсыз. Бірақ жауаптар жиынтығын бағдарламалауда тұрақты модельдерді пайдалану мұндай бағдарламаларға басқаша көзқарас ұсынады. Бұл бағдарламалау парадигмасында берілген іздеу мәселесі логикалық бағдарлама арқылы бейнеленеді, сондықтан бағдарламаның тұрақты модельдері шешімдерге сәйкес келеді. Осылайша, көптеген тұрақты модельдері бар бағдарламалар көптеген шешімдері бар мәселелерге, ал тұрақты модельдері жоқ бағдарламалар шешілмейтін мәселелерге сәйкес келеді. Мысалы, сегіз патшайымның жұмбағы 92 шешімге ие; оны жауаптар жиынтығын бағдарламалау арқылы шешу үшін біз оны 92 тұрақты модельді логикалық бағдарламамен кодтаймыз. Осы тұрғыдан алғанда, жауаптар жиынтығын бағдарламалауда дәл бір тұрақты моделі бар логикалық бағдарламалар алгебрадағы дәл бір түбірі бар полиномдар сияқты ерекше болып табылады.
has two stable models , The one rule program
has no stable models. If we think of the stable model semantics as a description of the behavior of Prolog in the presence of negation then programs without a unique stable model can be judged unsatisfactory: they do not provide an unambiguous specification for Prolog style query answering. For instance, the two programs above are not reasonable as Prolog programs—SLDNF resolution does not terminate on them. But the use of stable models in answer set programming provides a different perspective on such programs. In that programming paradigm, a given search problem is represented by a logic program so that the stable models of the program correspond to solutions. Then programs with many stable models correspond to problems with many solutions, and programs without stable models correspond to unsolvable problems. For instance, the eight queens puzzle has 92 solutions; to solve it using answer set programming, we encode it by a logic program with 92 stable models. From this point of view, logic programs with exactly one stable model are rather special in answer set programming, like polynomials with exactly one root in algebra.
Бағдарламаның аяқталуы
Таяу негіздегі бағдарламаның кез келген тұрақты моделі бағдарламаның өзінің де, сонымен қатар оның толықтырылуының да моделі болып табылады [Marek and Subrahmanian, 1989]. Дегенмен, керісінше дұрыс емес. Мысалы, бір ережелі бағдарламаның толықтырылуы таутология болып табылады. Осы таутологияның моделі – бағдарламаның тұрақты моделі, бірақ оның басқа моделі – емес. Франсуа Фаж [1994] логикалық бағдарламаларда мұндай қарсы мысалдарды жоятын және бағдарламаның толықтырылуының әрбір моделінің тұрақтылығын қамтамасыз ететін синтаксистік шартты тапты. Оның шартын қанағаттандыратын бағдарламалар тығыз деп аталады. Фанчжэн Лин және Ютинг Чжао [2004] толықтырылмаған бағдарламаны қалай күшейтуге болатынын көрсетті, осылайша оның барлық тұрақсыз модельдері жойылады. Олар толықтыруға қосатын қосымша формулалар циклдық формулалар деп аталады.
is the tautology The model of this tautology is a stable model of , but its other model is not. François Fages [1994] found a syntactic condition on logic programs that eliminates such counterexamples and guarantees the stability of every model of the program's completion. The programs that satisfy his condition are called tight. Fangzhen Lin and Yuting Zhao [2004] showed how to make the completion of a nontight program stronger so that all its nonstable models will be eliminated. The additional formulas that they add to the completion are called loop formulas.
Жақсы негізделген семантика
Логикалық бағдарламаның негізді моделі барлық ядролық атомдарды үш топқа бөледі: рас, жалған және белгісіз. Егер атом негізді модельде рас болса, онда ол барлық тұрақты модельдерге жатады. Алайда, керісінше, әдетте дұрыс емес. Мысалы, бағдарлама
екі тұрақты модельге ие: және . Олардың екеуіне де тиесілі болғанымен, оның негізді модельдегі мәні белгісіз. Бұдан әрі, егер атом бағдарламаның негізді моделінде жалған болса, онда ол оның ешбір тұрақты моделіне жатпайды. Осылайша, логикалық бағдарламаның негізді моделі оның тұрақты модельдерінің қиылысы үшін төменгі шек және олардың бірігі үшін жоғарғы шек береді.
Толық емес ақпаратты білдіреді
Білімді бейнелеу тұрғысынан алғанда, негізгі атомдар жиыны білімнің толық күйін сипаттау ретінде қарастырылуы мүмкін: жиынға жататын атомдар рас деп танылады, ал жиынға жатпайтын атомдар жалған деп танылады. Мүмкін толық емес білім күйін дәйекті, бірақ толық емес болуы мүмкін әдебиеттер жиыны арқылы сипаттауға болады; егер атом жиынға жатпаса және оның жоқтығы да жиынға жатпаса, онда ол рас па, жалған ба белгісіз болады. Логикалық бағдарламалау контекстінде бұл идея екі түрлі жоқтыққа бөлу қажеттігіне әкеледі – жоқтық сәтсіздік ретінде, жоғарыда талқыланғандай, және күшті жоқтық, бұл жерде күшті жоқтық деп белгіленеді. Екі түрлі жоқтықтың айырмашылығын көрсететін мысал Джон Маккартиге тиесілі. Мектеп автобусы пойыз келмей тұрған жағдайда теміржол жолынан өте алады. Егер біз пойыздың келе жатқан-келмей жатқанын білмейтін болсақ, онда жоқтық ретінде пайдаланылатын ереже бұл идеяны толыққанды жеткізбейді: ол пойыз туралы ақпарат болмағанда өтуге болатынын айтады. Күшті жоқтықты қолданатын әлсіз ереже артық: ол біз пойыз келмейтінін білгенде ғана өтуге болатынын айтады.
is not an adequate representation of this idea: it says that it's okay to cross in the absence of information about an approaching train. The weaker rule, that uses strong negation in the body, is preferable:
It says that it's okay to cross if we know that no train is approaching.
Ұйғарымдық формулалар жиынтығының тұрақты үлгілері
Ережелер, тіпті дизъюнктивтік ережелер де, кездейсоқ логикалық формулалармен салыстырғанда, ерекше синтаксистік формаға ие. Әрбір дизъюнктивтік ереже, по сути, импликация болып табылады, онда оның антецеденті (ереженің денесі) – литералдардың конъюнкциясы, ал консеквенты (басы) – атомдардың дизъюнкциясы. Дэвид Пирс [1997] және Паоло Феррарис [2005] тұрақты модельдің анықтамасын кездейсоқ логикалық формулалар жиынына қалай кеңейтуге болатынын көрсетті. Бұл жалпылау жиынтық бағдарламалауда жауап беруге қолданылады. Пирс ұсынған формулировка тұрақты модельдің бастапқы анықтамасынан мүлдем өзгеше. Редукциялардың орнына, ол Крипке модельдеріне негізделген, монотонды емес логика жүйесі – тепе-теңдік логикасына сілтеме жасайды. Ал Феррарис ұсынған формулировка редукцияға негізделген, бірақ ол қолданатын редукцияны құру процесі жоғарыда сипатталғаннан өзгеше. Логикалық формулалар жиыны үшін тұрақты модельдерді анықтаудың екі тәсілі де бір-біріне эквивалентті.
Тұрақты модельдің жалпы семантикасының қасиеттері
Кез келген тұрақты модельдің барлық элементтері бағдарламаның бас атомдары екенін айтатын теореманы, егер бас атомдарды келесідей анықтасақ, ұйғарымдық формулалар жиынына дейін кеңейтуге болады. Егер ұйғарымдық формулалар жиынындағы формуланың біреуінде атом теріс пікірлеу шеңберіне де, импликацияның алшартына да кірмесе, онда ол атом – ұйғарымдық формулалар жиынының бас атомы болып саналады. (Біз эквиваленттілікті бастапқы байланыс емес, қысқарту ретінде қарастырамыз.) Дәстүрлі бағдарламаның тұрақты модельдерінің минималдылығы және анти-тізбек қасиеттері жалпы жағдайда сақталмайды. Мысалы, (бір ғана формуладан тұратын) жиынның екі тұрақты моделі бар, және екіншісі минималды емес, ал ол біріншісінің нақты үстін жиынтығы болып табылады. Ұйғарымдық формулалардың шекті жиынының тұрақты моделінің болуын тексеру, дизъюнктивті бағдарламалар сияқты, толық.
has two stable models, and The latter is not minimal, and it is a proper superset of the former. Testing whether a finite set of propositional formulas has a stable model is complete, as in the case of disjunctive programs.