Семантика стійких моделей

Поняття стійко́ї моде́лі (англ. stable model), або набору відповідей, застосовується для визначення декларативних семантик для логічних програм із запереченням як відмовою. Це один із декількох стандартних підходів до значення заперечення в логічному програмуванні, поряд із повнотою програми та добре обґрунтованими семантиками. Семантики стійких моделей є основою програмування наборами відповідей.

Обґрунтування

Дослідження декларативних семантик заперечення в логічному програмуванні спонукав той факт, що поведінка ВЛВЗВ-резолюції, — узагальнення ВЛВ-резолюції, застосовуваного Прологом, — за наявності заперечень у тілах правил не повністю відповідає таблицям істинності, знайомим із класичної логіки висловлень. Розгляньмо, наприклад, програму

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p,\ {\hbox{not }}q.$

За цієї програми запит $p$ досягне успіху, оскільки програма включає $p$ як факт; запит $q$ зазнає невдачі, оскільки він не зустрічається в голові жодного з правил. Запит $r$ також зазнає невдачі, оскільки єдине правило з $r$ у голові містить підціль $q$ у своєму тілі; як ми вже бачили, ця підціль зазнає невдачі. Нарешті, запит $s$ досягає успіху, оскільки досягає успіху кожна з його підцілей $p$ та ${\hbox{not }}q$. (Остання досягає успіху, оскільки відповідна ствердна ціль $q$ зазнає невдачі.) У підсумку, поведінку ВЛВЗВ-резолюції даної програми може бути представлено таким приписуванням істинності:

$p$	$q$	$r$	$s$
T	F	F	T.

З іншого боку, правила даної програми можуть розглядатися як предикати, якщо ми ідентифікуємо кому з кон'юнкцією $\land$, символ ${\hbox{not}}$ — із запереченням $\neg$, і погодимося розглядати $F\leftarrow G$ як імплікацію $G\rightarrow F$, записану навпаки. Наприклад, крайнє правило програми з цієї точки зору є альтернативним записом предикату

$p\land \neg q\rightarrow s.$

Якщо ми обчислимо значення істинності правил програми для наведених вище приписувань істинності, то ми побачимо, що кожне правило набуває значення T. Іншими словами, що приписування є моделлю програми. Але ця програма має також й інші моделі, наприклад,

$p$	$q$	$r$	$s$
T	T	T	F.

Таким чином, одна з моделей даної програми є особливою в тому сенсі, що вона правильно представляє поведінку ВЛВЗВ-резолюції. Якими є математичні властивості такої моделі, що роблять її особливою? Відповідь на це питання дає визначення стійкої моделі.

Зв'язок із немонотонною логікою

Значення заперечення в логічних програмах тісно пов'язане з двома теоріями немонотонного міркування — автоепістемною логікою та логікою замовчувань. Відкриття цих зв'язків стало ключовим кроком до винаходження семантик стійких моделей.

Синтаксис автоепістемної логіки використовує модальний оператор, який дозволяє розрізняти, що є істинним, а чому вірять. Майкл Гельфонд 1987 року запропонував читати ${\hbox{not}}\ p$ в тілі правила як «$p$ немає віри», і розуміти правило із запереченням як відповідну формулу автоепістемної логіки. Семантика стійких моделей в її найпростішому вигляді може розглядатися як переформулювання цієї ідеї, що уникає явних посилань на автоепістемну логіку.

В логіці замовчувань замовчування подібне до правила висновування, за виключенням того, що воно, крім своїх передумов та висновку, включає перелік формул, що називаються підтвердженнями (англ. justifications). Замовчування може використовуватися для виведення його висновків за припущення, що його підтвердження узгоджуються з поточними переконаннями. Ніколь Бідуа та Крістін Фруадво 1987 року запропонували розглядати заперечні атоми в тілах правил як підтвердження. Наприклад, правило

$s\leftarrow p,\ {\hbox{not }}q$

