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

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

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

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

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

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

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

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

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

${\displaystyle p\ }$

${\displaystyle r\leftarrow p,\ q}$

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

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

${\displaystyle p\ }$

${\displaystyle r\leftarrow p,\ q}$

${\displaystyle s\leftarrow p.}$

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

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

${\displaystyle p\ }$

${\displaystyle r\leftarrow p,\ q.}$

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

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

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

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

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

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

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

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

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

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

${\displaystyle p\leftarrow p}$

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

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

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

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

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

${\displaystyle r\leftarrow p}$

${\displaystyle r\leftarrow q}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle r\ }$

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

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

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

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

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

${\displaystyle p(a,b)\ }$

${\displaystyle p(c,d)\ }$

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

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

${\displaystyle p(a,b),\ p(c,d)\ }$

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

${\displaystyle \sim p(a,a),\ \sim p(a,c),\ \dots }$

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle p\lor \neg p}$

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

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