Programmazione Logica -- Lezione 2: Semantica Operazionale
Introduzione
Lo scopo di un programma logico e' quello di definire certi predicati. Una
computazione consiste nel cercare di dimostrare che un predicato,
applicato a certi termini,
e' conseguenza logica del programma. In generale ci interessa anche
computare i termini per cui
tale predicato vale.
Un modo di fare questa dimostrazione potrebbe essere quello di
sfruttare l'analogia con le definizioni induttive, e di costruire quindi l'albero
di prova per l'atomo che vogliamo dimostrare appartenere al modello minimo.
Tale strategia pero' non e' una buona definizione computazionale, perche' non e'
indicato come si debba effettuare l'istanziazione delle metavariabili.
Provare tutte le istanziazioni ovviamente non e' ragionevole, poiche' in
generale i termini dell'universo di Herbrand sono infiniti!
Invece di istanziare le variabili con termini ground, conviene
quindi cercare di istanziare di volta in volta quel tanto che basta per
poter fare un passo di deduzione. Vediamo piu' formalmente cosa significa.
Cominciamo col dare un po' di definizioni:
Sostituzioni
- Definizione
- Una sostituzione e' una qualsiasi funzione
sigma
dalle variabili nei termini tale che:
Dom(sigma) = {x | sigma(x) =/= x } e' finito
Notazione: se Dom(sigma) = {x1, x2, ... , xn} e
sigma(x1) = t1, sigma(x2) = t2, ... , sigma(xn) = tn,
rappresenteremo sigma con l'insieme
{x1/t1, x2/t2, ... , xn/tn}.
- Definizione
- L'applicazione di una
sostituzione
sigma
ad un termine t, che indicheremo con la notazione
postfissa t sigma,
e' il termine che si ottiene sostituendo simultaneamente ad ogni
variabile x
in t il termine sigma(x).
Notare che invece di sigma(x) possiamo anche
scrivere x sigma.
- Esempio
- Consideriamo il termine
t = f(x , y , g(a,z)) e
la sostituzione
sigma = {x/h(y), y/b}.
Avremo che t sigma = f(h(y),b,g(a,z)).
- Definizione
- La composizione di due sostituzioni
sigma e theta,
che indicheremo con la notazione
postfissa sigma theta,
e' semplicemente la composizione funzionale, cioe' la funzione definita
da:
(sigma theta)(x) = (x sigma) theta.
- Esempio
- Consideriamo le sostituzioni
sigma = {x/f(y), z/a} e
theta = {x/b, y/g(z), z/c}.
Avremo che sigma theta = {x/f(g(z)), y/g(z), z/a}.
- Proposizione
- La composizione di sostituzioni gode delle seguenti
proprieta':
-
t (sigma theta) = (t sigma) theta,
- (sigma theta) phi = sigma (theta phi)
(associativita')
- Prova
- Per esercizio.
Unificatori
- Definizione
- Consideriamo un sistema di equazioni di termini
E = {t1 =-= u1, t2 =-= u2, ... , tn =-= un}.
(Stiamo usando il simbolo =-= per sottolineare
la distinzione fra equazione e uguaglianza).
Una sostituzione sigma e' un
unificatore per
E se la sua applicazione ai termini di
E verifica simultaneamente tutte le equazioni,
ossia se vale che:
t1 sigma = u1 sigma, t2 sigma = u2 sigma, ... , tn
sigma = un sigma.
- Esempio
- Consideriamo l'equazione
f(x,y,g(z)) =-= f(a,w,w).
Abbiamo che le sostituzioni
sigma = {x/a, y/g(z), w/g(z)}
e theta = {x/a, y/g(b), z/b, w/g(b)} sono
unificatori per tale equazione.
La sostituzione
psi = {x/a, y/w, w/g(z)} non e' invece
un unificatore.
- Esempio
- L'equazione
x =-= f(x) non e' unificabile (cioe' non
ammette un unificatore),
infatti per poterla unificare occorrerebbe sostituire ad
x il termine infinito
f(f(f(...))).
Analogamente, anche l'equazione
g(y,y) =-= g(x,f(x)) non e' unificabile.
Most general unifier
- Definizione
- Dato un sistema di equazioni
E, una sostituzione sigma
e' un most general unifier (mgu) per
E se e solo se vale che:
- sigma e' un unificatore per
E,
- sigma e' piu' generale di ogni altro unificatore per
E, ossia: per ogni theta
che unifica E, esiste una sostituzione
phi tale che
theta = sigma phi.
- Esempio
- Nell'esempio precedente
dell'equazione f(x,y,g(z)) =-= f(a,w,w),
la sostituzione
sigma e' un most general unifier,
e theta invece non lo e'. Notare che
theta si ottiene da
sigma applicando a
quest'ultima la sostituzione
phi = {z/b}.
- Proposizione
- Se un sistema di equazioni
E e' unificabile (cioe' ammette un
unificatore),
allora esiste un mgu per
E. Inoltre, tutti i suoi mgu sono equivalenti,
cioe' si ottendono l'uno dall'altro tramite renaming.
(Un renaming e' una permutazione di variabili, cioe' una sostituzione da
variabili in variabili biunivoca).
Questa e' una proprieta' molto importante perche' ci assicura che tutte le
soluzioni di un sistema di equazioni si possono rappresentare in modo
compatto tramite una sola sostituzione.
Le nozioni di applicazione di sostituzione si estende nel modo ovvio
anche agli atomi, e cosi' pure le nozioni di unificatore, di mgu ecc.
Derivazioni
- Definizione
- Dato un programma logico
P, e un goal
G = <- A1, ... , An, consideriamo un
particolare atomo Ai in
G (atomo selezionato), e supponiamo che
esista una clausola H <- B1, ... , Bn
in P (eventualmente con variabili ridenominate
in modo da evitare confusione con quelle di G),
tale che Ai =-= H sia unificabile. Sia
sigma il suo mgu. Avremo allora che si puo'
effettuare un passo di computazione da G, ottenendo il goal
G' = <- ( A1, ... , Ai-1, B1, ... , Bn, Ai+1, ... ,
An ) sigma
Indicheremo tale passo di computazione con la seguente notazione:
G |-sigma-> G'
Notare che un passo di computazione corrisponde ad una inferenza logica:
G infatti rappresenta la negazione di
A1, ... , An, quindi la derivazione di
G' tramite la clausola
H <- B1, ... , Bn corrisponde ad effettuare
una specie di modus ponens con la formula equivalente
not(H) -> not(B1, ... , Bn).
- Definizione
- Una derivazione e' una sequenza di passi di computazione
G |-sigma1-> G1 |-sigma2-> G2 .... |-sigman-> Gn
Indicheremo questa derivazione anche con la notazione compatta
G |-sigma->* Gn, dove
sigma
e' la composizione di tutti gli mgu
sigma1 sigma2 ... sigman
ristretta alle
variabili del goal iniziale. Ometteremo sigma
quando questa e' vuota.
- Se Gn e' vuoto, la derivazione si dice di
successo (o refutazione), e
sigma e' detta computed
answer substitution (cas). Indicheremo una refutazione con la
notazione G |-sigma->* o (si dovrebbe
usare un quadratino, ma in mancanza di esso useremo il carattere
"o" per indicare il goal vuoto).
- Se Gn non e' vuoto, e non esiste nessuna
clausola, nel programma, la cui testa sia unificabile con l'atomo
selezionato, allora la derivazione e' detta di fallimento.
Notare che una derivazione di successo e' una specie di prova per assurdo,
e la cas dice quali sono i valori delle variabili del goal iniziale per cui
si ha una contraddizione col programma (ossia, la parte positiva del goal e'
conseguenza logica del programma).
Per quanto riguarda le computazioni di fallimento, notiamo che e'
ragionevole dichiarare "fallita" una computazione in cui non si riesce ad
andare avanti con un determinato atomo (atomo selezionato). Provare con un
altro atomo, infatti, non porterebbe comunque ad un successo. Se ad un
certo punto in un goal compare
un atomo non unificabile, infatti, tale atomo rimarra' presente anche nei
goal successivi della derivazione
(eventualmente istanziato con gli mgu dei passi di
computazione) e continuera' a non essere unificabile con nessuna delle
teste delle clausole. Cosi' non si arrivera' mai ad un goal vuoto.
- Esercizio
- Consideriamo il programma della lezione precedente, che definisce il
predicato sum
(somma di numeri naturali).
Provare che:
- Il goal <- sum(s(0),y,z) ha una sola
refutazione, con cas {z/s(y)}.
- Il goal <- sum(x,s(0),z) ha infinite
refutazioni, con cas {x/0, z/s(0)},
{x/s(0), z/s(s(0))}, ...
- Il goal <- sum(x,y,s(0)) ha due
refutazioni, con cas {x/0, y/s(0)} e
{x/s(0), y/0}.
Notiamo che una delle caratteristiche della programmazione logica e' quella di
poter manipolare strutture simboliche. Le strutture simboliche, cioe'
i termini, sono infatti i "tipi di dato primitivi" del linguaggio.
Vedremo in seguito che in programmazione logica
e' facile e naturale risolvere problemi di
manipolazione di formule simboliche, quali ad esempio il calcolo della
derivata di funzioni come sin (log x),
exp (5*x) , ecc.
In realta' anche in un linguaggio
come il Pascal si possono definire strutture che rappresentino
termini. Infatti i termini possono essere visti come alberi, e
quindi si possono implementare tramite records e puntatori. C'e'
pero' una cosa che nei linguaggi imperativi classici non si puo'
fare, o si puo' simulare solo molto artificiosamente, ed e' quella di
esprimere legami (simbolici) fra variabili o vincoli.
Ad esempio, la cas {z/s(y)} esprime un legame fra
y e z, che
rappresenta le infinite soluzioni {y=0, z=s(0)},
{y=s(0), z=s(s(0))}, ... .
Notare la differenza con la programmazione imperativa standard,
dove alle variabili possono solo essere assegnati valori del dominio dei dati,
cioe' oggetti
ground.
Un'altra interessante caratteristica della programmazione logica e' la
cosiddetta invertibilita' degli argomenti: quando definiamo un
predicato, non si stabilisce che certi argomenti sono "di input" e altri "di
output": tutti gli argomenti possono essere usati come input o come output
indifferentemente. Ad esempio, col programma della somma, posso scrivere
un goal <- sum(t,u,v) con
t e u istanziati a
termini ground, e v variabile, in modo da
calcolare in v il risultato della somma di
t e u. Oppure,
viceversa, posso avere t e
u variabili,
e v istanziato a termine ground,
in modo da calcolare tutti i possibili valori
per t e u
la cui somma faccia v.