можна розуміти як замовчування, що дозволяє нам виводити $s$ із $p$ за припущення, що $\neg q$ є узгодженим. Семантика стійких моделей використовує таку ж ідею, але не посилається явно на логіку замовчувань.

Стійкі моделі

Наведене нижче визначення стійкої моделі використовує дві умови. По-перше, приписування істинності ототожнюється з набором атомів, що набувають значення T. Наприклад, приписування істинності

$p$	$q$	$r$	$s$
T	F	F	T.

ототожнюється із набором $\{p,s\}$. Ця умова дозволяє використовувати відношення входження до цього набору для порівняння приписувань істинності між собою. Найменше з усіх приписувань істинності, $\emptyset$, є таким, яке робить кожен атом хибним; найбільше приписування істинності робить кожен атом істинним.

По-друге, логічна програма зі змінними розглядається як скорочений запис набору всіх замкнених примірників її правил, тобто результату підставлення вільних від змінних термів замість змінних до правил цієї програми всіма можливими способами. Наприклад, визначення парних (англ. even) чисел засобами логічного програмування

$even(0)\$

$even(s(X))\leftarrow {\hbox{not }}even(X)$

розглядається як результат заміни $X$ у цій програмі замкненими термами

$0,\ s(0),\ s(s(0)),\dots .$

всіма можливими способами. Результатом є нескінченна замкнена програма

$even(0)\$

$even(s(0))\leftarrow {\hbox{not }}even(0)$

$even(s(s(0)))\leftarrow {\hbox{not }}even(s(0))$

$\dots$

Визначення

Нехай $P$ буде набором правил вигляду

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

де $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ є замкненими атомами. Якщо $P$ не містить заперечення ($n=0$ у кожному з правил програми), тоді, за визначенням, єдиною стійкою моделлю $P$ є його модель, яка є мінімальною відносно включення правил. (Будь-яка програма без заперечення має рівно одну мінімальну модель.) Для розширення цього визначення на випадок програм із запереченням нам потрібне додаткове поняття збіднення (англ. reduct), визначене наступним чином.

Для будь-якого набору замкнених атомів $I$ збідненням (англ. reduct) $P$ відносно $I$ є набір правил без заперечення, отриманий з $P$ спершу виключенням кожного такого правила, в якому щонайменше один із атомів $C_{i}$ в його тілі

$B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

