Illustrazione dell'attivita' svolta durante il secondo anno
-----------------------------------------------------------

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 dei programmi si sono sviluppate due
metodologie per la dimostrazione della correttezza totale delle regole di
fold, unfold e goal replacement. Tali metodologie sono parametriche rispetto alla semantica
che viene preservata durante la trasformazione stessa [2] e  pertanto,
possono essere usate per provare la correttezza di regole di trasformazione
sia nell'ambito di programmi logici che in quello di programmi funzionali o
concorrenti o a vincoli. Occorre solamente che la semantica del linguaggio
in esame possa essere espressa con regole di inferenza.
Una prima metodologia e' quella dell'Unico Punto Fisso,
basata su una proprieta' di ben-fondatezza del calcolo della semantica
del programma derivato. Una seconda metodologia e' quella del Miglioramento
per cui nel programma di partenza il calcolo della semantica
della porzione vecchia del programma da sostituire non e' piu' corto
(in una opportuna misura) del calcolo della semantica della porzione nuova
di programma che sostituisce la vecchia.
Questa seconda metodologia puo' essere applicata anche nel caso in cui
le regole per il calcolo della semantica hanno un numero infinito di premesse.

    Sempre nell'ambito della trasformazione dei programmi si sono sviluppate
regole del tipo fold/unfold per il caso di programmi logici 'di ordine
elevato', nel senso che consentano di avere goals come argomenti di simboli
di predicato [4]. La necessita' di avere regole di trasformazione di programmi
logici di ordine elevato deriva dal fatto che spesso occorre evitare di
cambiare la posizione relativa delle formule atomiche in un goal composito,
giacche' tale cambiamento puo' modificare la semantica operazionale che usi
la regola di selezione left-to-right che e' la regola usata dal compilatore
Prolog. Accade anche che gli argomenti di tipo goal spesso
denotano una continuazione. Pertanto le regole che vengono proposte in [4]
permettono di eseguire in ambiente logico trasformazioni analoghe a
quelle che vengono fatte in ambiente funzionale e che fanno uso appunto
di argomenti di ordine elevato denotanti continuazioni.

    Per quanto riguarda la specializzazione dei programmi in [3] si e'
studiato il problema della specializzazione di programmi logici con vincoli.
Si sono proposte regole e strategie di trasformazione che permettono di derivare
programmi con vincoli particolarmente efficienti giacche' permettono di sfruttare
proprieta' invarianti che valgono durante la computazione dei programmi.
In particolare si e' introdotta la regola di Contextual Constraint Replacement
e una opportuna variante della regola di folding. Si sono anche introdotte la
Context Propagation Strategy e la Invariant Promotion Strategy.

    Nell'area della sintesi dei programmi logici abbiamo completato il
lavoro dello scorso anno pubblicando i risultati su rivista [1].

Strumentazione Realizzata:

Sviluppo del Prototipo preliminare di un trasformatore di programmi logici
con la realizzazione di un'interfaccia grafica per l'applicazione
di regole e strategie.
Ottenibile da: http://www.iasi.cnr.it/~proietti/system.html

Prodotti della ricerca:

 - Pubblicazioni su rivista a diffusione internazionale:

[1] Pettorossi,  A.  and Proietti, M.:  Synthesis  and  Transformation  of
    Logic Programs Using Unfold/Fold Proofs, Journal of Logic Programming,
    Vol 41, No. 2&3, pp. 197-230.

- Pubblicazioni su libri o atti di conferenze

[2] Maurizio Proietti and Alberto Pettorossi:
    "Transforming Inductive Definitions",
    D. De Schreye (ed.) Proceedings of the 16th International Conference on Logic Programming (ICLP'99),
    Las Cruces, New Mexico, USA, Nov. 29 - Dec. 4, 1999, MIT Press, pp. 486-499.

[3] Fioravanti Fabio, Alberto Pettorossi, Maurizio Proietti:
    "Rules and Strategies for Contextual Specialization of Constraint Logic Programs",
    M. Leuschel (ed.) Proceedings of the ICLP'99 Workshop on Optimization and Implementation of
    Declarative Programming Languages (WOID'99), Las Cruces, New Mexico, USA, Dec.2-3, 1999, pp. 1-9.

[4] Alberto Pettorossi and Maurizio Proietti:
    "Transformation Rules for Logic Programs with Goals as Arguments",
    Pre-Proceedings 9th LOPSTR '99 Report University of Venice (Italy) CS-99-16, pages 171-178

- Partecipazioni a conferenze nazionali e internazionali:
        Appia-Gulp-Prode '99 a L'Aquila (Italia) dal 7.9.99 al 9.9.99
        Lopstr '99 e SAS a Venezia (Italia) dal 22 al 24.9.99
        ICLP '99 a Las Cruces (New Mexico, USA) dal 29.11.99 al 4.12.99
 

--------------------------------------------------------------------------
Schema riassuntivo dell'utilizzo del finanziamento (cifre spesa o impegnate)
[da completare]

 Voce di spesa           Spesa in MILIONI               Descrizione
 --------------------------------------------------------------------------

 Materiale
 inventariabile

 Grandi
 Attrezzature                 ----

 Materiale di
 consumo

 Spese per
 calcolo ed
 elaborazione                 ----
 dati

 Personale a
 contratto

 Servizi esterni

 Missioni

 Altro
 --------------------------------------------------------------------------

                                       Per problemi e suggerimenti: adp@iasi.rm.cnr.it

Save this page at: home2/users/adp/public.html/MURST40-Levi-98/40Levi_RelazioneJan2000Roma2.html