Progetto Cofinanziato M.I.U.R.
Ragionamento su aggregati e
numeri a supporto della programmazione e relative verifiche: dagli algoritmi
di decisione alla programmazione con vincoli con multi-insiemi, insiemi
e mappe
(Coordinatore nazionale: Domenico
Cantone)
Unità di Parma
Programmazione dichiarativa
con vincoli su insiemi e multi-insiemi
(Coordinatore locale: Gianfranco
Rossi)
Stato d'avanzamento del progetto
Attività svolta
Il lavoro svolto dall'Unità di Parma nel primo
anno di attivita' del progetto ha riguardato essenzialmente la definizione,
uso e realizzazione di linguaggi di programmazione con vincoli insiemistici
e numerici. In accordo con la tempistica del Programma di Ricerca che prevede
la suddivisione del lavoro in due fasi successive, in questo primo anno
di attivita' sono state affrontate la maggior parte delle ricerche previste
per la prima fase, anticipando anche alcune di quelle previste per la seconda
fase. Piu' in dettaglio, sono state svolte le seguenti attivita'.
-
E' stata completata l'analisi e la definizione dei
risolutori
di vincoli su insiemi, multi-insiemi e liste in un contesto di programmazione
logica a vincoli (CLP) [DPR02a]. In particolare si e' analizzato a fondo
il problema dell'unificazione insiemistica [DOPR02c] e si e' approfondito
il confronto tra CLP(SET) ed i cosiddetti set-constraints
[DOP02b]. Si e' quindi proceduto ad integrare i risolutori per insiemi
e multi-insiemi nel linguaggio logico con insiemi esistente CLP(SET) (qui
indicato col nome di {log}+) [punto 3.1
del Programma di Ricerca, Fase 1].
-
Sono state analizzate alcune applicazioni di {log}+,
di CLP(FD) e, piu' in generale, dei risultati relativi alla computazione
su insiemi finora ottenuti. In particolare si e' mostrata l'effettivita'
della programmazione a vincoli su domini finiti per applicazioni di biologia
computazionale e di allocazione risorse [DBF02] [ABDDR02].
Si sono inoltre applicati alcuni dei risultati ottenuti nell'ambito dell'unificazione
insiemistica a problemi di confronto di grafi. Rappresentando gli
insiemi come grafi, l'uguaglianza di insiemi risulta infatti equivalente
al problema di bisimulazione tra grafi. Si e' quindi studiato dal punto
di vista computazionale tale problema sia con rappresentazioni esplicite
di grafi che simboliche [DBF02]. Si e' inoltre studiato il problema del
subgraph bisimulation, utile per l'estrazione di sottografi equivalenti
ad un grafo dato [DP03]. Applicazioni di {log}+ alla
risoluzioni di classici problemi di manipolazione di grafi quali quello
del "coloring" e quello del "traveling salesman" sono disponibili all'indirizzo
http://www.math.unipr.it/~gianfr/setlog.Home.html[punto
3.2 e in parte punto 4 del Programma di Ricerca, Fase 1].
Questa attivita' verra' comunque continuata ed
ampliata anche nel secondo anno del progetto (Fase 2).
-
Si e' iniziato lo studio relativo all'inserimento
e all'utilizzo di vincoli, in particolare di tipo insiemistico, nel contesto
dei linguaggi di programmazione convenzionale (piuttosto che CLP),
orientati alla programmazione dichiarativa, tipo Alma-0 [punto
3.3 del Programma di Ricerca, Fase 1]. Questo
ha portato alla progettazione di un nuovo linguaggio dichiarativo
con insiemi denominato Singleton [Ros02] (indicato nella
proposta del progetto genericamente con il nome di L0). Singleton
fornisce la maggior parte degli aspetti caratterizzanti di {log}+ (specificatamente,
astrazioni di aggregati di dati, quali insiemi e liste, definite sia estensionalmente
che intensionalmente, vincoli, computazioni non-deterministiche), ma incorporate
in un ambiente piu' convenzionale, usando una sintassi e delle convenzioni
Pascal-like, come avviene in Alma-0
[punto
3.6 del Programma di Ricerca, Fase 1].
Questa attivita' proseguira' nella Fase 2 del progetto (punto 3.3).
-
E' stato impostato il progetto e iniziato lo sviluppo
in linguaggio Java di un primo prototipo di ambiente di programmazione
visuale basato sulla nozione di insieme che offre all'utente un insieme
di "facilities" visuali per la definizione di oggetti insiemistici e la
loro manipolazione [punto 3.4 del Programma
di Ricerca, Fase 1]. Questa attivita'
proseguira' nella Fase 2 del progetto (punto 3.4).
-
Sono state migliorate in vari aspetti le prestazioni
dell'interprete del linguaggio {log}+. In particolare nell'interprete
vengono ora individuati e trattati separatamente in modo piu' efficiente
diversi casi di insiemi completamete specificati. Si e' poi iniziato lo
studio relativo alla combinazione di vincoli insiemistici con vincoli su
interi, e precisamente su domini finiti (CLP(FD)) e su insiemi di
interi (Conjunto), la cui realizzazione potra' comportare
ulteriori significativi miglioramenti delle prestazioni dell'interprete.
L'integrazione di questi nuovi domini di vincoli in {log}+ risulta particolarmente
semplice e naturale in quanto le nuove possibilita' introdotte sono comunque,
almeno da un punto di vista semantico, riconducibili a nozioni insiemistiche.
La disponibilita' di risolutori molto efficienti per questi tipi
particolari di vincoli insiemistici permette di ottenere notevoli miglioramenti
di efficienza, allargando di fatto lo spettro di problemi effettivamente
risolvibile in {log}+. L'individuazione dei vincoli da poter far trattare
ai risolutori CLP(FD) e Conjunto puo' essere resa automatica dall'utilizzo
di opportune tecniche di analisi statica del programma {log}+. In particolare
e' stato definito un reticolo per l'analisi statica e la catalogazione
di variabili insiemistiche che permette di capire se una variabile generica
in un programma sia un intero, un insieme di interi o ricorsivamente un
insieme di un tipo gia' noto, permettendo cosi' di riconoscere le variabili
del tipo gestito da Conjunto (insieme di interi) [punto
3.1 del Programma di Ricerca, Fase 2].
Si sono inoltre affrontati alcuni altri problemi, strettamente correlati
con quelli sopra esposti, anche se non espressamente previsti nel programma
originario. Specificatamente sono state svolte attivita' finalizzate alla
realizzazione di risolutori di vincoli come librerie utilizzabili
all'interno di linguaggio convenzionali (in particolare Object Oriented)
esistenti, e alla realizzazione di risolutori di vincoli su domini numerici.
-
E' stata progettata e realizzata una libreria Java, denominata JavaSet,
che fornisce alcune delle caratteristiche fondamentali dei linguaggi CLP
(quali, l'utilizzo di variabili logiche, l'unificazione, il non determinismo,
la
risoluzione dei vincoli) in un contesto di programmazione orientata
agli oggetti. I vincoli per ora considerati sono quelli relativi ad operazioni
insiemistiche di base (appartenenza, inclusione, unione, intersezione,
...) e gli algoritmi di risoluzione adottati sono essenzialmente quelli
di CLP(SET), ma implementati utilizzando il linguaggio Java. La libreria
puo' essere utilizzata in particolare per la risoluzione di problemi combinatori
di ricerca, quale quello della colorazione di una mappa, dell'allocazione
di risorse, ecc. Si prevede di estendere ulteriormente la libreria per
ottenere una migliore integrazione tra i costrutti del linguaggio Java
e le possibilita' fornite dalla libreria stessa e, possibilmente, di migliorare
l'interfaccia della libreria verso il linguaggio Java in modo da renderne
piu' semplice l'utilizzo.
-
Si sono proseguiti gli studi e le attivita' implementative
relative allo sviluppo della Parma Polyhedra Library (PPL), una libreria
C++ che permette la manipolazione di poliedri convessi non necessariamente
chiusi (NNC), rappresentati sia come insieme di vincoli sul dominio
dei numeri reali (sistemi di equazioni e disequazioni lineari, strette
e non) sia come sistemi di punti, raggi, rette e punti di chiusura del
poliedro in R^n (rappresentazione parametrica). In [BRZH02,BHZ02b],
in particolare, e' stato mostrato come la nozione di punto di chiusura
permetta di fornire un'elegante interfaccia per la rappresentazione parametrica
dei poliedri NNC e sono state studiate due implementazioni alternative,
fornendo in entrambi i casi un metodo innovativo ed efficiente per l'eliminazione
delle ridondanze nelle rappresentazioni a vincoli e parametriche.
Le possibilita' fornite dalla libreria PPL potranno
essere utilizzate sia nella direzione di un'integrazione tra risolutori
di vincoli insiemistici e risolutori di vincoli numerici (in particolari
sui reali), sia nello sviluppo di tecniche di manipolazione di insiemi
in forma intensionale. I sistemi manipolati dalla PPL possono vedersi infatti
come una definizione intensionale di sottoinsiemi poliedrali di R^n su
cui e' possibile effettuare operazioni insiemistiche di base quali il test
di insieme vuoto, di appartenenza, l'intersezione e, per mezzo di
opportune costruzioni parametriche, unioni finite di poliedri e dipendenze
funzionali tra poliedri.
Per quanto riguarda le attivita' relative alla definizione
e gestione degli insiemi intensionali, previste per la Fase 1 del
progetto (punto 3.5), si e' preferito posticiparne la loro attuazione alla
Fase 2. Si e' comunque gia' iniziata una attivita' di analisi e progetto
su queste problematiche in collaborazione con il Prof. Enrico Pontelli
dell'Universita' del New Mexico (USA).
Alla luce dei risultati fin qui ottenuti sembra
possibile confermere nelle sue linee generali il programma di ricerca formulato
nella proposta originaria.
Pubblicazioni
Su riviste internazionali
-
[Ros02] G. Rossi.
Set-based Nondeterministic Declarative Programming in SINGLETON.
In: 11th International Workshop on Functional and (constraint) Logic
Programming,
Electronic
Notes in Theoretical Computer Science, Vol. 76,
Elsevier Science B. V., 17 pages, 2002.
-
[DBF02] A. Dovier, M. Burato, and F. Fogolari.
Using Secondary Structure Information for Protein Folding in CLP(FD).
In: 11th International Workshop on Functional and (constraint) Logic
Programming,
Electronic
Notes in Theoretical Computer Science, Vol. 76,
Elsevier Science B. V., 2002.
-
[DGPP02] A. Dovier, R. Gentilini, C. Piazza, and A. Policriti.
Rank-Based Symbolic Bisimulation (and Model Checking).
In WOLLIC'02 (Ruy de Queiroz, Luiz Carlos Pereira, and Edward Hermann
Haeusler eds.),
Electronic
Notes in Theoretical Computer Science, Vol. 67,
Elsevier Science B. V., 2002.
-
[Dov03] A. Dovier.
Book review: Set Theory for Computing:
From Decision Procedures to Declarative Programming with
Sets by Domenico Cantone, Eugenio Omodeo, and Alberto Policriti,
Springer, 2001, In TPLP Vol 3(1) pp 125-128, 2003.
-
[DP03] A. Dovier and C. Piazza.
The Subgraph Bisimulation Problem.
To appear in IEEE Transaction on Knowledge and Data Engineering, 2003.
In atti di Conferenze internazionali
-
[ABDDR02] F. Avanzini, A. Belussi, A. Dal Palu', A. Dovier, and D. Rocchesso.
Optimal Placement of Acoustic Sources in a Built-up Area using CLP(FD).
In J. J. Moreno-Navarro and J. M. Carballo eds.,
AGP 2002, Joint Conference on Declarative Programming, Madrid, Spain,
September 2002, pp. 139--154.
-
[BRZH02] R. Bagnara, E. Ricci, E. Zaffanella, P. M. Hill.
Possibly not closed convex polyhedra and the Parma Polyhedra Library.
In M. V. Hermenegildo and G. Puebla, editors, Static Analysis:
Proceedings of the 9th International Symposium, volume 2477 of
Lecture Notes in Computer Science, pages 213-229, Madrid, Spain, 2002.
Springer-Verlag, Berlin (Disponibile on-line:
http://www.cs.unipr.it/ppl/Documentation/BagnaraRZH02.pdf)
Rapporti Tecnici e lavori sottomessi
-
[DPR02a] A. Dovier, C. Piazza, and G. Rossi.
A uniform approach to constraint-solving for lists, multisets, compact
lists, and sets
Gennaio 2002.
Sottomesso per pubblicazione su Rivista Internazionale (Disponibile
on-line:
http://www.math.unipr.it/~gianfr/PAPERS/RR_PR235.ps)
-
[DPR02b] A. Dovier, C. Piazza, G. Rossi.
Set-Based Constraints.
Rapporto di Ricerca, Quaderno n.309, Dipartimento di Matematica, Università
di Parma,
Dicembre 2002.
Sottomesso per pubblicazione su Rivista Internazionale (Disponibile
on-line:
http://www.math.unipr.it/~gianfr/PAPERS/RR_PR309.ps)
-
[DPR02c] A. Dovier, E. Pontelli, G. Rossi.
Set Unification.
Rapporto di Ricerca, Quaderno n.310, Dipartimento di Matematica, Università
di Parma,
n.310, Dicembre 2002.
Sottomesso per pubblicazione su Rivista Internazionale (Disponibile
on-line:
http://www.math.unipr.it/~gianfr/PAPERS/RR_PR310.ps)
-
[BHZ02] R. Bagnara, P. M. Hill, and E. Zaffanella.
A new encoding of not necessarily closed convex polyhedra.
In M. Carro, C. Vacheret, and K.-K. Lau, editors, Proceedings of
the 1st CoLogNet Workshop on Component-based Software Development and
Implementation Technology for Computational Logic Systems, pages
147-153, Madrid, Spain, 2002. Published as TR Number CLIP4/02.0,
Universidad Politécnica de Madrid, Facultad de Informática
(Disponibile on-line:
http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ02a.pdf)
-
[BRZH02b] R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill.
Possibly not closed convex polyhedra and the Parma Polyhedra Library.
Quaderno 286, Dipartimento di Matematica, Università di Parma,
Italy,
2002. (Disponibile on-line:
http://www.cs.unipr.it/Publications/Abstracts/Q286)
-
[BHZ02b] R. Bagnara, P. M. Hill, and E. Zaffanella.
A new encoding and implementation of not necessarily closed convex
polyhedra. Quaderno 305, Dipartimento di Matematica, Università
di
Parma, Italy, 2002 (Disponibile on-line:
http://www.cs.unipr.it/Publications/Abstracts/Q305)
Strumentazione acquisita
-
Per il primo anno le spese per strumentazione finalizzata alle attivita'
del progetto si sono limitate a quelle relative alla manutenzione di un
PC esistente (acquisto HD) e al cofinanziamento di un portatile ASUS. Per
il secondo anno prevediamo invece l'acquisizione, sempre per le finalita'
del progetto, di vari strumenti di calcolo (PC) e di una stampante laser.
Strumenti (software) realizzati
-
Interprete per il linguaggio logico con vincoli su insiemi e multi-insiemi
{log}+. L'interprete del linguaggio, scritto in
SICStus Prolog, è disponibile, insieme ad altra documentazione
relativa alla definizione ed uso di {log}+ all'indirizzo: http://www.math.unipr.it/~gianfr/setlog.Home.html.
-
Programma realizzato in CLP(FD) per la risoluzione del problema del folding
di una proteina. Codice, documentazione e dati si trovano in: http://www.dimi.uniud.it/~dovier/PF/pf_clp.html.
-
La Parma Polyhedra Library (PPL) e` stata estesa per consentire la gestione
efficiente di sistemi di vincoli lineari contenenti anche disuguaglianze
strette (ovvero, poliedri convessi che possono non godere della proprieta`
di chiusura topologica), fornendo due implementazioni alternative.
Indirizzo web del progetto PPL: http://www.cs.unipr.it/ppl/
Partecipazione a conferenze e scuole internazionali
-
Second International Summer School
on Computational Logic,
Maratea, Italy, August 25-30, 2002 (Bagnara)
-
SAS'02: 9th International Symposium
on Static Analysis, Madrid, Spain, 17-20 Settembre 2002 (Bagnara
e Zaffanella)
-
APPIA-GULP-PRODE 2002 (AGP02),
Joint Conference on Declarative Programming, Madrid, Spain,
16--18 Settembre 2002 (Dovier).
-
WFLP2002: 11th International
Workshop on Functional and (constraint) Logic Programming, Grado, Giugno
2002 (Dovier e Rossi).
Personale a contratto
Sono stati stipulati tre contratti per prestazione occasionale della
durata di 3 mesi ciascuno:
-
con la Dr. Elisa Ricci finalizzato allo sviluppo di software per
la manipolazione di poliedri convessi
-
con il Dr. Alessandro Dal Palu' finalizzato all'integrazione
di risolutori di vincoli insiemistici in un contesto
di programmazione logica con vincoli.
-
con la Dr. Elisabetta Poleo finalizzato alla progettazione e sviluppo
di una libreria Java per la programmazione con vincoli insiemistici
(in corso di approvazione).