MFI-Riscrittura (a.a. 2008-09)
Archivio E-Mail
Data: 4 maggio 2009
Subject: MFI (2) - Locale confluenza e coppie
critiche
Salve,
con questo messaggio vi invio alcuni dettagli relativi alla "seconda lezione",
che ha come argomento il concetto fondamentale di coppia critica.
Riferendomi sempre alle note "Sistemi di Riscrittura per Termini del
Prim'Ordine",
si tratta di studiare tutto il capitolo 6, tranne la prova del Lemma di Huet.
Come forse saprete, la prova del Lemma di Huet negli ultimi anni accademici ha
sempre fatto parte del programma del corso di MFI, in quanto interessante come
tecnica di prova e chiarificatrice del legame tra coppia critica e locale
confluenza. Tuttavia, considerata la situazione di questo periodo, ho deciso di
eliminare tale prova dal programma di MFI per l'a.a. 2008-09. D'altra parte
pero' vi invito comunque a leggerla, e faro' qualche breve commento su di essa
alla fine di questa email.
Quindi, dopo aver visto la terminazione negli srt ed alcuni ordinamenti per
decidere tale proprieta', passiamo a considerare alcuni strumenti per verificare
l'altra proprieta' di interesse, ovvero la confluenza. In realta', noi non
verificheremo direttamente la confluenza di un srt R ma, sfruttando il Lemma
di Newman, cercheremo di verificare la locale confluenza di R.
Quindi, le situazioni che considereremo saranno sempre del seguente tipo:
dato un srt R, prima verifichiamo se R e' terminante rispetto ad un qualche
ordinamento di riduzione. Se R risulta terminante, in base al Lemma di Newman
la verifica della confluenza viene ricondotta alla verifica della locale
confluenza.
Il Lemma 1 di Cap.6 fornisce una *procedura di decisione* per la convertibilita'
o uguaglianza in una teoria E descritta tramite un srt R:
se occorre decidere se due termini s,t sono convertibili in R e si ha che R
e' terminante e confluente, allora basta calcolare la forma normale di s e t
(che esiste ed e' unica, essendo R canonico) e poi controllare se la f.n. di
s e la f.n. di t sono sintatticamente uguali. Se lo sono, s e t sono
convertibili in R.
Quindi vediamo come affrontare la verifica della locale confluenza.
Vale lo stesso
approccio visto per la terminazione. La locale confluenza e' una proprieta' in
generale indecidibile, la cui definizione si basa sul controllare la convergenza
(ovvero la riduzione ad uno stesso termine tramite -*->) dei picchi di locale
confluenza (ovvero a -> b ed a -> c per ogni a,b,c) che in generale possono
essere un numero infinito. Pertanto si cercano condizioni sufficienti che in un
numero finito di passi consentano di derivare se un srt R e' localmente
confluente.
Come puo' succedere che un termine t possa ridursi in due modi diversi? Cio'
succede se esistono in t due redessi per due regole di R (o per la stessa regola
con redessi in posizioni diverse), ovvero t puo' essere visto come un contesto
C1 che contiene un'istanza del lato sinistro l1 di una regola l1 -> r1 di R ed
anche come un contesto C2 che contiene un'istanza del lato sinistro l2 di
un'altra
regola l2 -> r2 di R. In altre parole, t puo' essere visto come la chiusura
rispetto a sostituzioni e operazioni (o contesti) dei lati sinistri di regole di
R. Ecco che si introduce il concetto di spectrum di R come l'insieme di tutte
le possibili istanze del lato sinistro di una regola di R. Se due elementi dello
spectrum di R (ovvero, due termini che sono istanze di due lati sinistri
diversi)
sono uguali, questi individuano un termine che si riscrive in due modi diversi,
ovvero il vertice di un picco di locale confluenza. Questo termine si riscrive
con due regole "in testa", cioe' in posizione epsilon, per cui questa e' una
situazione semplificata.
La situazione piu' generale e' data da un termine che si riscrive in due modi
diversi in posizione non in testa, ovvero si ha non solo la chiusura rispetto
alle sostituzioni (che e' cio' che fa lo spectrum), ma anche chiusura rispetto
ai contesti (quindi, redessi non necessariamente in testa).
In altre parole, se t si riscrive in due modi diversi, significa che due regole
si intersecano o sovrappongono tra di loro all'interno di t. Da qui segue
un criterio per la locale confluenza basato sul controllare se le regole di
R si sovrappongono tra loro (overlapping o superposition) verificando se
esistono unificazioni tra i lati sinistri delle regole.
Cio' da' luogo al calcolo della "coppia critica" (c.c.), che e' una coppia
di termini corrispondenti ai vertici in basso di un picco di locale confluenza
e che e' detta "critica" in quanto puo' compromettere la locale confluenza
se i due termini non convergono ad uno stesso termine. I termini della c.c.
sono i termini risultanti dall'applicazione di due regole di R che si
sovrappongono, a partire dal termine piu' generale che si puo' riscrivere
con tali regole.
Alcune osservazioni sulla definizione di coppia critica:
1. La condizione di intersezione vuota tra gli insiemi di variabili delle
regole serve per non perdere possibili unificazioni. Tale condizione puo'
essere sempre ottenuta ridenominando opportunamente le variabili delle regole.
2. La condizione che p deve essere una posizione non di variabile esclude
i casi in cui il lato sinistro di una regola unifica con una variabile di
un'altra regola (cosa sempre possibile che farebbe esplodere il numero di
c.c. inutilmente, in quanto non e' un caso critico come evidenziato
dalla prova del Lemma di Huet).
3. Il termine teta(l1) e' un'istanza di l1, quindi si riduce con la regola
l1 -> r1 in posizione epsilon ottenendo teta(r1), ma per def. di c.c. nella
posizione p esiste un'istanza teta(l2) riducibile con la regola l2 -> r2
ottenendo teta(l1)[teta(r2)]p. Il termine teta(l1)[teta(r2)]p puo' essere
scritto anche come teta(l1[r2]p).
4. La mgu presente nella def. di c.c., chiamata teta nella dispensa, puo'
essere vista come la composizione delle due sostituzioni di match corrispondenti
ai due passi di riscrittura che originano da teta(l1).
5. Le c.c. individuano le situazioni piu' generali (tramite l'applicazione
di una mgu e non una qualsiasi unificatrice) in cui un termine puo' riscriversi
in piu' modi diversi.
Nell'ipotesi di un srt R con un numero finito di regole, il numero di c.c. e'
possibilmente grande ma finito. Quindi il controllo di una qualche proprieta'
sulle c.c. puo' essere fatto in tempo finito. Pertanto l'idea e' di ridurre
la verifica della locale confluenza ad un controllo sulle c.c. tra le regole
di R. Il Lemma di Huet fa proprio questo mostrando che un srt R e' localmente
confluente se e solo se tutte le sue c.c. sono convergenti.
Importante: notare che nel Lemma di Huet non vi e' alcuna ipotesi di
terminazione di R.
Qualche breve commento sulla prova del Lemma di Huet (che comunque non sara'
argomento di esame):
La dimostrazione dell'implicazione "tutte le c.c. di R sono convergenti =>
R e' localmente confluente" (l'altra implicazione segue banalmente dalla def.
di locale confluenza) considera i vari casi in cui si possono avere picchi di
locale confluenza, ovvero un termine che si riscrive in due modi diversi.
Se i due passi di riscrittura operano su redessi indipendenti o disgiunti tra
loro (caso 1), si tratta di un non determinismo innocuo (ed infatti questo
caso non viene fuori con le c.c.) ed il picco converge applicando l'altra
riduzione sul redesso rimasto inalterato dopo la prima riduzione.
Se i redessi sono invece annidati, ovvero uno o piu' redessi (interni) si
trovano all'interno dell'altro (esterno) ed istanziano (eventualmente con un
contesto) una o piu' variabili del lato sinistro della regola che riduce
il redesso esterno (caso 2), anche in questo caso il picco di locale confluenza
si chiude tramite l'applicazione delle due regole.
Esempio: siano dati
1. f(x,x) -> x
2. g(x) -> a
ed il termine t = h(f(k(g(y)),k(g(y))),c). Si ha t -> t1 = h(k(g(y)),c) con
la regola 1 e t -> t2 = h(f(k(a),k(g(y))),c) con la regola 2 sul primo dei
due redessi interni. Il redesso g(y) per la regola 2 dentro al contesto k[]
da' luogo al termine k(g(y)) che istanzia la variabile x della regola 1.
La regola 1 ora non e' applicabile su t2, ma lo diventa se riscriviamo gli
altri redessi interni (in questo caso ve ne e' solo uno) con la 2 ottenendo
t2 -> h(f(k(a),k(a)),c) -> h(k(a),c). Questo termine e' raggiunto anche a
partire da t1 applicando la regola 2 (in quanto il lato destro della regola
1 ha un'occorrenza della variabile x) chiudendo cosi' il picco.
Notare che se la regola 1 contiene a destra piu' occorrenze di x, occorre
applicare piu' volte la regola 2 (la si applica zero volte se la variabile
x non compare nel lato destro della prima regola).
Sovrapposizioni di questo tipo (ovvero su variabile) non sono critiche e
non vengono fuori con la def. di c.c.
Il terzo caso e' invece quello piu' complesso e piu' difficile da rappresentare
graficamente, ovvero il caso di redessi sovrapposti individuato dalla def.
di c.c. e in cui si sfrutta l'ipotesi di convergenza delle c.c.
Vi inviero' alcuni esercizi svolti sul calcolo di coppie critiche di srt
non appena possibile. Fatemi sapere via email per qualsiasi problema.
Saluti,
Monica Nesi