MFI-Riscrittura (a.a. 2008-09)
Archivio E-Mail

Data: 6 giugno 2009
Subject: MFI (4) - narrowing ed E-unificazione

Salve,

con questo messaggio vi invio alcune osservazioni relative alla "quarta macro-lezione", che ha come argomento l'E-unificazione basata su narrowing (Cap. 8 delle note sugli SRT fino a Sez.8.3 incluso).

L'ultimo argomento che affrontiamo nella parte del corso relativa alla teoria della riscrittura del I ordine e' l'unificazione semantica o E-unificazione, ovvero unificazione modulo una teoria equazionale E. La procedura di E-unificazione che consideriamo e' basata sul concetto di narrowing (una relazione di riduzione in un srt R diversa dalla riscrittura classica in R) e ha come ipotesi fondamentale il fatto che la teoria equazionale E ammetta un srt R equivalente canonico (quindi, tutta la teoria vista finora ci e' utile per garantire tale assunzione).

In precedenza abbiamo visto l'unificazione sintattica, ovvero la E-unificazione in cui E e' l'insieme vuoto. Dati due termini s,t, si ha che sigma e' una unificatrice sintattica di s e t sse (def) sigma(s) = sigma(t), dove = denota l'uguaglianza sintattica (ovvero i due termini devono essere esattamente uguali). L'unificazione semantica o E-unificazione (unificazione modulo una teoria equazionale E non vuota) e' un'estensione del concetto di unificazione. Dati due termini s,t ed una teoria equazionale E, una sostituzione sigma e' una E-unificatrice di s e t sse (def.) sigma(s) =E sigma(t), dove =E denota l'uguaglianza modulo la teoria E (ovvero un'istanza del problema della parola in E che noi sappiamo risolvere con una procedura di decisione nel caso in cui E ammetta un srt R equivalente canonico).

Il problema della E-unificazione sorge in vari contesti. Uno di questi e' dovuto all'esistenza di equazioni che non possono essere trasformate in regole di riscrittura, e.g. gli assiomi di tipo permutativo come la proprieta' commutativa f(x,y) = f(y,x) per un dato operatore f, in quanto cio' comprometterebbe la terminazione del sistema di regole risultante. In tal caso queste equazioni sono mantenute come tali (non vengono orientate) e si passa a considerare la "riscrittura modulo una teoria equazionale".
Quindi, supponiamo di avere una teoria equazionale T rappresentata tramite un srt R ed un insieme di equazioni E, non orientabili in regole o che si preferisce mantenere come equazioni. La riscrittura in T diventa "riscrittura in R modulo E" che puo' essere applicata secondo due approcci presenti nella letteratura (che sono stati poi mostrati equivalenti sotto determinate ipotesi):
1. un approccio basato su riscrittura tra classi di equivalenza di E;
2. un approccio basato sull'estendere le nozioni della riscrittura gia' viste alle corrispondenti nozioni "modulo E", ovvero E-match, E-unificazione ed E-unificatrici, completamento modulo E (dove le c.c. sono calcolate modulo E, ovvero cercando una E-unificatrice tra le regole), etc.
In particolare, di tutti questi concetti estesi modulo E noi studiamo solo l'E-unificazione, quindi l'estensione del concetto di unificazione da sintattica a semantica.

Il concetto di E-unificazione puo' essere visto anche come il problema della *risoluzione di equazioni modulo una teoria E*. Noi abbiamo visto che, se una teoria equazionale E ammette un srt R equivalente canonico, il problema della parola e' decidibile. La procedura di decisione consiste semplicemente nel ridurre i due termini del problema alla loro forma normale in R (che esiste ed e' unica per la canonicita' di R) e nel verificare l'uguaglianza sintattica di tali forme normali. Cio' vale per i termini chiusi, ovvero senza variabili, in T(Sigma).
Cosa significa invece considerare il problema della parola su termini aperti, ovvero termini con variabili, in T(Sigma,V)? Se due termini s,t con variabili risultano uguali modulo E secondo la procedura di decisione applicata per i termini chiusi, significa che s e t sono uguali in E "per ogni valore" che le variabili in s e t possono assumere. In altre parole, s =E t e' un'equivalenza vera in E per ogni valore delle variabili. Quindi, rimpiazzando le variabili in s e t con qualsiasi termine (e cio' significa applicare una sostituzione sulle variabili), si ottengono termini (eventualmente chiusi) uguali modulo E.

Consideriamo la teoria E che formalizza la funzione somma sui numeri naturali su una segnatura Sigma = {0,s,+}:
+(0,x) = x
+(s(x),y) = s(+(x,y))
Completando la teoria E rispetto ad un rpo basato sulla precedenza + > s, si ha che l'srt R ottenuto orientando le due equazioni da sx a dx risulta canonico (in particolare, non esistono coppie critiche). Quindi, si ha R:
+(0,x) -> x
+(s(x),y) -> s(+(x,y))

1) Siano dati i termini chiusi t1 = s(s(+(0,0))) e t2 = +(s(0),s(0)). Per determinare se t1 =E t2, calcoliamo le f.n. in R di t1 e t2. Si ha:
t1 = s(s(+(0,0))) -> s(s(0)) f.n.
t2 = +(s(0),s(0)) -> s(+(0,s(0))) -> s(s(0)) f.n.
Le due f.n. sono uguali, per cui t1 =E t2.

2) Siano dati i termini con variabili t1 = s(+(s(0),x)) e t2 = +(s(0),s(x)). Per determinare se t1 =E t2, si ha:
t1 = s(+(s(0),x)) -> s(s(+(0,x))) -> s(s(x)) f.n.
t2 = +(s(0),s(x)) -> s(+(0,s(x))) -> s(s(x)) f.n.
Le due f.n. sono sintatticamente uguali, per cui t1 =E t2 e' vera *per ogni* assegnamento (o sostituzione) sigma su x. Il ragionamento puo' essere banalmente generalizzato a termini con piu' di una variabile.

3) Siano date le seguenti coppie di termini con variabili:
- t1 = +(x,x) e t2 = s(s(0));
- t1 = +(x,y) e t2 = s(0);
- t1 = +(x,y) e t2 = +(s(0),x); etc.

