Sémantique des modèles stables

Soit P un ensemble de règles de la forme

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

où ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$ sont des termes clos. Si P ne contient pas de négation (${\displaystyle n=0}$ dans chaque règle du programme) alors, on peut montrer qu'il a exactement un modèle minimal (au sens de l'inclusion des ensembles[1]) obtenu par propagation des clauses unitaires, ceci permet de définir le modèle stable de P.

Pour étendre cette définition au cas des programmes avec négation, nous avons besoin du concept auxiliaire de réduction, que l'on définit comme suit.

Pour tout ensemble I d'atomes clos, la réduction du programme P par rapport à I est l'ensemble des règles sans négation obtenu à partir de P en supprimant d'abord chaque règle pour laquelle au moins un des atomes ${\displaystyle C_{i}}$ dans son corps

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

appartient à I. Puis en supprimant les parties ${\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$ dans le corps de toutes les règles restantes.

On dit alors que I est un modèle stable de P si I est le modèle stable du programme ${\displaystyle P_{|I}}$ obtenu en réduisant P par rapport à I. Par construction ${\displaystyle P_{|I}}$ ne contient pas de négation et son modèle stable est donc bien défini. Comme le suggère le terme « modèle stable », tout modèle stable de P est un modèle de P.

Pour illustrer ces définitions, vérifions que ${\displaystyle \{p,s\}}$ est un modèle stable du programme suivant :

${\displaystyle p\ }$

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

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

La réduction de ce programme par rapport à ${\displaystyle \{p,s\}}$ est

${\displaystyle p\ }$

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

${\displaystyle s\leftarrow p.}$

(En effet, puisque ${\displaystyle q\not \in \{p,s\}}$, la réduction est obtenue en supprimant la partie négative de la dernière règle.) Comme l'ensemble satisfait toutes les règles de la réduction (et aucun de ses sous-ensembles n'a cette propriété), le modèle stable de la réduction est donc ${\displaystyle \{p,s\}}$. Ainsi, comme la réduction de notre programme par ${\displaystyle \{p,s\}}$ aboutit à ce même ensemble, cet ensemble est bien un modèle stable.

On peut alors vérifier de la même manière que les 15 autres ensembles constitués des atomes ${\displaystyle p,\ q,\ r,\ s}$ ne sont pas eux-mêmes des modèles stables. Par exemple, la réduction du programme par rapport à ${\displaystyle \{p,q,r\}}$ est

${\displaystyle p\ }$

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

Le modèle stable de cette réduction est ${\displaystyle \{p\}}$ ce qui est différent de l'ensemble ${\displaystyle \{p,q,r\}}$ utilisé pour la réduction.

Un programme avec négation peut avoir plusieurs modèles stables ou bien aucun modèle stable. Par exemple, le programme

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

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

a deux modèles stables ${\displaystyle \{p\}}$, ${\displaystyle \{q\}}$ . Tandis que le programme constitué d'une seule règle

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

n'a pas de modèles stables.

Si nous considérons la sémantique du modèle stable comme une description du comportement de Prolog en présence de négation, alors les programmes qui n'ont pas un modèle stable unique peuvent être jugés non satisfaisants dans le sens où ils ne fournissent pas une spécification sans ambiguïté pour la réponse aux requêtes de style Prolog. Ainsi, les deux programmes ci-dessus ne forment pas des programmes Prolog raisonnables puisque leur résolution du SLDNF ne termine pas.

Mais l'utilisation des modèles stables dans ASP offre une perspective différente sur de tels programmes. Dans ce paradigme de programmation, un problème de recherche donné est représenté par un programme logique de sorte que les modèles stables du programme correspondent aux solutions. Dans ce cadre, les programmes ayant plusieurs modèles stables correspondent à des problèmes avec plusieurs solutions, tandis que les programmes sans modèles stables sont des problèmes insolubles. Par exemple, le problème des huit reines a 92 solutions ; pour le résoudre à l'aide d'un programme ASP, nous l'encodons par un programme logique ayant 92 modèles stables. De ce point de vue, les programmes logiques avec exactement un modèle stable sont des cas assez spéciaux dans ASP, comme peuvent l'être en algèbre, les polynômes avec une seule racine.

Tout modèle stable d'un programme clos fini est non seulement un modèle du programme lui-même, mais aussi un modèle de son achèvement [Marek et Subrahmanian, 1989]. Cependant, l'inverse n'est pas vrai. Par exemple, l'achèvement du programme constitué de l'unique règle :

