per la specifica, l'analisi, la verifica, la sintesi e
la trasformazione di sistemi
software.
Università degli studi di Roma Tor Vergata
Dipartimento di Informatica, Sistemi e Produzione
Responsabile: Alberto Pettorossi
Ammontare del Finanziamento disponibili lire
10,100,000
acquisibili lire 6,200,000
cofinanziamento richiesto lire 20,700,000
Fondi disponibili e acquisiti per il primo anno:
lire 10,100,000
Illustrazione dell'attivita' svolta
-----------------------------------
Relazione scientifica.
Il lavoro sviluppato dall'Unita' di Roma Tor Vergata
si e' incentrato in modo
particolare sulla trasformazione, sulla specializzazione
e sulla sintesi dei
programmi logici.
Per quanto riguarda la trasformazione
e la specializzazione e' stato prodotto
un lavoro (vedasi [1]) di rassegna e risistemazione
organica dei risultati
noti nella letteratura. Abbiamo considerato
in particolare la tecnica di
trasformazione basata se `regole e strategie'.
Ci siamo interessati dapprima
ai `definite logic programs'.
Sono state considerate le seguenti
regole : (i) introduzione di una
definizione (con predicati che possono essere ricorsivi),
(ii) eliminazione
di una definizione, (iii) unfolding, (iv) folding,
(v) rimpiazzamento di goal
in una data clausola, (vi) rimpiazzamento di clausola.
Quest'ultima regola
viene usata per il riordinamento delle clausole,
l'eliminazione di clausole
sussunte, l'eliminazione di clausole con un body
che fallisce finitamente, la
generalizzazione + l'introduzione di eguaglianze.
Sono state considerate diverse
semantiche e in particolare, la semantica del
least Herbrand model, la semantica delle computed
answers substitutions, la
semantica del fallimento finito, e la semantica del
Prolog puro. Per ognuna
di queste semantiche e per un dato insieme di regole
di trasformazione
abbiamo indicato vari teoremi di correttezza per
sequenze di programmi
generati da queste regole.
I teoremi di correttezza sono
della forma seguente: dato un insieme R di
regole, se una sequenza di programmi e'costruita
attraverso R allora la
semantica del programma iniziale e' uguale alla semantica
del programma del
programma finale della sequenza considerata.
Nel lavoro di rassegna abbiamo
indicato anche delle versioni dei teoremi di
correttezza che permettono l'uso della regola di
folding rispetto alle
definizioni di predicato che occorrono in un programma
qualsiasi della
sequenza e non necessariamente solo nel programma
corrente.
Abbiamo presentato anche un metodo,
detto `unfold/fold proof method', per
provare equivalenze della forma: per ogni X
(esiste Y tale che G1(X,Y) se e
solo se esiste Z tale che G2(X,Z)), dove G1 and G2
sono goal (cioe',
congiunzioni di atomi). Questo metodo e' molto
utile per l'applicazione
della regola di rimpiazzamento di goal che, infatti,
richiede la prova di
tali equivalenze. L'unfold/fold proof method
fa uso di tecniche di
trasformazione, e pertanto, esso permette di fare
sia le prove dei programmi
che la derivazione dei programmi facendo uso di un
unico sistema software di
manipolazione dei programmi.
Abbiamo poi considerato la classe
dei programmi normali con la semantica
della computed answer substitution e la semantica
detta della Clark's
completion. Anche per questa classe di programmi
e per le loro semantiche
abbiamo indicato vari teoremi di correttezza.
Nella seconda parte del lavoro
abbiamo presentato le strategie per
controllare e guidare l'applicazione delle regole
di trasformazione cosi` da
poter derivare dei programmi efficienti a partire
dalle loro versioni
iniziali non necessariamente efficienti o a partire
da specifiche date nel
calcolo dei predicati del primo ordine. Sono
state considerate le seguenti
strategie di base: (i) la strategia di tupling,
(ii) la strategia di loop
absorption, (iii) la strategia di generalizzazione.
Abbiamo mostrato che alcune tecniche
di trasformazione molto utili in
pratica, e che sono state pubblicate in letteratura,
come il `compiling
control', la composizione dei programmi e il cambiamento
della
rappresentazione dei dati possono essere tutte considerate
come opportune
sequenze di applicazione delle suddette strategie
di base.
Nel lavoro e' stata anche fatta
una breve panoramica di altre tecniche per la
trasformazione dei programmi, come la tecnica basata
su equivalenze di schemi
di programmi, la tecnica di rimozione della ricorsione,
la tecnica di
annotazione e infine, la tecnica di memoing.
Nella parte finale del lavoro
abbiamo analizzato la relazione esistente tra
(i) la trasformazione dei programmi, (ii) la valutazione
parziale dei
programmi e (iii) la specializzazione dei programmi.
In particolare, abbiamo
paragonato l'approccio a la Lloyd-Shepherdson per
la valutazione parziale dei
linguaggi con l'approccio basato sulle regole di
unfold/fold e abbiamo
illustrato la stretta corrispondenza esistente tra
i due metodi presentando
un esempio di valutazione parziale dei programmi
per un problema di matching
su stringhe.
Un secondo lavoro [2] svolto dall'unita` di Roma Tor
Vergata si e' sviluppato
a partire dalle tecniche di prova basate sulle regole
di fold e unfold. Esso
ha riguardato la sintesi dei programmi logici a partire
da specifiche date
come formule del calcolo dei predicati del primo
ordine. Questo lavoro e'
diviso in due parti. La prima parte riguarda
il metodo di prova detto
`unfold/fold proof method'. Come detto sopra,
esso serve per provare
proprieta' di goal nel contesto di un dato programma
logico fatto da clausole
di Horn. La seconda parte del lavoro riguarda
invece la sintesi dei
programmi logici a partire dalle specifiche.
Nella prima parte del lavoro abbiamo
mostrato che l'unfold/fold proof method
puo' essere usato in particolare per dimostrare che
dato un programma logico
P e dati due goal G1 and G2, nel minimo modello di
Herbrand di P vale la
seguente equivalenza:
(*) per ogni X (esiste Y tale che G1(X,Y) se e solo
se
esiste Z tale che G2(X,Z)).
La prova di tale equivalenza consiste nel derivare
per trasformazione a
partire dal programma P e la clausola C1: new1(X)
<- G1(X,Y) un insieme,
diciamo S, di clausole che puo' essere derivato per
trasformazione (modulo la
ridenominazione di new1 con new2) anche dal programma
P e dalla clausola C2:
new2(X) <- G2(X,Z).
Durante le due derivazioni dell'insieme
S di clausole, quella a partire da P
U {C1} e quell'altra a partire da P U {C2}, si possono
applicare le seguenti
regole di trasformazione: (i) unfolding, (ii)
folding, (iii) rimpiazzamento
di un goal, (iv) generalizzazione + introduzione
di uguaglianze e (v)
simplificazione di uguaglianze. Dopo che una
equivalenza tra i goal G1 e G2,
come la (*) di cui sopra, e' stata provata, essa
puo' essere usata per
l'applicazione della regola di rimpiazzamento di
un goal durante il processo
di trasformazione a partire dal programma P.
Se vogliamo che il rimpiazzamento
del goal G1 con il goal G2 preservi la
correttezza totale (cioe' il programma prima del
rimpiazzamento e quello dopo
il rimpiazzamento abbiano lo stesso minimo modello
di Herbrand) occorre che
la prova della equivalenza (*) con metodo di unfold/fold
sia `non-ascending'
nel senso seguente: per ogni clausola M nell'insieme
S di clausole, se M e'
stata derivata dal programma P U {C1} attraverso
la sequenza s1 di regole di
trasformazione, allora M, ove new1 sia stato ridenominato
in new2, possa
essere derivata anche a partire dal programma P U
{C2} attraverso una
sequenza s2 di regole di trasformazione, che abbia
un numero di passi di
unfolding che non sia piu' grande di quello di s1.
Nella seconda parte del lavoro
abbiamo usato l'unfold/fold proof method per
la sintesi di un insieme, chiamiamolo Eureka, di
clausole, tale che dato un
programma P e la specifica implicita di un nuovo
predicato newp della forma:
(**) per ogni X (esiste Y tale che spec(X,Y) se e
solo se esiste Z tale che
(context(X,Z) e newp(X,Z))), si abbia che la (**)
vale nel minimo modello di
Herbrand del programma P U Eureka. Nella formula
(**) abbiamo assunto che i
predicati che occorrono nelle formule spec e context
siano tutti definiti nel
programma in P.
Questo metodo di sintesi basato sull'unfold/fold proof
method si applica al
problema della sintesi automatica di programmi che
manipolano
liste-differenza a partire da programmi che manipolano
liste. L'abbiamo
applicato anche per la sintesi di programmi logici
in cui si eviti il
non-determinismo ridondante presente in versioni
iniziali degli stessi che
siano risultino essere programmi ricorsivi-sinistri.
Per quanto riguarda la tematica di ricerca sulle reti
neuronali e sulle
specifiche dei sistemi reattivi basate sulla teoria
degli automi esse non
hanno potuto trovare sviluppo. Ci si e' interessati
invece alle
problematiche di security (dial-back authentication)
durante la connessione
alle Intranet da parte di utenti remoti e alle tipologie
di accesso a
connettivita' di tipo switched su base fissa (PSTN
o ISDN) o di tipo
cellulare (GSM o ETACS) [3]. Si sono anche
studiate problematiche di
combinatorica su grafi [4].
Strumentazione Realizzata:
Prototipo preliminare di un trasformatore di programmi
logici
Ottenibile da: http://www.iasi.cnr.it/~proietti/system.html
Prodotti della ricerca:
- pubblicazioni su rivista a diffusione internazionale:
[2] Pettorossi, A.
and Proietti, M. Synthesis and Transformation of
Logic
Programs Using Unfold/Fold Proofs Journal of Logic Programming
(to appear)
[4] Fachini, E. and J. Korner:
Color Number capacity and Perfectness of
Directed
Graphs. Graphs and Combinatorics. (to appear).
- pubblicazioni su libri o atti di conferenze:
[1] Pettorossi, A. and Proietti,
M.: Transformation of Logic Programs
Handbook
of Logic in Artificial Intelligence and Logic Programming,
Volume
5. 1998. D. M. Gabbay, C. J. Hogger, and
J. A.
Robinson,
editors. pages 697-787
[3] Buttarazzi, B. and Mazza,
S.: La connessione ad Intranet da computer
mobili.
AICA 98. Napoli.
- partecipazioni a conferenze internazionali:
Partecipazione
all'ETAPS a Lisbona (Esop 98) dal 28.3.98 al 4.4.98
SAS e
PLILP a Pisa dal 15 al 19.9.98
--------------------------------------------------------------------------
Schema riassuntivo dell'utilizzo del finanziamento
(cifre spesa o impegnate)
Voce di spesa
Spesa in MILIONI
Descrizione
--------------------------------------------------------------------------
Materiale
0,121 libri
inventariabile
Grandi
Attrezzature
----
Materiale di
1,208 cancelleria, accessori per computer
consumo
toner per stampante.
Spese per
calcolo ed
elaborazione
----
dati
Personale a
contratto
Servizi esterni
Missioni 4,067
Altro
0,004 Spese bancarie
--------------------------------------------------------------------------
Per problemi e suggerimenti: adp@iasi.rm.cnr.it
Save this page at: home2/users/adp/public.html/MURST40-Levi-98/40Levi_Relazione01-03-99Roma2.html