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

Data: 19 maggio 2009
Subject: MFI (3) - Completamento di teorie equazionali

Salve,

con questo messaggio vi invio alcune osservazioni relative alla "terza macro-lezione", che ha come argomento il completamento di teorie equazionali (Cap. 7 delle note sugli SRT).

Il problema e' sempre quello di definire degli strumenti (basati sulla teoria della riscrittura del prim'ordine) per poter rispondere al "word problem", i.e. il problema della parola in una teoria equazionale: dati (gli assiomi di) una teoria equazionale E e due termini s,t, si vuole determinare se s = t modulo E, scritto anche E |- s = t oppure s =E t. Nel rispondere a tale problema, l'obiettivo e' cercare di evitare di usare le equazioni di E in favore di regole di riscrittura (ovvero equazioni orientate) derivate da E (in tal modo, le regole sono corrette rispetto al ragionamento equazionale in E) che consentano di ottenere gli stessi risultati che si avrebbero usando la teoria E (quindi, regole complete rispetto alle derivazioni in E).
Quindi si cerca di avere un srt R "equivalente" ad E nel senso descritto dalla Def. 33, ovvero un R tale che la convertibilita' in R coincida con l'equivalenza in E. Cio' significa che, se per ogni coppia di termini s, t convertibili in R si ha che s e t sono uguali modulo E e, viceversa, dati due termini uguali modulo E, questi sono convertibili in R, allora R ha lo stesso *potere deduttivo* di E (e' equivalente ad E) e quindi puo' essere usato al posto di E per derivare le equivalenze in E.
Se, oltre ad essere equivalente ad E, l'srt R e' anche canonico (i.e., terminante e confluente), in base al Lemma 1 del Cap. 6 (che fornisce una procedura di decisione per la convertibilita' in R) si ha che il problema della parola in E diventa decidibile. Cio' e' quanto espresso dal Teorema 8.
Quindi, nel caso in cui una teoria E ammetta un srt R equivalente e canonico, vorremo capire come sia possibile ottenere tale srt a partire da E. Il Teorema 9, detto anche Teorema di Knuth-Bendix (dai nomi di coloro che per primi hanno scritto un "algoritmo di completamento"), mette insieme i due risultati dati dal Lemma di Newman e dal Lemma di Huet. Notare una imprecisione nella dimostrazione di tale teorema: nella prima frase della dimostrazione "Se il sistema e' SN e tutte le sue cc sono convergenti..." togliere l'ipotesi "il sistema e' SN", in quanto il Lemma di Huet non ha alcuna ipotesi di terminazione e la frase scritta in questo modo potrebbe generare confusione. L'ipotesi "il sistema e' SN" va spostata all'inizio della seconda frase della dimostrazione, quando si usa il Lemma di Newman.

Per trovare un srt R equivalente ad una teoria E che sia anche canonico, si puo' applicare una "procedura di completamento" in cui si assume di avere un srt terminante e quindi ci si concentra sul problema della verifica della confluenza. Tipicamente, nei primi passi di tale procedura l'srt R puo' essere visto come costituito dalle regole ottenute orientando gli assiomi in E rispetto ad un ordinamento di riduzione che garantisce la terminazione di R.
N.B. Ogni procedura di completamento dipende da un ordinamento di riduzione, ovvero quando si completa una teoria E o un srt R lo si fa sempre *rispetto ad un dato ordinamento di riduzione*, che quindi e' un dato di input della procedura di completamento insieme alla teoria E. Puo' accadere che il completamento di una stessa teoria o di uno stesso srt rispetto a ordinamenti di riduzione differenti dia luogo a risultati molto diversi. Ad esempio, il completamento di una data teoria puo' fallire rispetto ad un certo ordinamento di riduzione, mentre termina con successo se svolto rispetto ad un altro ordinamento piu' potente.

La proprieta' di terminazione dell'srt R viene preservata da ogni passo della procedura di completamento e, data tale ipotesi, per il Lemma di Newman la verifica della confluenza si riduce alla verifica della locale confluenza. Quindi, dato un srt R terminante ma non localmente confluente, si cerca di ottenere un srt R' terminante, equivalente ad R (ovvero le relazioni di convertibilita' sono equivalenti) e localmente confluente. Per il Lemma di Huet si calcolano le coppie critiche di R e si controlla se sono convergenti nell'srt R corrente.
Se tutte le c.c. di R convergono, R e' WCR e quindi, essendo terminante, e' confluente e canonico.
Se esistono c.c. di R non convergenti, che quindi compromettono la locale confluenza di R, queste vengono aggiunte ad R come nuove regole ottenute orientando le c.c. rispetto all'ordinamento di riduzione dato. Il completamento consiste infatti nell'aggiungere queste nuove regole derivate da c.c. per recuperare la perdita di potere deduttivo che si puo' avere quando si orientano gli assiomi di E in regole di riscrittura (in quanto non si ha piu' la possibilita' di usare la chiusura simmetrica della relazione di equivalenza).
L'aggiunta di una regola derivata da c.c. e' corretta rispetto alla convertibilita' in R in quanto gli elementi s,t di una c.c. (s,t) sono convertibili tra loro, ovvero sono uguali modulo E.
Ad ogni passo i della procedura di completamento, le c.c. dell'srt corrente R_i sono in numero finito, ma le nuove regole derivate da c.c. possono dar luogo a nuove c.c. al passo successivo e cosi' via. Cio' puo' accadere all'infinito e portare cosi' alla non terminazione della procedura di completamento, detta anche *divergenza* del completamento.
In tal caso, studiando il modo in cui si genera la divergenza, si puo' anche riuscire a stabilire la regola o le regole che, sovrapponendosi sulle altre o su se stesse, generano un completamento infinito. Tale regola (o regole, se piu' di una) da' luogo al cosidetto "pattern di divergenza" (vedremo poi qualche esercizio sulla divergenza del completamento).
La terminazione con fallimento si ha tipicamente quando si trova un'equazione in E o una c.c. di R che non puo' essere orientata rispetto all'ordinamento di riduzione dato.
La terminazione con successo si ha quando tutte le equazioni (incluso le eventuali c.c. non convergenti) sono state orientate e/o tutte le c.c. sono convergenti, per cui non si hanno piu' equazioni (E_i = {}) e l'srt R_i e' canonico.
Le procedure di completamento possono essere diverse in quanto diverse, piu' o meno ottimizzate o efficienti, etc., possono essere le strategie usate nell'applicare le regole di inferenza che definiscono il completamento (piu' avanti vedremo due di queste strategie). Infatti, le regole del completamento date in Fig.2 possono essere applicate non deterministicamente, anche se in modo "fair", ovvero prima o poi una regola che risulta sempre applicabile deve essere applicata.

Qualche commento sulle regole basilari del completamento.
- Orienta non fa altro che orientare le equazioni di E (incluso le c.c. di R) in regole, se si riesce a provare che un lato dell'equazione e' maggiore dell'altro rispetto all'ordinamento di riduzione dato.
- Fallimento e' la regola che decreta la terminazione con fallimento della procedura se un'equazione non e' orientabile rispetto all'ordinamento di riduzione dato.
- Cancella elimina le equazioni che sono identita'.
- Normalizza (a sx, a dx) riduce tramite le regole di R il lato sx e il lato dx (rispettivamente) delle equazioni in E, se questi sono riducibili (in modo da mantenere le equazioni in forma ridotta rispetto ad R ed eventualmente trasformarle in identita' da eliminare).
- Uguaglia calcola le c.c. di R e le aggiunge come equazioni in E (da cui saranno poi selezionate per essere eventualmente ridotte tramite Normalizza e/o cancellate con Cancella oppure orientate in nuove regole tramite Orienta).

Le ulteriori regole (non basilari) Componi e Collassa hanno lo scopo di normalizzare il lato dx ed il lato sx delle regole dell'srt R, ovvero consentono di mantenere le regole di R in forma intraridotta rispetto ad R stesso, cosi' come le due versioni della regola Normalizza consentono di mantenere le equazioni di E in forma ridotta rispetto ad R. Componi tratta il caso in cui il lato dx r di una regola l -> r di R puo' essere ridotto in R ottenendo r'. In tal caso si puo' semplicemente rimpiazzare l -> r in R con l -> r'. La regola Collassa considera il caso piu' delicato in cui ad essere riducibile in R e' il lato sx l di una regola l -> r di R. Questo caso e' formalizzato utilizzando un ordinamento benfondato sulle regole, ma l'importante e' capire che questa situazione non puo' essere gestita come quella trattata da Componi, ovvero non si puo' direttamente rimpiazzare l -> r in R con l' -> r dove l' e' il termine ottenuto riducendo l tramite R (in quanto non e' detto che l' sia maggiore di r nell'ordinamento di riduzione dato). Collassa dice che in questo caso si elimina l -> r da R e si aggiunge l' = r alle equazioni di E, in quanto occorre gestire l' = r come equazione, di cui verificare l'eventuale orientamento o cancellazione.

Negli esercizi che svolgeremo cercheremo sempre di applicare il piu' possibile anche le regole non basilari Componi e Collassa per mantenere l'srt R in forma intraridotta. Due possibili strategie per l'applicazione dei passi del completamento sono le seguenti:

nr-complete = (Cancella*.(Orienta + Fallimento)*.Uguaglia*)*

complete = (((Cancella + Normalizza)*. (Orienta + Fallimento). (Componi + Collassa)*)*. Uguaglia*)*

dove r* denota l'iterazione della regola di inferenza r fintantoche' r e' applicabile, r1 + r2 denota la scelta non deterministica tra r1 ed r2, ed r1.r2 denota l'applicazione della regola r1 seguita dalla regola r2. L'applicazione della regola Fallimento determina la terminazione con fallimento dell'intera procedura di completamento. La strategia nr-complete (nr = non-reducing) esegue il completamento iterando solamente l'applicazione delle regole Cancella per l'eliminazione di identita', Orienta per l'orientamento delle equazioni ed Uguaglia per il calcolo delle c.c. Quindi non esegue alcuna intrariduzione sulle equazioni e/o sulle regole. La strategia complete provvede invece ad effettuare anche normalizzazioni tramite R sia sulle equazioni in E tramite Normalizza che sulle regole stesse di R tramite Componi e Collassa. Le c.c. vengono calcolate su regole normalizzate quando non vi sono altre regole di inferenza del completamento da applicare.

Cerchero' di inviarvi al piu' presto alcuni esercizi svolti di completamento di teorie equazionali, oltre ad un esempio di completamento divergente.

Saluti,
Monica Nesi