${\displaystyle p\leftarrow p}$

est la tautologie ${\displaystyle p\leftrightarrow p}$ . Le modèle ${\displaystyle \emptyset }$ de cette tautologie est un modèle stable de ${\displaystyle p\leftarrow p}$, mais son autre modèle ${\displaystyle \{p\}\ }$ n'en est pas un. Comme l'a prouvé François Fages [1994], il existe une condition syntaxique sur les programmes logiques permettant de se prémunir contre de tels contre-exemples et qui garantit ainsi la stabilité de chaque modèle d'achèvement du programme. De tels programmes sont dits serrés.

Fangzhen Lin et Yuting Zhao [2004] ont montré comment renforcer l'achèvement d'un programme non serré, en y ajoutant des formules dites "de boucles", afin d'éliminer tous ses modèles instables.

Dans la sémantique bien fondée, les atomes clos d'un programme logique sont répartis en trois ensembles : vrai, faux et inconnu. Si un atome est vrai dans le modèle bien fondé de ${\displaystyle P}$, alors il est vrai dans tous les modèles stables de ${\displaystyle P}$. Encore une fois, l'inverse n'est pas vrai en général. Par exemple, le programme

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

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

${\displaystyle r\leftarrow p}$

${\displaystyle r\leftarrow q}$

a deux modèles stables, ${\displaystyle \{p,r\}}$ et ${\displaystyle \{q,r\}}$. Bien que ${\displaystyle r}$ soit vrai dans ces deux modèles, sa valeur dans le modèle bien fondé est inconnue.

De plus, si un atome est faux dans le modèle bien fondé d'un programme alors il est faux pour tous ses modèles stables. Ainsi, le modèle bien fondé d'un programme logique fournit-il une borne inférieure sur l'intersection de ses modèles stables et une borne supérieure sur leur union.

Du point de vue de la représentation des connaissances, un ensemble d'atomes clos peut être considéré comme la description d'un état des connaissances : les atomes qui appartiennent à l'ensemble sont connus pour être vrais, et les atomes qui n'appartiennent pas à l'ensemble sont connus pour être faux. Un état de connaissance éventuellement incomplet peut cependant être décrit à l'aide d'un ensemble cohérent mais éventuellement incomplet de littéraux (c'est-à-dire de l'ensemble des atomes clos et de leurs négations) ; si ni un atome ${\displaystyle p}$ ni sa négation n'appartiennent à l'ensemble alors on ne sait pas si ${\displaystyle p}$ est vrai ou faux.

Dans le contexte de la programmation logique, cette idée conduit à la nécessité de distinguer deux types de négation — la négation par l'échec, discutée ci-dessus, et la négation forte, que nous indiqueront par ${\displaystyle \sim }$[2]. L'exemple suivant, illustrant la différence entre ces deux types de négation, a été proposé par John McCarthy : "Un autobus scolaire ne peut traverser une voie ferrée qu'à condition qu'aucun train ne s'approche". Si l'on ne sait pas si un train approche ou non, alors une règle reposant sur la négation par l'échec

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

n'est pas une représentation adéquate de cette idée : puisqu'elle laisserait à penser qu'il est acceptable de traverser en l'absence d'informations sur l'approche d'un train. La règle, plus faible, qui utilise une négation forte dans son corps, est ainsi préférable :

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

elle dit qu'il est possible de traverser si et seulement si nous savons qu'aucun train ne s'approche.

Afin d'introduire la notion de négation forte dans la théorie des modèles stables, Gelfond et Lifschitz [1991] ont proposé que chacune des expressions ${\displaystyle A}$, ${\displaystyle B_{i}}$, ${\displaystyle C_{i}}$ dans une règle

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

puisse être soit un atome, soit la négation forte d'un atome. Cette généralisation fournit alors des ensembles de réponses (au lieu de modèles stables), qui peuvent inclure à la fois des atomes et des atomes préfixés par une négation forte.

Une approche alternative [Ferraris et Lifschitz, 2005] traite la négation forte comme une partie d'un atome (elle ne nécessite donc aucun changement dans la définition d'un modèle stable). Dans cette théorie de la négation forte, nous distinguons des atomes de deux sortes, positifs et négatifs, et nous supposons que chaque atome négatif est une expression de la forme ${\displaystyle \sim A}$, où ${\displaystyle A\ }$ est un atome positif. Un ensemble est dit cohérent s'il ne contient pas de paires d'atomes "complémentaires" ${\displaystyle \ A,\sim A}$ . Les modèles stables cohérents d'un tel programme sont alors identiques aux ensembles de réponses cohérentes au sens de [Gelfond et Lifschitz, 1991].