належить до $I$, а потім виключенням частин ${\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$ з тіл усіх правил, що лишилися.

Кажуть, що $I$ є стійкою моделлю $P$, якщо $I$ є стійкою моделлю збіднення $P$ відносно $I$. (Оскільки збіднення не містить заперечення, його стійку модель вже було визначено.) Як підказує термін «стійка модель», кожна стійка модель $P$ є моделлю $P$.

Приклад

Щоби проілюструвати ці визначення, перевірмо, чи є $\{p,s\}$ стійкою моделлю програми

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p,\ {\hbox{not }}q.$

Збідненням цієї програми відносно $\{p,s\}$ є

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p.$

(Справді, оскільки $q\not \in \{p,s\}$, збіднення отримується з програми виключенням частини ${\hbox{not }}q.\$) Стійкою моделлю збіднення є $\{p,s\}$. (Справді, цей набір атомів задовольняє кожне правило збіднення, і не має власного включення із такою ж властивістю.) Таким чином, після обчислення стійкої моделі збіднення ми повернулися до того ж самого набору $\{p,s\}$, з якого й починали. Отже, цей набір і є стійкою моделлю.

Перевірка таким самим чином інших 15 наборів з атомів $p,\ q,\ r,\ s$ показує, що ця програма не має інших стійких моделей. Наприклад, збідненням програми відносно $\{p,q,r\}$ є

$p\$

$r\leftarrow p,\ q.$

Стійкою моделлю цього збіднення є $\{p\}$, що відрізняється від набору $\{p,q,r\}$, з якого ми починали.

Програми без унікальної стійкої моделі

Програма з запереченням може мати багато стійких моделей, та не мати їх взагалі. Наприклад, програма

$p\leftarrow {\hbox{not }}q$

$q\leftarrow {\hbox{not }}p$

має дві стійкі моделі, $\{p\}$ та $\{q\}$. Програма з одного правила

$p\leftarrow {\hbox{not }}p$

не має стійких моделей.

Якщо ми думаємо про семантику стійких моделей як про опис поведінки Прологу в присутності заперечення, то програми без унікальної стійкої моделі можуть розцінюватися як незадовільні: вони не забезпечують недвозначного визначення для надавання відповідей на запити в стилі Прологу. Наприклад, наведені вище дві програми як Прологові програми є нерозумними — ВЛВЗВ-резолюція на них не добігає кінця.

Але застосування стійких моделей в програмуванні наборами відповідей пропонує таким програмам іншу перспективу. В цій парадигмі програмування дана задача пошуку представляється такою логічною програмою, стійкі моделі якої відповідають розв'язкам. Тоді програми з багатьма стійкими моделями відповідають задачам з багатьма розв'язками, а програми без стійких моделей відповідають нерозв'язним задачам. Наприклад, задача про вісім ферзів має 92 розв'язки; щоби розв'язати її із застосуванням програмування наборами відповідей, ми кодуємо її логічною програмою з 92 стійкими моделями. З цієї точки зору логічні програми з рівно однією стійкою моделлю в програмуванні наборами відповідей є радше особливими, як многочлени з рівно одним коренем в алгебрі.

Властивості семантики стійких моделей

В цьому розділі, як і в визначенні стійкої моделі вище, під логічною програмою ми розуміємо набір правил вигляду

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

де $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ є замкненими атомами.

Атоми голів (англ. head atoms): Якщо атом $A$ належить до стійкої моделі логічної програми $P$, то $A$ є головою одного з правил $P$.

Мінімальність (англ. minimality): Будь-яка стійка модель логічної програми $P$ є мінімальною серед моделей $P$ відносно включення до набору.

Антиланцюгова властивість (англ. the antichain property): Якщо $I$ та $J$ є стійкими моделями однієї й тієї ж логічної програми, то $I$ не є власним включенням $J$. Іншими словами, набір стійких моделей програми є антиланцюгом.

NP-повнота: Перевірка того, чи має скінченна замкнена логічна програма стійку модель, є NP-повною.

Зв'язок з іншими теоріями заперечення як відмови

Повнота програми

Будь-яка стійка модель скінченної замкненої програми є моделлю не лише самої програми, а й її повної програми. Обернене твердження, проте, не є вірним. Наприклад, повною програмою для програми з одного правила

$p\leftarrow p$

є тавтологія $p\leftrightarrow p$. Модель $\emptyset$ цієї тавтології є стійкою моделлю $p\leftarrow p$, але інша її модель, $\{p\}\$, — ні. Франсуа Фаж 1994 року знайшов синтаксичну умову для логічних програм, що усуває такі контрприклади, і гарантує стійкість кожної моделі повноти програми. Програми, які задовольняють цю умову, називаються цупкими (англ. tight).

Фанжен Лін та Ютін Жао 2004 року показали, як робити повну програму нецупкої програми сильнішою, так що всі її нестійкі моделі буде усунено. Додаткові формули, які вони додають до повної програми, називаються цикловими формулами (англ. loop formulas).

Добре обґрунтована семантика

Добре обґрунтована модель логічної програми поділяє всі замкнені атоми на три набори: істинні, хибні та невідомі. Якщо атом є істинним у добре обґрунтованій моделі програми $P$, то він належить до кожної стійкої моделі $P$. Зворотне, взагалі кажучи, не має місця. Наприклад, програма

$p\leftarrow {\hbox{not }}q$

$q\leftarrow {\hbox{not }}p$

$r\leftarrow p$

$r\leftarrow q$

має дві стійкі моделі, $\{p,r\}$ та $\{q,r\}$. Навіть незважаючи на те, що $r$ належить до них обох, його значенням у добре обґрунтованій моделі є невідоме.

Крім того, якщо атом є хибним у добре обґрунтованій моделі програми, то він не належить до жодної з її стійких моделей. Таким чином, добре обґрунтована модель логічної програми пропонує нижню межу перетину її стійких моделей, та верхню межу їхнього об'єднання.

Сильне заперечення

Представлення неповної інформації

З точки зору представлення знань набір замкнених атомів може розглядатися як опис повного стану знань: про атоми, що належать до набору, відомо, що вони істинні, а про атоми, що не належать до набору, відомо, що вони хибні. Можливо неповний стан знання може бути описано із застосуванням несуперечливого, але можливо неповного набору літералів; якщо атом $p$ не належить до цього набору, і його заперечення також не належить до цього набору, то не відомо, чи є $p$ істинним.

В контексті логічного програмування ця ідея призводить до потреби розрізнювати два типи заперечення — заперечення як відмови, обговорюваного вище, та сильного заперечення (англ. strong negation), що позначається тут через $\sim$. Наступний приклад, який показує різницю між цими двома типами заперечення, належить Джонові Маккарті. Шкільний автобус може перетнути (англ. Cross) залізничну колію за умови, що не наближається потяг (англ. Train). Якщо ми не обов'язково знаємо, чи наближається потяг, то правило з використанням заперечення як відмови

${\hbox{Cross}}\leftarrow {\hbox{not Train}}$

не є адекватним представленням цієї ідеї: воно каже, що можна перетинати за відсутності інформації про потяг, що наближається. Слабше правило, яке використовує сильне заперечення у своєму тілі, є кращим:

${\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.$

Воно каже, що можна перетинати, якщо ми знаємо, що потяг не наближається.

Послідовні стійкі моделі

Щоби включити сильне заперечення до теорії стійких моделей, Гельфонд та Ліфшиць дозволили кожному з виразів $A$, $B_{i}$ та $C_{i}$ у правилі

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

бути або атомом, або атомом із префіксом у вигляді символу сильного заперечення. Замість стійких моделей це узагальнення використовує набори відповідей (англ. answer sets), які можуть включати як атоми, так і атоми з префіксом сильного заперечення.

Альтернативний підхід розглядає сильне заперечення як частину атому, і не вимагає жодних змін у визначенні стійкої моделі. В цій теорії сильного заперечення ми розрізняємо атоми двох типів, ствердні (англ. positive) та заперечні (англ. negative), та припускаємо, що кожен заперечний атом є виразом вигляду $\sim A$, де $A\$ є ствердним атомом. Набір атомів називається послідовним (англ. coherent), якщо він не містить «взаємодоповнювальних» пар атомів $\ A,\sim A$. Послідовні стійкі моделі програми є ідентичними її несуперечливим наборам відповідей у сенсі Гельфонда та Ліфшиця 1991 року.

Наприклад, програма

$p\leftarrow {\hbox{not }}q$

$q\leftarrow {\hbox{not }}p$

$r\$

$\sim r\leftarrow {\hbox{not }}p$

має дві стійкі моделі, $\{p,r\}\$ та $\ \{q,r,\sim r\}$. Перша модель є послідовною, а друга — ні, оскільки вона містить як атом $\ r$, так і атом $\ \sim r$.

Припущення про замкненість світу

Відповідно до Гельфонда та Ліфшиця 1991 року, припущення про замкненість світу для предикату $p\$ може бути виражено правилом

$\sim p(X_{1},\dots ,X_{n})\leftarrow {\hbox{not }}p(X_{1},\dots ,X_{n})$

(відношення $p\$ не виконується для кортежу $X_{1},\dots ,X_{n}$, якщо немає свідчення, що воно виконується). Наприклад, стійка модель програми

$p(a,b)\$

$p(c,d)\$

$\sim p(X,Y)\leftarrow {\hbox{not }}p(X,Y)$

складається із 2 ствердних атомів

$p(a,b),\ p(c,d)\$

та 14 заперечних атомів

$\sim p(a,a),\ \sim p(a,c),\ \dots$

тобто, сильних заперечень всіх інших ствердних атомів, утворених із $p,\ a,\ b,\ c,\ d$.

Логічна програма із сильним запереченням може включати правила припущення замкненості світу для деяких її предикатів, і залишати інші предикати у сфері припущення про відкритість світу.

Програми з обмеженнями

Семантику стійких моделей було узагальнено на багато типів логічних програм, крім збірок обговорених вище «традиційних» правил — правил вигляду

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

де $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ є атомами. Одне з простих розширень дозволяє програмам містити обмеження (англ. constraints) — правила з порожньою головою:

$\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}.$

Пригадайте, що традиційне правило може розглядатися як альтернативний запис предикату, якщо ми ідентифікуємо кому з кон'юнкцією $\land$, символ ${\hbox{not}}$ — із запереченням $\neg$, і погодимося розглядати $F\leftarrow G$ як імплікацію $G\rightarrow F$, записану навпаки. Для розширення цієї угоди на обмеження ми ідентифікуємо обмеження із запереченням формули, що відповідає його тілу:

$\neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).$