Per determinare se t1 =E t2, si ha che i termini sono gia' in f.n. in R (solo il terzo t2 e' riducibile e si ottiene s(x)) e le f.n. di t1 e t2 non sono uguali sintatticamente. Quindi, t1 =E t2 non e' vera per ogni termine sostituito alle variabili. Non si hanno equivalenze o identita' vere in E, ma "equazioni da risolvere in E". Il problema non e' piu' il problema della parola, ma e' il problema della risoluzione di equazioni modulo una teoria E, ovvero determinare *se esistono* dei termini che rimpiazzati alle variabili di t1 e t2 rendono vera l'equazione t1 =E t2. In altre parole, occorre determinare *se esiste* una sostituzione sigma sulle variabili in t1 e t2 tale che sigma(t1) =E sigma(t2). Quest'ultima equazione costituisce la definizione di sigma come E-unificatrice di t1 e t2 ed e' un'equazione che rientra nei casi 1 e 2 visti sopra.
Consideriamo t1 = +(x,y) e t2 = s(s(0)). Esistono tre soluzioni per l'equazione t1 =E t2, date dalle seguenti E-unificatrici: sigma1 = {s(0)/x, s(0)/y}, sigma2 = {0/x, s(s(0))/y}, sigma3 = {s(s(0))/x, 0/y}. Per verificare che queste sostituzioni sono delle E-unificatrici, basta controllare che valga sigma(t1) =E sigma(t2) per ogni sost. sigma. Per esempio, per sigma1 occorre verificare sigma1(t1) =E sigma1(t2), ovvero il problema della parola +(s(0),s(0)) =E s(s(0)). Il secondo termine e' gia' in f.n. in R, il primo termine viene ridotto alla stessa f.n. in R applicando in successione la seconda e la prima regola di R.

Questo esempio anticipa il fatto che nella E-unificazione non esiste l'unicita' della E-unificatrice piu' generale. Le tre sostituzioni sigma1, sigma2 e sigma3 sono inconfrontabili tra loro. In generale, due termini E-unificabili avranno un insieme di E-unificatrici piu' generali.

A questo punto si passa alle Def. 34, 35 e 36 che estendono i concetti di match, unificatrici, unificazione, etc. al caso "modulo E". Nell'Esempio 25, guardate solo i primi due casi, tralasciate l'esempio di Huet che non mi sembra funzionare.

