MFI-Riscrittura (a.a. 2008-09)
Archivio E-Mail
Data: 24 aprile 2009
Subject: MFI (1)
Salve,
non ho avuto alcuna risposta alla mia precedente email. Quindi, assumendo che
chi tace acconsente, procedo con la "prima lezione" invitandovi comunque a
segnalare qualsiasi problema via email.
Riferimento: note "Sistemi di Riscrittura per Termini del Prim'Ordine"
(disponibile all'indirizzo
qui)
Considerato dove eravamo arrivati nell'ultima lezione in classe, ricominciamo
studiando il capitolo 4 (tutto) sui sistemi di riscrittura (srt) ed
il cap. 5 relativo alla terminazione degli srt.
Del cap.5 *non sono inclusi nel programma e quindi non occorre studiare* le
parti seguenti:
- Esempio 10
- prova di Prop. 7 (ma e' fondamentale sapere e capirne l'enunciato)
- la parte che comincia dopo Esempio 11 e si estende fino alla prova del Thm.3
(ovvero non facciamo lo sprofondamento e Thm. 2 e Thm. 3)
- prova di Prop.8
- tutta la Sezione 5.2
Osservazioni
1. Notate la somiglianza tra Def. 23 e Def. 13. La differenza consiste nel
poter usare una identita' sia come regola da sx a dx che da dx a sx (ovvero
il "viceversa" prima di Def.13), cio' non e' possibile nell'applicazione di
una regola di riscrittura, il cui orientamento e' fissato.
2. Notate inoltre in Def. 22 le chiusure rispetto a sostituzioni ed operazioni,
chiusure che abbiamo gia' visto nella deduzione della convertibilita' di
due termini e che giocano un ruolo importante anche nella definizione degli
ordinamenti di riduzione (Sez.5.1). Infatti queste chiusure sono
condizioni basilari per garantire la terminazione di un srt.
3. Quando si ha a che fare con proprieta' indecidibili in generale, come la
terminazione (e poi sara' il caso della confluenza e locale confluenza),
si cerca di trovare condizioni sufficienti che in un numero finito di passi
consentano di decidere se la proprieta' vale oppure no. Quindi, condizioni
che riguardano l'insieme dei termini, tipicamente infinito, non aiutano,
mentre si cercano condizioni sulle regole (che nel nostro caso saranno
sempre in numero finito) per poter decidere in un numero finito di passi.
Il teorema di Lankford fornisce tali condizioni e costituisce la teoria
alla base di ogni esercizio di terminazione che vi sara' chiesto di fare.
Nel nostro caso gli ordinamenti di riduzioni che potremo usare saranno solo
ordinamenti di semplificazione o rpo, ma in letteratura ne esistono molti
4. Cercate di capire perche' la proprieta' del sottotermine (la cui definizione
si e' rivelata ostica nelle prove orali dell'anno scorso) implica la
benfondatezza WF.
5. L'rpo e' un ordinamento "sintattico" basato su una relazione tra i simboli
che compaiono alla radice dei termini e poi ricorsivamente sugli argomenti,
in contrasto agli ordinamenti "semantici" basati sull'assegnamento di pesi
o precedenze agli operatori. Fate attenzione alle definizioni di >rpo e
di ordinamento su multinsiemi >>, che ultimamente alcuni vostri colleghi
non hanno saputo enunciare in modo corretto.
6. La clausola iv) dell'rpo generalizzato e' un caso particolare della
proprieta' del sottotermine, ma non si deve intendere la proprieta' del
sottotermine limitata solo al caso di sottotermine di tipo variabile.
Es. dato un ordinamento di semplificazione >, si ha che f(x,a) > a
per la proprieta' del sottotermine, dove a e' una costante
nella segnatura Sigma.
Vi inviero' alcuni esercizi svolti sulla terminazione degli srt non appena
possibile. Fatemi sapere via email per qualsiasi problema.
Saluti,
Monica Nesi