Тепер ми можемо розширити визначення стійкої моделі на програми з обмеженнями. Як і у випадку традиційних програм, ми починаємо із програм, які не містять заперечень. Така програма може бути суперечливою; тоді ми кажемо, що вона не має стійких моделей. Якщо така програма є узгодженою, то $P$ має унікальну мінімальну модель, і ця модель розглядається як єдина стійка модель $P$.

Далі, стійкі моделі довільних програм із запереченнями визначаються із застосуванням збіднень, утворених таким же самим чином, як і у випадку традиційних програм (див. визначення стійкої моделі вище). Набір $I$ атомів є стійкою моделлю програми $P$ з обмеженнями, якщо збіднення $P$ відносно $I$ має стійку модель, і ця стійка модель дорівнює $I$.

Зазначені вище властивості семантики стійких моделей для традиційних програм мають місце також і в присутності обмежень.

Обмеження відіграють важливу роль у програмуванні наборами відповідей, оскільки додавання обмеження до логічної програми $P$ впливає на збірку стійких моделей $P$ дуже простим чином: воно усуває стійкі моделі, які порушують це обмеження. Іншими словами, для будь-якої програми з обмеженнями $P$ та будь-якого обмеження $C$ стійкі моделі $P\cup \{C\}$ можна охарактеризувати як стійкі моделі $P$, які задовольняють $C$.

