Relazione del primo anno di attività

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
 --------------------------------------------------------------------------
 

Save this page at: home2/users/adp/public.html/MURST40-Levi-98/40Levi_Relazione01-03-99Roma2.html