Par exemple, le programme

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

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

${\displaystyle r\ }$

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

a deux modèles stables : ${\displaystyle \{p,r\}\ }$ et ${\displaystyle \ \{q,r,\sim r\}}$, le premier modèle étant cohérent et le second ne l'étant pas.

Selon [Gelfond et Lifschitz, 1991], l'hypothèse du monde clos pour un prédicat ${\displaystyle p\ }$ peut être exprimé par la règle

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

(la relation ${\displaystyle p\ }$ est considérée comme fausse pour un tuple ${\displaystyle X_{1},\dots ,X_{n}}$ s'il n'y a aucune preuve qu'elle soit vraie). Par exemple, le modèle stable du programme

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

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

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

se compose de 2 atomes positifs

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

et 14 atomes négatifs

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

c'est-à-dire, les négations fortes de tous les autres atomes clos positifs formés à partir de ${\displaystyle p,\ a,\ b,\ c,\ d}$.

Un programme logique utilisant la négation forte peut inclure les règles d'hypothèse du monde clos uniquement pour certains de ses prédicats, laissant ainsi les autres prédicats dans le domaine de l'hypothèse du monde ouvert .

Selon [Ferraris, 2005], la réduction d'une formule propositionnelle ${\displaystyle F}$ par rapport à un ensemble ${\displaystyle I}$ d'atomes est la formule obtenue à partir de ${\displaystyle F}$ en remplaçant chaque sous-formule maximale non satisfaite par ${\displaystyle I}$ par la constante logique ${\displaystyle \bot }$ (faux). La réduction d'un ensemble ${\displaystyle P}$ de formules propositionnelles par ${\displaystyle I}$ se compose alors des réductions de toutes les formules de ${\displaystyle P}$ par ${\displaystyle I}$ . Comme dans le cas des programmes disjonctifs, on dit qu'un ensemble ${\displaystyle I}$ d'atomes est un modèle stable de ${\displaystyle P}$ si ${\displaystyle I}$ est minimale (au sens de l'inclusion des ensembles) parmi les modèles de la réduction de ${\displaystyle P}$ par ${\displaystyle I}$.

Par exemple, la réduction de l'ensemble

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

par l'ensemble ${\displaystyle \{p,s\}}$ est

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

Puisque ${\displaystyle \{p,s\}}$ est un modèle de cette réduction, et que les sous-ensembles stricts de cet ensemble ne sont pas des modèles de la réduction, ${\displaystyle \{p,s\}}$ est bien un modèle stable de cet ensemble de formules.

Nous avons vu que ${\displaystyle \{p,s\}}$ est aussi un modèle stable de la même formule, écrit en tant que programme logique. C'est un exemple d'un fait général : lorsqu'elle est appliquée à un ensemble de (formules correspondant à) des règles (au sens traditionnel, avec contrainte ou même disjonctives), la définition d'un modèle stable selon Ferraris est équivalente à la définition donnée dans cet article.

Le théorème affirmant que les éléments de tous les modèle stable d'un programme ${\displaystyle P}$ sont des atomes des têtes de ${\displaystyle P}$ peut être étendu à des ensembles de formules propositionnelles en utilisant la définition suivante. Un atome ${\displaystyle A}$ est un atome de tête d'un ensemble ${\displaystyle P}$ de formules propositionnelles si au moins une occurrence de ${\displaystyle A}$ dans une formule de ${\displaystyle P}$ n'est ni dans la portée d'une négation ni dans l'antécédent d'une implication.

La minimalité et la propriété d'antichaîne des modèles stables valable pour un programme traditionnel ne sont cependant plus vrai dans ce cas général. Par exemple, (l'ensemble singleton composé de) la formule

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

a deux modèles stables, ${\displaystyle \emptyset }$ et ${\displaystyle \{p\}}$ . Ce dernier n'est cependant pas minimal et c'est un sur-ensemble strict du premier.

Tester si un ensemble fini de formules propositionnelles a un modèle stable est ${\displaystyle \Sigma _{2}^{\rm {P}}}$ -complet, comme dans le cas des programmes disjonctifs .