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$ :

$\cup$ è il programma ottenuto unendo le clausole di e .
$\cap$ è il programma ottenuto come segue:
Se $H \leftarrow A_{1}, \ldots , A_{n}$ è una clausola di
e $H' \leftarrow B_{1}, \ldots , B_{k}$ è una clausola di
e esiste $\theta$ =
allora $(H \leftarrow A_{1}, \ldots , A_{n},B_{1}, \ldots , B_{k})\theta$ è una clausola di $\cap$ .

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

$\forall x_{1},\ldots ,x_{n} (p(x_{1},\ldots ,x_{n}) \leftrightarrow \Lambda)$ è la definizione completata di in $comp(P \cup Q)$ , e $\Lambda \leftrightarrow (\Psi \vee \Phi)$ ;
$\forall x_{1},\ldots ,x_{n} (p(x_{1},\ldots ,x_{n}) \leftrightarrow \Lambda)$ è la definizione completata di 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$ :

$T_{P \cup Q}$ = $\lambda I.$ $T_{P}(I) \cup T_{Q}(I)$
$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

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$

è l'interpretazione minimale che è modello sia di $P$

che di

, mentre il modello minimo dell'intersezione è il più grande modello minimo comune di due sottoteorie ground di $P$

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:

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.

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

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$ .