Si passa quindi a dare un algoritmo per l'E-unificazione, che e' un problema in generale indecidibile. Tale problema diventa semidecidibile se la teoria E ammette un srt R equivalente canonico (e quindi ritroviamo delle condizioni per le quali abbiamo studiato la teoria nelle lezioni precedenti).
La procedura che studiamo noi si basa sul concetto di narrowing (Def. 37). L'idea e' la seguente: per poter risolvere equazioni con variabili, occorre lavorare *anche sulle variabili dei termini dell'equazione* e non solo (come fatto finora con la relazione di riscrittura e le sostituzioni di match) sulle variabili delle regole applicate. Pertanto, abbiamo bisogno di un concetto di riduzione diverso dalla riscrittura classica, che verifica se in un termine esiste un'istanza del lato sx di una regola, per passare ad una trasformazione dei termini in cui anche le variabili di tali termini possano essere sostituite in modo da rendere i termini istanziati riducibili tramite le regole di un srt R. Si passa cosi' dalle sostituzioni di match alle sostituzioni unificatrici tra lato sx di una regola di R ed un sottotermine del termine da ridurre. In termini di paradigmi di programmazione, cio' vuol dire passare dalla programmazione funzionale (basata sulla riscrittura classica ed il pattern matching) alla programmazione logica (basata sull'unificazione). Gli studenti che hanno sostenuto l'esame di Intelligenza Artificiale, avranno studiato un po' di programmazione e di deduzione logica basata sul metodo della risoluzione, che usa l'unificazione (la Sez. 8.5 delle note sugli SRT presenta un breve confronto tra la risoluzione SLD e la procedura di E-unificazione basata su narrowing).

N.B. Dato un srt R, la relazione di riscrittura ->R in R e' un caso particolare della relazione di narrowing /\->R in R, in quanto per sostituzioni non cicliche un match e' un caso particolare di unificatrice. Confrontando la Def.37 di narrowing e la Def.23 di riscrittura, si notano le differenze: nel narrowing la sostituzione da cercare e' l'mgu tra il lato sx l ed il sottotermine t|p invece che un match, mentre il termine risultante dal passo di riduzione, oltre al rimpiazzamento effettuato alla posizione p, in generale risente dell'applicazione dell'mgu anche nel contesto intorno a t|p (cio' non avviene invece nella riscrittura in quanto le variabili del termine t non appartengono al dominio della sostituzione di match che rimpiazza solo variabili della regola applicata).

Assumendo che la teoria E ammetta un srt R equivalente canonico, l'idea della procedura di E-unificazione basata su narrowing e' la seguente. Siano s, t termini di cui dobbiamo verificare se sono E-unificabili, ovvero se esiste sigma sostituzione tale che sigma(s) =E sigma(t). Prima di tutto, visto che le nostre definizioni di riduzione di termini vedono coinvolto sempre un solo termine, utilizziamo un nuovo simbolo || che non appartiene alla segnatura Sigma per poter scrivere il goal iniziale come il termine ||(s,t). Ovviamente, poiche' || non sta in Sigma e quindi non vi sono regole in R che riducono termini con || in testa, un termine che comincia con || non potra' mai ridursi in posizione epsilon.
Nelle Sez. 8.2 e 8.3 cancellate l'asterisco * sopra la riduzione di narrowing, non consideriamo zero o piu' passi di riduzione ma semplicemente un passo di narrowing per volta.
Nella procedura si parte con il goal iniziale ||(s,t), il suo insieme di posizioni non di variabili (vedi la def. di narrowing) ed una sostituzione vuota o identita'. L'idea e' applicare passi di narrowing in R sul termine ||(s,t) fino ad ottenere una soluzione (successo) o fallimento (termini non E-unificabili) o continuare all'infinito alla ricerca di soluzioni (il problema e' semidecidibile). Poiche' i passi di narrowing applicabili su un dato goal possono essere piu' di uno in posizioni uguali con regole di R diverse oppure in posizioni diverse, la procedura da' luogo ad un albero di derivazioni di narrowing possibilmente infinito in lunghezza (ma finito in ampiezza) con il goal iniziale ||(s,t) alla sua radice.

Siano ||(s_i,t_i) il goal corrente al passo i, Pos_i l'insieme delle posizioni e sigma_i la sostituzione corrente. Si hanno tre casi:
1. s_i e t_i unificano *sintatticamente* con mgu teta. In questo caso i termini iniziali s e t sono E-unificabili ed una E-unificatrice e' ottenuta componendo teta con sigma_i.
2. s_i e t_i non unificano sintatticamente e non e' possibile applicare alcun passo di narrowing su nessuna delle posizioni in Pos_i (ovvero nessun sottotermine individuato dalle posizioni in Pos_i e' unificabile sintatticamente con il lato sx di una regola di R). Cio' significa che in base al cammino che da ||(s,t) ha portato a ||(s_i,t_i), i termini s e t non sono E-unificabili. Per cercare altre possibili soluzioni occorre esaminare gli altri cammini dell'albero di derivazione di narrowing.
3. s_i e t_i non unificano sintatticamente e ||(s_i,t_i) e' riducibile tramite narrowing con una regola di R mediante l'mgu sigma. Si ottiene un nuovo goal ||(s_i+1,t_i+1) tramite l'applicazione del passo di narrowing ed una nuova sostituzione data dalla composizione di sigma con sigma_i.

Come afferma il Thm.10 di correttezza e completezza della procedura di E-unificazione definita da Fay, Hullot e Lankford, le E-unificatrici di s e t calcolate dalla procedura non sono altro che la composizione di tutte le mgu dei passi di narrowing calcolate lungo i cammini che portano ad una soluzione. Ovviamente, come succede nella risoluzione di equazioni in un qualsiasi dominio, puo' succedere che una equazione abbia un insieme finito di soluzioni (in particolare puo' avere una sola soluzione) oppure puo' avere un insieme infinito di soluzioni (che possono eventualmente essere caratterizzate in maniera finita) oppure puo' non avere soluzioni (quindi tutti i cammini dell'albero terminano con fallimento o vanno all'infinito chiudendosi con fallimento).

Notare come questa procedura di E-unificazione (o unificazione semantica) si basi sull'unificazione sintattica tramite il calcolo di mgu per l'applicazione dei passi di narrowing e per il passo di terminazione con successo.

L'ultima osservazione sulla procedura riguarda due sue possibili ottimizzazioni, che sono state provate corrette e complete da Hullot. Facendo alcuni esercizi di E-unificazione (tipicamente il secondo esercizio dato in una prova scritta d'esame) dovreste accorgervi presto che la procedura considerata e' "cieca" e non applica alcuna strategia particolare per ottimizzare il calcolo ne' e' in grado di "tagliare" i cammini che portano al fallimento all'infinito, in quanto questa versione della procedura non prevede strumenti per accorgersi quando e' inutile continuare ad applicare passi di narrowing all'infinito, passi che non porteranno ad alcuna soluzione.
Possiamo pero' includere due semplici ottimizzazioni. Si parla di:
- narrowing "normale" se il passo di narrowing viene applicato solo su termini in formale normale rispetto ad R. Cio' significa che, prima di vedere se e' possibile applicare un passo di narrowing, si normalizza il goal corrente riscrivendolo in f.n. in R (notare che comunque un passo di riscrittura e' un particolare passo di narrowing).
- narrowing "basilare" se le posizioni del goal corrente su cui applicare passi di narrowing non sono semplicemente le posizioni non di variabile del goal corrente, ma sono definite come specificato alla fine della Sez.8.3. Tale definizione prevede che al passo iniziale Pos_0 sia l'insieme della posizioni non di variabile del goal iniziale. Se al passo i si e' applicato un passo di narrowing sulla posizione p di Pos_i con la regola l->r di R, l'insieme Pos_i+1 di posizioni su cui lavorare al passo successivo e' dato da:

Pos_i+1 = Pos_i \ {q | p prefisso di q} U {p.q | q in Pos'(r)}

ovvero Pos_i+1 e' ottenuto da Pos_i togliendo tutte le posizioni sotto alla posizione p e aggiungendo tutte le posizioni del tipo p.q dove q e' posizione non di variabile del lato dx r della regola applicata. L'idea e' che non occorre considerare le posizioni non di variabile del termine istanziato sigma(r), dove sigma e' l'mgu del passo di narrowing, ma solo quelle di r. Quindi, nel narrowing basilare non si applicano passi di narrowing su sottotermini che derivano da passi precedenti di narrowing per istanziazioni di variabili delle regole applicate. A seconda del problema di unificazione, il narrowing basilare potra' coincidere con il narrowing basato sulle usuali posizioni non di variabile. In alcuni esercizi invece potra' capitare di avere una certa riduzione dello spazio di ricerca rappresentato dall'albero di derivazione di narrowing, perche' l'insieme delle posizioni basilari e' effettivamente ristretto rispetto a quello usuale con le posizioni non di variabile.

Il programma della parte del corso relativa alla riscrittura termina con le posizioni basilari, ovvero fino alla Sez. 8.3 inclusa.
Gli studenti che hanno studiato Intelligenza Artificiale sono invitati a leggere la Sez.8.5 dove viene presentato un breve confronto tra E-unificazione basata su narrowing ed SDL-risoluzione.

Seguiranno a breve alcuni esercizi di E-unificazione basata su narrowing.

Saluti,
Monica Nesi