next up previous Sommario
Next: 5.2 Differenza tra programmi Up: 5. Operatori su teorie Previous: 5. Operatori su teorie   Sommario

5.1 Unione e intersezione di programmi logici

Due operatori di composizione di base sono l'unione e l'intersezione di programmi logici [BMPT90,MPRT90]che sono definiti come segue:

Definizione 5.1 (visione trasformazionale)  

Dati due programmi $P$ e $Q$:

Il primo ha il semplice effetto di restituire l'unione insiemistica delle clausole dei due programmi, mentre il secondo è l'operatore duale che restituisce una sorta di intersezione tra gli argomenti.

Esempio 5.1  


\begin{displaymath}(p(x,a) \leftarrow \neg q(x) ) \cap (p(b,y) \leftarrow r(y)) = (p(b,a) \leftarrow \neg q(b),r(a)) \end{displaymath}


\begin{displaymath}((p(a) \leftarrow q(b)) \cup p(b)) \cap (p(a) \leftarrow \neg q(c)) = (p(a) \leftarrow q(b),\neg q(c)) \end{displaymath}

Naturalmente, ogni programma può essere visto come una giustapposizione delle sue clausole.

L'interpretazione logica di questi operatori può essere data riferendosi alla teoria del completamento di un programma.

Teorema 5.1 (visione logica)  

Sia $\forall x_{1},\ldots ,x_{n} (p(x_{1},\ldots ,x_{n}) \leftrightarrow \Psi )$ la definizione completata del predicato $p$ in $comp(P)$ e $\forall x_{1},\ldots ,x_{n} (p(x_{1},\ldots ,x_{n}) \leftrightarrow \Phi)$ la definizione completata del predicato $p$ in $comp(Q)$

allora

  1. $\forall x_{1},\ldots ,x_{n} (p(x_{1},\ldots ,x_{n}) \leftrightarrow \Lambda)$ è la definizione completata di $p$ in $comp(P \cup Q)$, e $\Lambda \leftrightarrow (\Psi \vee \Phi)$;

  2. $\forall x_{1},\ldots ,x_{n} (p(x_{1},\ldots ,x_{n}) \leftrightarrow \Lambda)$ è la definizione completata di $p$ in $comp(P \cap Q)$, e $\Lambda \leftrightarrow (\Psi \wedge \Phi)$;

Se la classe di programmi considerata è quella dei programmi definiti, sono validi i seguenti risultati che forniscono una semantica dell'unione e dell'intersezione basata prima sull'operatore di conseguenza immediata e poi sui modelli.

Teorema 5.2  

Dati due programmi $P$ e $Q$:

  1. $T_{P \cup Q}$ = $\lambda I. $ $ T_{P}(I) \cup T_{Q}(I)$

  2. $T_{P \cap Q}$ = $\lambda I. $ $ T_{P}(I) \cap T_{Q}(I)$

Nel seguito la notazione $ P' \ll P$ sta per "$P'$ è un sottoinsieme di $ground(P)$'' e $facts(P)$ denota l'insieme delle clausole unitarie di $P$.

Definizione 5.2  

Dati due programmi $P$ e $Q$:

$M_{P \cup Q}$ = $\bigcap \{ M \mid M \models P \; \& \; M \models Q\}$ = min $\{M \mid M \models P \; \& \; M \models Q\}$

$M_{P \cap Q}$ = $\bigcup \{M \mid M = M_{P'} = M_{Q'} \; \& \; P' \ll P \; \& \; Q'\ll Q \; \& \; facts(P') = facts(Q') \}$

La definizione data stabilisce che il modello minimo dell'unione di due programmi $P$ e $Q$ è l'interpretazione minimale che è modello sia di $P$ che di $Q$, mentre il modello minimo dell'intersezione è il più grande modello minimo comune di due sottoteorie ground di $P$ e $Q$ con lo stesso insieme di clausole unitarie.

Il fatto che $M_{P \cup Q}$ e $M_{P \cap Q}$ sono effettivamente modelli minimi di Herbrand di $P \cup Q$ e $P \cap Q$, rispettivamente, è stabilito dal seguente teorema:

Teorema 5.3  

Dati due programmi $P$ e $Q$:


\begin{displaymath}lfp(T_{P \cup Q}) = M_{P \cup Q} \end{displaymath}


\begin{displaymath}lfp(T_{P \cap Q}) = M_{P \cap Q} \end{displaymath}

Un'ulteriore definizione di questi operatori è quella meta-interpretativa, che può essere data estendendo il meta-interprete standard solve (vanilla). Tale meta-interprete, che simula il modello computazionale dei programmi logici, è definito nel seguente modo:


\begin{displaymath}solve(true) \leftarrow \end{displaymath}


\begin{displaymath}solve(G1,G2) \leftarrow solve(G1), solve(G2) \end{displaymath}


\begin{displaymath}solve(G) \leftarrow clause(G \leftarrow B), solve(B) \end{displaymath}

dove il predicato clause è usato per rappresentare il programma oggetto.

Naturalmente, per trattare una molteplicità di programmi, è necessario aggiungere un nuovo argomento sia a solve che a clause per specificare il programma in cui provare un certo goal.

La definizione di solve diventa:


\begin{displaymath}solve(T,true) \leftarrow \end{displaymath}


\begin{displaymath}solve(T, (G1,G2)) \leftarrow solve(T,G1), solve(T,G2) \end{displaymath}


\begin{displaymath}solve(T,G) \leftarrow clause(T,G \leftarrow B), solve(T,B) \end{displaymath}

Usando la ricorsione nella definizione del predicato clause infine si ottengono le definizioni meta-interpretative degli operatori:


\begin{displaymath}clause((T1 \cup T2),H \leftarrow B) \leftarrow clause (T1,H \leftarrow B) \end{displaymath}


\begin{displaymath}clause((T1 \cup T2),H \leftarrow B) \leftarrow clause (T2,H \leftarrow B) \end{displaymath}


\begin{displaymath}clause((T1 \cap T2),H \leftarrow (B1,B2)) \leftarrow clause(T1, H \leftarrow B1), clause(T2, H \leftarrow B2) \end{displaymath}

Il seguente teorema prova che questa visione meta-interpretativa è equivalente a quella trasformazionale.

Teorema 5.4  

Siano $P$ e $Q$ due programmi logici. $T$ denoti il programma composto dal meta-interprete solve e delle clausole di $P$ e $Q$ rappresentate per mezzo del predicato clause. $Op$ denoti $\cup$ oppure $\cap$.

Il programma ottenuto valutando parzialmente rispetto al goal $\leftarrow solve((P Op Q),p(X))$, per ogni predicato $p$ definito in $P$ o in $Q$, è $P Op Q$.


next up previous Sommario
Next: 5.2 Differenza tra programmi Up: 5. Operatori su teorie Previous: 5. Operatori su teorie   Sommario
Roberto Giungato 2001-03-14