Диз'юнктивні програми

У диз'юнктивному правилі (англ. disjunctive rule) голова може бути диз'юнкцією декількох атомів:

$A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

(крапка з комою розглядається як альтернативний запис диз'юнкції $\lor$). Традиційні правила відповідають $k=1$, а обмеження — $k=0$. Для розширення семантики стійких моделей на диз'юнктивні програми ми спершу визначаємо, що за відсутності заперечення ($n=0$ у кожному з правил) стійкими моделями програми є її мінімальні моделі. Визначення збіднення для диз'юнктивних програм залишається таким самим, як і раніше. Набір атомів $I$ є стійкою моделлю $P$, якщо $I$ є стійкою моделлю збіднення $P$ відносно $I$.

Наприклад, набір $\{p,r\}$ є стійкою моделлю диз'юнктивної програми

$p;q\$

$r\leftarrow {\hbox{not}}\ q$

оскільки він є однією з двох мінімальних моделей збіднення

$p;q\$

$r.\$

Наведена вище програма має ще одну стійку модель, $\{q\}$.

Як і у випадку традиційних програм, кожен елемент будь-якої стійкої моделі диз'юнктивної програми $P$ є атомом голови $P$, в тому сенсі, що він трапляється в голові одного з правил $P$. Як і у традиційному випадку, стійкі моделі диз'юнктивної програми є мінімальними, та утворюють антиланцюг. Перевірка того, чи має диз'юнктивна програма стійку модель, є $\Sigma _{2}^{\rm {P}}$-повною.

Стійкі моделі наборів предикатів

Правила, і навіть диз'юнктивні правила, мають доволі особливий синтаксичний вигляд у порівнянні з довільними предикатами. Кожне диз'юнктивне правило є по суті імплікацією, такою що її посилка (тіло правила) є кон'юнкцією літералів, а її наслідок (голова) є диз'юнкцією атомів. Девід Пірс 1997 року та Паоло Ферраріс 2005 року показали, як розширити визначення стійкої моделі на набори довільних предикатів. Це узагальнення має застосування в програмуванні наборами відповідей.

Пірсове формулювання виглядає дуже відмінним від первинного визначення стійкої моделі. Замість збіднень воно посилається на рівноважну логіку (англ. equilibrium logic) — систему немонотонної логіки на основі моделей Кріпке. З іншого боку, формулювання Ферраріса ґрунтується на збідненнях, хоча застосовуваний процес побудови збіднення і відрізняється від описаного вище. Ці два підходи до визначення стійких моделей для наборів предикатів є рівнозначними.

Загальне визначення стійкої моделі

Згідно Ферраріса, збідненням предикату $F$ відносно набору атомів $I$ є предикат, отриманий з $F$ заміною кожного максимального підпредикату, який не задовольняється $I$, логічною сталою $\bot$ (хиба). Збіднення набору предикатів $P$ відносно $I$ складається зі збіднень усіх предикатів із $P$ відносно $I$. Як і у випадку диз'юнктивних програм, ми кажемо, що набір атомів $I$ є стійкою моделлю $P$, якщо $I$ є мінімальною (відносно входження до набору) серед моделей збіднення $P$ відносно $I$.

Наприклад, збідненням набору

$\{p,\ p\land q\rightarrow r,\ p\land \neg q\rightarrow s\}$

відносно $\{p,s\}$ є

$\{p,\ \bot \rightarrow \bot ,\ p\land \neg \bot \rightarrow s\}.$

Оскільки $\{p,s\}$ є моделлю збіднення, а власні включення цього набору не є моделями збіднення, $\{p,s\}$ є стійкою моделлю даного набору предикатів.

Ми побачили, що $\{p,s\}$ є також стійкою моделлю тієї ж формули, записаної записом логічного програмування, в сенсі первинного визначення. Це є прикладом загального факту: в застосуванні до набору традиційних правил (предикатів, що відповідають їм) визначення стійкої моделі за Феррарісом є рівнозначним первинному визначенню. Теж саме є вірним, у загальнішому плані, для програм із обмеженнями та диз'юнктивних програм.

Властивості загальної семантики стійких моделей

Теорему про те, що всі елементи будь-якої стійкої моделі програми $P$ є атомами голови $P$, може бути розширено на набори предикатів, якщо ми визначимо атоми голови наступним чином. Атом $A$ є атомом голови набору предикатів $P$, якщо щонайменше одне входження $A$ до предикату з $P$ є ані під запереченням, ані в посилці імплікації. (Тут ми припускаємо, що еквівалентність трактується як абревіатура, а не як первісний сполучник.)

Мінімальність та властивість антиланцюговості стійких моделей традиційних програм в загальному випадку не мають місця. Наприклад, (одноелементний набір, єдиним елементом якого є) предикат

$p\lor \neg p$

має дві стійкі моделі, $\emptyset$ та $\{p\}$. Друга не є мінімальною, вона є власною надмножиною першої.

Перевірка того, чи має скінченний набір предикатів стійку модель, є $\Sigma _{2}^{\rm {P}}$-повною, як і в випадку диз'юнктивних програм.

Література

• S. Hanks and D. McDermott [1987] Nonmonotonic logic and temporal projection. Artificial Intelligence, Vol. 33, pages 379—412. (англ.)
• R. Reiter [1980] A logic for default reasoning. Artificial Intelligence, Vol. 13, pages 81–132. (англ.)

Див. також

• Програмування наборами відповідей
• Логічне програмування
• Заперечення як відмова