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.