UNIVERSITA DEGLI STUDI DI PISA

Facolta di Scienze

Matematiche Fisiche e Naturali

Corso di Laurea in Scienze dell’Informazione

Tesi di Laurea

Interpretazione astratta di linguaggilogici con vincoli su domini finiti

Candidato:Roberto Bagnara

Relatore: Controrelatore:Prof. Giogio Levi Prof. Ugo Montanari

Anno Accademico 1991/92

A Vincenzo ed Ermelinda,

che avrebbero voluto

vedere questo giorno.

Indice

1 Introduzione 4

2 Preliminari 92.1 Notazione basilare . . . . . . . . . . . . . . . . . . . . . . . . 92.2 Specifiche algebriche . . . . . . . . . . . . . . . . . . . . . . . 102.3 Strutture algebriche . . . . . . . . . . . . . . . . . . . . . . . . 132.4 Interpretazione astratta . . . . . . . . . . . . . . . . . . . . . 172.5 Lo schema CLP . . . . . . . . . . . . . . . . . . . . . . . . . . 19

3 Semantica generalizzata di CLP 223.1 Algebre di vincoli . . . . . . . . . . . . . . . . . . . . . . . . . 24

3.1.1 Sistemi di termini . . . . . . . . . . . . . . . . . . . . . 243.1.2 Uno schema algebrico per i sistemi di vincoli . . . . . . 263.1.3 Correlazione dei sistemi di vincoli: correttezza . . . . . 33

3.2 Semantica generalizzata . . . . . . . . . . . . . . . . . . . . . 363.2.1 Semantica operazionale . . . . . . . . . . . . . . . . . . 383.2.2 Semantica di punto fisso . . . . . . . . . . . . . . . . . 39

3.3 Interpretazione astratta di CLP . . . . . . . . . . . . . . . . . 41

4 Il linguaggio CLP(FD) 464.1 Motivazioni . . . . . . . . . . . . . . . . . . . . . . . . . . . . 464.2 Definizione del linguaggio . . . . . . . . . . . . . . . . . . . . 474.3 Risoluzione di vincoli . . . . . . . . . . . . . . . . . . . . . . . 50

5 Interpretazioni basate sulle bounding box 525.1 Motivazioni . . . . . . . . . . . . . . . . . . . . . . . . . . . . 545.2 Intervalli . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 565.3 Bounding box . . . . . . . . . . . . . . . . . . . . . . . . . . . 625.4 Dai vincoli alle bounding box . . . . . . . . . . . . . . . . . . 70

5.4.1 Possibili soluzioni . . . . . . . . . . . . . . . . . . . . . 705.4.2 Una soluzione offerta dall’AI . . . . . . . . . . . . . . . 72

1

5.4.3 Reti e propagazione di vincoli . . . . . . . . . . . . . . 725.4.4 Inferenza di etichette . . . . . . . . . . . . . . . . . . . 755.4.5 Normalizzazione dei vincoli . . . . . . . . . . . . . . . 765.4.6 Raffinamento delle bounding box . . . . . . . . . . . . 785.4.7 L’algoritmo di Waltz per le bounding box . . . . . . . 81

5.5 Astrazione dell’algebra dei vincoli . . . . . . . . . . . . . . . . 895.5.1 Vincoli residui . . . . . . . . . . . . . . . . . . . . . . . 905.5.2 Vincoli approssimati . . . . . . . . . . . . . . . . . . . 92

5.6 Un esempio . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

6 Conclusioni 102

2

Elenco delle figure

4.1 Struttura di un sistema CLP . . . . . . . . . . . . . . . . . . . 50

5.1 Approssimazione mediante politopi convessi . . . . . . . . . . 535.2 Approssimazione mediante bounding box . . . . . . . . . . . . 535.3 Congiunzione di due bounding box . . . . . . . . . . . . . . . 665.4 Disgiunzione di due bounding box . . . . . . . . . . . . . . . . 675.5 L’algoritmo di Waltz . . . . . . . . . . . . . . . . . . . . . . . 825.6 Rete di vincoli . . . . . . . . . . . . . . . . . . . . . . . . . . . 835.7 Assiomi per il calcolo degli intervalli di variazione . . . . . . . 885.8 Congiunzione di vincoli astratti . . . . . . . . . . . . . . . . . 95

3

Capitolo 1

Introduzione

Lo scopo dell’analisi data-flow e quello di determinare, a tempo di compila-zione, certe proprieta caratterizzanti il comportamento computazionale deiprogrammi. Queste proprieta sono tipicamente applicabili a tutte le possibilisequenze di controllo e di flusso dei dati, pertanto forniscono informazioniimpossibili da ottenersi semplicemente eseguendo il programma o ispezio-nandone solo una parte. Dal momento che la maggior parte delle proprieta“interessanti” dei programmi sono indecidibili, le informazioni che si posso-no ottenere per mezzo dell’analisi sono necessariamente approssimate. Ciononostante tali informazioni possono essere convenientemente utilizzate perun numero di applicazioni quali:

• la generazione di asserzioni invarianti per la verifica dei programmi,

• il miglioramento dell’affidabilita del software semplificando la gene-razione di documentazione e automatizzando parte del processo didebugging [47],

• l’analisi automatica della complessita [22],

• la generazione di codice efficiente per i programmi sfruttando tecnicheavanzate di compilazione.

Molte delle analisi data-flow che sono state proposte (in particolare per iprogrammi logici) sono basate su una tecnica chiamata interpretazione astrat-ta. L’idea essenziale e quella di ricavare descrizioni finite del comportamentodi un programma, eseguendo il programma su un dominio “astratto”. Ildominio astratto contiene le descrizioni degli “oggetti concreti” che sonomanipolati nell’esecuzione del programma. Le operazioni di composizionedelle descrizioni, usate nell’esecuzione astratta, “modellano”, rispetto alleproprieta alle quali si e interessati, i corrispondenti operatori sugli oggetti

4

concreti. Il dominio concreto e le descrizioni sono opportunamente correlatiper garantire la correttezza dell’astrazione. Con questa tecnica si ottengonoalgoritmi di analisi basati direttamente sulla semantica del linguaggio. In talmodo risulta semplificata la progettazione degli algoritmi e la dimostrazionedella loro correttezza.

Le tecniche di analisi statica si sono dimostrate di fondamentale impor-tanza per guidare la fase di ottimizazione dei compilatori, al fine di ottenereimplementazioni efficienti dei sistemi di programmazione logica, soprattuttoProlog. Alcuni risultati preliminari [35] suggeriscono come l’analisi globale dialcuni linguaggi che ricadono nel paradigma CLP di programmazione logicacon vincoli, possa essere ancora piu “redditizia”.

La programmazione logica con vincoli (CLP) e una generalizzazione delparadigma di programmazione logica pura con caratterizzazioni semantichedel tutto simili (model-theoretic, di punto fisso e operazionali) [33]. CLP e unparadigma generale che puo essere istanziato su vari domini computazionalisenza richiedere la codifica dei dati come termini del primo ordine. In CLPil passo operazionale basilare nell’esecuzione dei programmi e il controllo disoddisfacibilita di vincoli in una data struttura algebrica (dominio). Unadistinzione di fondamentale importanza in CLP e quella tra il controllo disoddisfacibilita e il calcolo delle soluzioni. Nel caso della programmazione lo-gica ordinaria le due azioni coincidono e sono incapsulate nel procedimento diunificazione, che controlla la soddisfacibilita di un insieme di equazioni calco-landone, se esiste, la soluzione piu generale. In CLP il calcolo delle soluzionidi un insieme di vincoli e demandato ad un apposito risolutore, il quale noninfluenza la definizione semantica del linguaggio. Gli aspetti linguistici es-senziali di CLP possono cosı essere separati dai dettagli del sistema di vincoli(dominio) sul quale e istanziato. Si puo allora parametrizzare la semanticadei linguaggi CLP rispetto ai particolari domini semantici delle sue istanze.Una tale generalita del paradigma consente di formalizzare l’interpretazioneastratta all’interno del paradigma stesso. Vale a dire che l’interpretazioneastratta di un programma P in un’istanza di CLP, viene condotta eseguendo(in modo finito) un programma P ′ (fortemente correlato a P ) in un’altraistanza di CLP [27].

La compilazione dei linguaggi CLP pone nuovi problemi, richiedendo l’e-stensione di tecniche gia utilizzate nella compilazione di Prolog e di tecnicheche provengono da altri campi dell’informatica, ad esempio quelle tipichedella ricerca operativa e dell’intelligenza artificiale (AI) per la soluzione ef-ficiente di sistemi di vincoli. Non e ancora ben chiaro quali ottimizzazioniusate nella compilazione di Prolog possano essere convenientemente estese alcontesto CLP, ne quale tipo di tecniche specifiche per i domini possano esseresviluppate.

5

In questa tesi, ci proponiamo di affrontare il problema dell’analisi staticadi linguaggi logici con vincoli studiandone l’applicabilita ad alcuni casi signi-ficativi. Le considerazioni che se ne deducono permettono di avere un quadromigliore degli strumenti semantici necessari per formalizzare l’interpretazioneastratta di CLP.

Uno dei contributi della presente tesi e l’integrazione di tecniche di dedu-zione approssimata, note nel campo dell’intelligenza artificiale, con uno sche-ma opportuno per la definizione di semantiche non standard di CLP. Questaintegrazione risulta particolarmente appropriata al caso specifico, considera-to in questa tesi, dell’interpretazione approssimata (astratta) di programmilogici con vincoli. La tecnica di inferenza utilizzata in questa tesi e quellanota, in generale, sotto il nome di propagazione su rete di vincoli . Una retedi vincoli e una struttura dichiarativa che esprime relazioni tra oggetti, econsiste di un certo numero di nodi connessi da vincoli. I nodi rappresentanosingoli parametri, e sono caratterizzati da un valore (attributo, proprieta),noto o ignoto. Un vincolo rappresenta una relazione tra i valori dei nodiche esso connette. La tecnica di propagazione di vincoli consiste nel dedurreinformazioni da un piccolo gruppo di vincoli e nodi, e nel memorizzare questeinformazioni modificando la rete. Le successive deduzioni faranno uso di que-ste modifiche per produrre ulteriori cambiamenti nella rete. In questo modole conseguenze deducibili delle informazioni presenti nella rete si diffondonogradualmente nella struttura.

L’ipotesi di lavoro che ha guidato questo lavoro di tesi e che tecniche diquesto genere siano importanti per l’analisi dei programmi logici con vincoli.Innanzitutto l’assonanza tra i termini “propagazione di vincoli” e “program-mazione logica con vincoli” non e solo linguistica. La generalita del para-digma CLP si accoppia bene con la generalita della propagazione di vincoli,che puo essere istanziata su varie classi di vincoli, parametri, tipi delle in-formazioni che vengono dedotte. Il concetto di rete di vincoli vista come uninsieme di connessioni locali e comune in AI. Ad esempio i sistemi di ragio-namento fisico si basano sul fatto che gli effetti fisici si propagano attraversole connessioni tra le componenti del sistema. In genere, quindi, i vincoli suivalori delle grandezze fisiche mettono in relazione solo i parametri relativi apoche componenti connesse [20]. Questa nozione non e estranea al campodella programmazione logica con vincoli. Qui, infatti, possiamo considerarei vincoli di ogni istanza di clausola come componenti connesse locali i cuieffetti si propagano attraverso i “meccanismi di passaggio dei parametri”.1

1Naturalmente questo non implica che i tipici programmi CLP abbiano particolaricaratteristiche di localita. Di fatto, anche l’espressione “tipico programma CLP” non ha,a tutt’oggi, un significato ben definito.

6

La propagazione di vincoli potrebbe allora rappresentare uno schema di al-goritmi applicabili all’analisi data-flow dei programmi CLP. Da un punto divista pragmatico tali algoritmi (quale quello di Waltz) hanno il vantaggio difar parte di un patrimonio consolidato e ben compreso, e di rappresentareun soddisfacente compromesso tra precisione ed efficienza. Sfruttando questecaratteristiche degli algoritmi di propagazione di vincoli e uno schema alge-brico adeguato, in questa tesi ci ripromettiamo di colmare il salto che spessoesiste tra la formalizzazione teorica dell’analisi in termini di interpretazioneastratta e la realizzazione di algoritmi efficienti che la implementano.

L’esempio considerato in questa tesi consiste nella definizione di una se-mantica non standard per un linguaggio logico con vincoli su domini numericifiniti (CLP(FD)). L’interpretazione astratta cosı ottenuta consente di otte-nere delle approssimazioni “quantitative” dell’insieme di successo associatoai programmi. Le informazioni ricavate da tale analisi sono direttamente im-piegabili nel processo di compilazione. Le soluzioni dei vincoli di CLP(FD)sono approssimate “spazialmente” per mezzo di regioni rettangolari che chia-meremo bounding box . Intuitivamente le soluzioni di un vincolo su n variabilirappresentano una certa “sagoma” in uno spazio n-dimensionale. Questa sa-goma puo essere approssimata con un parallelepipedo con i lati paralleli agliassi (bounding box) che la contenga. Le bounding box sono forme moltosemplici di approssimazione spaziale: sono facilmente memorizzabili e mani-polabili. Una bounding box e univocamente determinata dalle sue proiezionisugli assi coordinati associati alle variabili. Per questo motivo si puo indiffe-rentemente parlare di bounding box che approssimano le soluzioni dei vincoli,o di intervalli che rappresentano una sovrastima dei possibili valori assuntidalle variabili. Questa tecnica di approssimazione (rappresentare i valoridelle variabili con intervalli ed effettutare deduzioni circa questi intervalli) ecomune nel campo dell’interpretazione astratta [13].

La presente tesi ha inoltre permesso di osservare come alcune restrizio-ni (quali la distributivita degli operatori fondamentali di composizione deivincoli), introdotte in un sistema di vincoli appositamente studiato per l’in-terpretazione astratta di programmi CLP in [27, 28], fossero eccessive peralcune classi di analisi. Il rilasciamento di queste condizioni non pregiudicala sussistenza di alcune importanti proprieta (quali la monotonia dell’opera-tore astratto delle conseguenze immediate) della semantica utili nell’analisi.Questo approccio ha comunque evidenziato come le condizioni piu restrittiveintrodotte in [27] siano invece necessarie per assicurare la validita di altririsultati semantici standard quali l’equivalenza tra il modello operazionale equello di punto fisso associato al programma da analizzare.

La tesi e cosı suddivisa: nel capitolo 2 vengono introdotte le nozionie i concetti fondamentali che saranno utilizzati nel seguito. Il capitolo 3

7

contiene l’esposizione dello schema di semantica generalizzata che useremoper formalizzare l’interpretazione approssimata basata sulle bounding box.Il capitolo 4 da una breve descrizione del linguaggio CLP(FD) oggetto dellanostra analisi. Il capitolo 5 contiene la formalizzazione dell’interpretazionesulle bounding box di CLP(FD), compresa la descrizione degli algoritmi dipropagazione di vincoli. Infine il capitolo 6 trae le conclusioni di questolavoro e suggerisce alcuni possibili sviluppi futuri.

Comunque, se avessi aspettato abbastanza,probabilmente non avrei mai scritto nulla,

perche c’e la tendenza,quando s’incomincia a imparare realmente qualcosa,

a non volerne scrivere ma piuttosto a continuare a studiarla. . .non accade mai che siate in grado di dire:

adesso so tutto su questa cosa e voglio scriverne.Certamente non dico questo ora. . .

ma so delle cose che potrebbero essere interessanti adesso. . .

e allora tanto vale che scriva adesso quello che so gia.

— ERNEST HEMINGWAY, in Morte nel Pomeriggio (1932)

8

Capitolo 2

Preliminari

In questo capitolo vengono introdotte le notazioni e i concetti base chesaranno utilizzati nel seguito.

2.1 Notazione basilare

Sia S un insieme, se S e l’insieme vuoto allora si scrive S = ∅, inoltre

|S| denota la cardinalita di S; se S e un insieme finito allora |S| e il numerodi elementi di S; se S puo essere messo in corrispondenza biunivoca conl’insieme dei numeri naturali N allora si dice che e infinito e numerabileoppure che ha la potenza del numerabile oppure che ha cardinalita ℵ0

e si scrive |S| = ℵ0; per contro, le espressioni “S e finito” e |S| < ℵ0

sono equivalenti;

℘(S) denota l’insieme di tutti i sottoinsiemi di S, anche detto insieme delleparti di S o insieme potenza di S;

℘f (S) denota l’insieme di tutti i sottoinsiemi finiti di S;

S∗ denota l’insieme delle sequenze, possibilmente vuote o infinite, di ele-menti di S; la sequenza vuota si indica con λ;

S+ denota l’insieme delle sequenze, possibilmente infinite ma non vuote (ameno che non sia S = ∅), di elementi di S;

S∗f denota l’insieme delle sequenze finite, possibilmente vuote, di elementidi S;

S+f denota l’insieme delle sequenze finite e non vuote (a meno che non siaS = ∅) di elementi di S;

9

Siano S e T due insiemi. La notazione S ⊆f T significa S ⊆ T e |S| < ℵ0,ovvero che S e un sottoinsieme finito di T .

Se f :A→ B e una funzione e S ⊆ A, allora si pone

f(S) = f(x) | x ∈ S ⊆ B.

2.2 Specifiche algebriche

Definizione 2.2.1 Una “segnatura” Σ e una coppia

Σ = (S,Op)

dove S e un insieme non vuoto di “sorte” (simboli che denotano insiemi), e

Op =⋃

a∈S∗f ,s∈S

Opsa,

dove ∀a ∈ S∗f e ∀s ∈ S gli Opsa sono gli insiemi, a due a due disgiunti,dei “simboli di operatore” con “sorte argomento” a e “sorta risultato” s.Un “simbolo di costante” N ∈ Opsλ viene denotato con N : → s, mentreun “simbolo di operazione” N ∈ Opsa dove a = s1 · · · sn viene denotato conN : s1 · · · sn → s.

Definizione 2.2.2 Un’algebra A = (SA,OpA) di segnatura Σ = (S,Op), oΣ-algebra, e costituita da due famiglie

SA =(As

)s∈S

, OpA =(NA

)N∈Op

,

dove

1. ∀s ∈ S, As e un insieme, detto “insieme base” di A;

2. per ogni simbolo di costante N : → s (ovvero N ∈ Opsλ), NA e unelemento di As ed e chiamato una “costante” di A;

3. ∀s1 · · · sn ∈ S+f , per ogni simbolo di operazione N : s1 · · · sn → s (ovvero

N ∈ Opss1···sn), NA : As1 × · · · × Asn → As e una funzione, detta“operazione” di A.

Definizione 2.2.3 Data una segnatura Σ = (S,Op), X e un “insieme divariabili su Σ” se

X =⋃s∈S

Xs

dove, ∀s ∈ S, Xs e l’insieme delle “variabili di sorta s”. Gli insiemi dellevariabili Xs sono a due a due disgiunti e sono inoltre disgiunti da Op.

10

Definizione 2.2.4 Data una segnatura Σ = (S,Op) e un insieme X divariabili su Σ, si definisce “insieme dei termini di sorta s”, indicato conT sOp(X), il piu piccolo insieme induttivo tale che:

T sOp(X) ⊇ Xs;

T sOp(X) ⊇ Opsλ;

T sOp(X) ⊇

N(t1, . . . , tn)

∣∣∣∣∣∣N ∈ Op,N : si1 , . . . , sim → s,t1 ∈ T s1Op(X), . . . , tm ∈ T smOp (X)

.

Si definisce “insieme dei termini ground di sorta s”, T sOp, l’insieme

T sOp = T sOp(∅).

Unendo rispetto alle sorte, si dicono “insieme dei termini” e “insieme deitermini ground”, rispettivamente, gli insiemi

TΣ(X) = TOp(X) =⋃s∈S

T sOp(X), TΣ = TOp =⋃s∈S

T sOp .

Teorema 2.2.1 (Induzione Strutturale) [23]. Sia p un predicato definitosui termini t ∈ TΣ(X) di una segnatura Σ = (S,Op) con variabili in X.L’asserzione p(t) e vera per ogni t ∈ TΣ(X) se sono soddisfatte le seguenticondizioni:

1. [Base di induzione strutturale] p(t) e vero per ogni simbolo di costante t :→ s in Op e per ogni variabile t ∈ X;

2. [Passo di induzione strutturale] per ogni termine N(t1, . . . , tn) ∈ TΣ(X), sep(t1), p(t2), . . . e p(tn) sono veri, allora anche p(N(t1, . . . , tn)) e vero.

Definizione 2.2.5 Data una segnatura Σ = (S,Op) e un insieme di variabiliX su Σ, la Σ-algebra TΣ = (ST ,Op T ) e cosı definita:

1. ST =(T sOp(X)

)s∈S e la famiglia degli insiemi base;

2. Op T 3 NT = N per ogni simbolo di costante N :→ s in Op;

3. Op T 3 NT : T s1Op(X) × · · · × T smOp (X) → T sOp(X) per ogni simbolo dioperazione N : s1 · · · sn → s in Op; NT e definita da

NT (t1, . . . , tm) = N(t1, . . . , tm),

dove ti ∈ T siOp(X) con i = 1, . . . ,m;

11

4. Op T non contiene altri elementi oltre a quelli esplicitati nei punti 2 e3.

TΣ e detta “algebra di termini” su Σ e X.

Definizione 2.2.6 Siano A e B due Σ-algebre con Σ = (S,Op). Un “mor-fismo” h:A→ B, anche detto Σ-morfismo, e una famiglia di funzioni

hs:As → Bs, ∀s ∈ S,

tale che, per ogni s ∈ S e per ogni simbolo di costante N :→ s in Op

hs(NA) = NB,

e, per ogni simbolo di operazione N : s1 · · · sm → s in Op, per ogni ei ∈ Asicon i ∈ 1, . . . ,m,

hs(NA(e1, . . . , em)) = NB(hs1(e1), . . . , hsm(em)).

Un morfismo h:A→ B e detto un “isomorfismo”, scritto h:A ' B, se tuttele funzioni hs:As → Bs, per s ∈ S, sono biiettive.Le algebre A e B sono dette “isomorfe”, scritto A ' B, se esiste un isomor-fismo h:A ' B oppure g:B ' A.

Teorema 2.2.2 L’algebra dei termini TΣ e “iniziale” nella classe di tuttele Σ-algebre, nel senso che esiste un unico morfismo dall’algebra TΣ in ognialtra Σ-algebra.

Definizione 2.2.7 Sia A una Σ-algebra con Σ = (S,Op). Una relazione diequivalenza su A, ovvero una famiglia di relazioni di equivalenza ≈s su Asper ogni s ∈ S, e una “relazione di congruenza su A” se risulta

(∀i = 1, . . . , n, ai ≈si bi) ⇒ NA(a1, . . . , an) ≈s NA(b1, . . . , bn),

per ogni simbolo di operazione N : s1 · · · sn → s, con n ≥ 1, in Op e per ogniai, bi ∈ Asi.

Definizione 2.2.8 Siano A una Σ-algebra con Σ = (S,Op) e ≈A una re-lazione di congruenza su A. La Σ-algebra “quoziente di A rispetto a ≈A” edefinita come segue:

A/≈A =(

(Qs)s∈S, (NQ)N∈Op

),

con

12

1. Qs = [a] | a ∈ As per ogni s ∈ S, dove la classe di congruenza [a] edefinita da [a] = b ∈ As | a ≈s b ;

2. NQ = [NA] per ogni simbolo di costante N :→ s in Op e s ∈ S;

3. NQ:Qs1×· · ·×Qsn → Qs e una funzione, per ogni simbolo di operazioneN : s1 · · · sn → s in Op, definita da

NQ([a1], . . . , [an]) = [NA(a1, . . . , an)]

per ai ∈ Asi e i = 1, . . . , n.

2.3 Strutture algebriche

Definizione 2.3.1 Una “struttura algebrica” o “algebra mono-sortale” euna coppia (S,Q), dove

1. S e un insieme non vuoto detto “insieme base” o “carrier”;

2. Q e una funzione definita su un insieme di indici I, possibilmente in-finito non numerabile, tale che, ∀i ∈ I, Q(i) e un’operazione finitaria(ovvero n-aria con n finito, possibilmente nullo) da elementi di S adelementi di S. Ad esempio, se Q(i) e n-aria, allora

Q(i):

n︷ ︸︸ ︷S × · · · × S → S.

Anziche con la coppia (S,Q), nel seguito le algebre saranno usualmentedenotate con una (k + 1)-pla

(S, o1, . . . , ok)

dove S e il medesimo insieme non vuoto della definizione, e o1, . . ., ok sonoalcune operazioni nel codominio di Q. L’arieta delle oi sara specificata divolta in volta.

Definizione 2.3.2 Un’algebra

A = (L,⊗,⊕)

con le due operazioni binarie ⊗ (detto “meet”) e ⊕ (detto “join”) e un“reticolo” se valgono, ∀x, y, z ∈ L, le seguenti identita:

L1(a) : x⊗ y = y ⊗ x,

13

L1(b) : x⊕ y = y ⊕ x, [leggi commutative]

L2(a) : x⊗ (y ⊗ z) = (x⊗ y)⊗ z,

L2(b) : x⊕ (y ⊕ z) = (x⊕ y)⊕ z, [leggi associative]

L3(a) : x⊗ x = x,

L3(b) : x⊕ x = x, [leggi di idempotenza]

L4(a) : x⊗ (x⊕ y) = x,

L4(b) : x⊕ (x⊗ y) = x. [leggi di assorbimento]

Definizione 2.3.3 Una relazione binaria ≤ definita su un insieme S e una“relazione di ordinamento parziale” su S se le seguenti condizioni valgonoidenticamente in S, ∀a, b, c ∈ S,

O1 : a ≤ a, [riflessivita]

O2 : (a ≤ b) ∧ (b ≤ a)⇒ a = b, [antisimmetria]

O3 : (a ≤ b) ∧ (b ≤ c)⇒ a ≤ c. [transitivita]

Se inoltre, ∀a, b ∈ S, vale

O4 : (a ≤ b) ∨ (b ≤ a),

allora ≤ e detta “relazione di ordinamento totale” su S.

Definizione 2.3.4 Un insieme non vuoto P equipaggiato con una relazionedi ordinamento parziale ≤ su P e chiamato “insieme parzialmente ordinato”o “poset”. Se ≤ e una relazione di ordinamento totale su P , allora P vienedetto “insieme totalmente ordinato” o “catena”. In un insieme parzialmenteordinato si usa l’espressione a < b con il significato a ≤ b ma a 6= b.

Definizione 2.3.5 Sia (P,≤) un poset e sia A ⊆ P . Un elemento p ∈ P eun “limite superiore” per A se a ≤ p per ogni a ∈ A. Un elemento p ∈ Pe il “sup” di A, scritto p = sup(A), se p e un limite superiore per A e, perogni altro limite superiore p′ per A, risulta p ≤ p′. In modo del tutto analogoun elemento p ∈ P e un “limite inferiore” per A se p ≤ a per ogni a ∈ A.Un elemento p ∈ P e detto “inf” di A, scritto p = inf(A), se p e un limiteinferiore per A e, per ogni altro limite inferiore p′ per A, risulta p′ ≤ p.

Definizione 2.3.6 Un poset (D,≤) e un “cpo”, o “dominio”, se e solo seha un elemento minimo e, per ogni catena K ⊆ D, esiste sup(K) ∈ D.

14

Definizione 2.3.7 Un insieme parzialmente ordinato L e un “reticolo” se esolo se, ∀a, b ∈ L, esistono in L sia supa, b che infa, b.

Proposizione 2.3.1 [10] Le definizioni di reticolo 2.3.2 e 2.3.7 sono equi-valenti. Inoltre, se L e un reticolo per la prima definizione, la secondadefinizione si ottiene ponendo, ∀a, b ∈ L,

a ≤ b ⇐⇒ a⊗ b = a ⇐⇒ a⊕ b = b.

Viceversa, se L e un reticolo per la seconda definizione, la prima definizionesi ottiene ponendo, ∀a, b ∈ L,

a⊗ b = infa, b e a⊕ b = supa, b.

Le due trasformazioni sono inverse l’una dell’altra.

Definizione 2.3.8 Un reticolo L e un “reticolo distributivo” se e solo sesoddisfa, ∀x, y ∈ L le seguenti identita:

D1 : x⊗ (y ⊕ z) = (x⊗ y)⊕ (x⊗ z),

D2 : x⊕ (y ⊗ z) = (x⊕ y)⊗ (x⊕ z). [leggi distributive]

Proposizione 2.3.2 [10] Un reticolo soddisfa D1 se e solo se soddisfa D2.

Definizione 2.3.9 Un poset P e “completo” se, per ogni A ⊆ P esistono inP sia sup(A) che inf(A). Tutti i poset completi sono reticoli e un reticolo Lche e completo come poset e detto “reticolo completo”.

Proposizione 2.3.3 [10] Sia P un poset tale che esista sup(A) per ogniA ⊆ P , oppure tale che esista inf(A) per ogni A ⊆ P . Allora P e un reticolocompleto.

Nella precedente proposizione l’esistenza di sup(∅) garantisce l’esistenzadi un elemento minimo in P e, similmente, l’esistenza di inf(∅) garantiscel’esistenza di un elemento massimo in P . Si puo percio riformulare la pro-posizione 2.3.4 in un modo equivalente e che sara spesso usato in questatesi.

Proposizione 2.3.4 [10] Un poset P e completo se possiede un elementominimo ed esiste sup(A) per ogni A sottoinsieme non vuoto di P , oppure sepossiede un elemento massimo ed esiste inf(A) per ogni A sottoinsieme nonvuoto di P .

15

Definizione 2.3.10 [10] Un’algebra

(L,⊗,⊕,>,⊥)

con due operatori binari e due operatori nullari e un “reticolo limitato” sesoddisfa ∀x ∈ L:

B1 : (L,⊗,⊕) e un reticolo,

B2(a) : x⊗⊥ = ⊥,

B2(b) : x⊕> = >. [leggi di annichilazione]

Si osservi che se (L,⊗,⊕) e un reticolo completo, allora

(L,⊗,⊕, sup(L), inf(L))

e un reticolo limitato. In questa tesi si utilizzera talvolta la nozione di reticololimitato e completo, ma al solo scopo di esibire, assieme al carrier e aglioperatori, anche gli elementi estremi (massimo e minimo) dell’algebra.

Definizione 2.3.11 Un “monoide” e un’algebra

(M, ·, 1)

con un operatore binario “ ·” e un operatore nullario “ 1” che soddisfa, ∀x, y, z ∈M le seguenti identita:

M1 : x · (y · z) = (x · y) · z, [legge associativa]

M2 : x · 1 = 1 · x = 1. [legge dell’unita]

Un “monoide commutativo” e un monoide che soddisfa, ∀x, y ∈M ,

M3 : x · y = y · x.

Un “monoide idempotente” e un monoide che soddisfa, ∀x ∈M ,

M4 : x · x = x.

In questo lavoro avremo bisogno di definire diverse relazioni di ordinamen-to, poset, reticoli e algebre. Per facilitare la lettura useremo una notazioneche permetta di stabilire facilmente su quale insieme sono definiti i vari or-dinamenti, operatori e cosı via. Ad esempio, se B e un insieme parzialmenteordinato, la relazione d’ordine corrispondente sara denotata con ≤B. Il sim-bolo ≤ sara utilizzato solo per denotare l’usuale ordinamento sui numeri.Qualora B sia un poset o un reticolo completo gli operatori sup e inf definitisu ℘(B) saranno denotati con supB e infB. In un’algebra definita sul carrierB gli operatori saranno denotati con simboli indicizzati del tipo ⊗B, ⊕B, >B,⊥B

16

2.4 Interpretazione astratta

Riassumiamo brevemente la nozione di interpretazione astratta introdotta in[13]. Consideriamo un dominio concreto DP , ovvero un insieme di rappre-sentazioni di stati computazionali associati ad un generico programma P .Assumiamo che DP sia un reticolo completo rispetto ad un ordinamento par-ziale ≤DP . Sia inoltre EP :DP → DP una funzione di transizione di stato suDP e supponiamo che il “comportamento computazionale” di P sia comple-tamente caratterizzato dall’equazione x = EP (x). Possiamo quindi affermareche la tripla (DP ,≤DP , EP ) definisce una semantica di punto fisso standard(o concreta) per il programma P . Dal momento che le computazioni possonoessere infinite questa definizione non puo essere utilizzata per l’analisi staticadei programmi. Per questo motivo si definisce una semantica di punto fissonon standard basata su un dominio astratto D]

P , usualmente finito, che ga-rantisca la finitezza dell’analisi. Tale semantica e detta semantica astratta ede anch’essa definita da una tripla (D]

P ,≤D]P , E]P ). Ovviamente la semantica

astratta e, in generale, soltanto un’approssimazione di quella concreta.La relazione tra la semantica standard e quella astratta e stata stabilita

in [13] definendo una coppia di funzioni, α e γ (astrazione e concretizza-zione), che formano una connessione di Galois tra (D]

P ,≤D]P ) e (DP ,≤DP )

[32, 44, 48]. Questa nozione consente di definire formalmente la condizionedi corretteza di uno schema di interpretazione astratta [6]. Formalmente unoschema di interpretazione astratta [13, 42] e una tupla

〈(DP ,≤DP ), EP , (D]P ,≤D]P ), E]

P , α, γ〉

tale che

1. (DP ,≤DP ) e (D]P ,≤D]P ) sono reticoli completi,

2. EP :DP → DP e E]P :D]

P → D]P sono funzioni monotone,

3. α:DP → D]P e γ:D]

P → DP sono funzioni monotone,

4. ∀d] ∈ D]P , α(γ(d])) ≤D]P d

],

5. ∀d ∈ DP , d ≤DP γ(α(d)).

Le ultime tre condizioni definiscono una connessione di Galois tra il do-minio astratto e quello concreto. Una inserzione di Galois e una connessionedove γ e iniettiva o, equivalentemente, α γ e la funzione identita su D]

P

[44, 48]. Si osservi che γ e iniettiva se e soltanto se α e suriettiva [44].

17

Le connessioni di Galois impongono una relazione molto forte tra il domi-nio concreto della computazione e quello, usualmente piu semplice, associatoall’analisi (il dominio astratto). La loro utilita, originariamente esposta in[13, 15], e quella di consentire, in modo agevole, di dimostrare la correttezzadi un’interpretazione astratta. Un’inserzione di Galois assicura che il domi-nio astratto D]

P non contiene elementi ridondanti, inoltre la concretizzazionenon causa alcuna perdita di informazione. D’altra parte la condizione 5 dicui sopra (che e comune alle connessioni e alle inserzioni di Galois) illustrail fatto che l’astrazione di un oggeto concreto puo comportare, come e logicoattendersi, perdita di informazione.

Data una connessione di Galois 〈α, γ〉 tra i reticoli completi (DP ,≤DP ) e(D]

P ,≤D]P ), valgono i seguenti risultati [44, 48, 32]:

• α e γ si determinano univocamente l’un l’altra,

• γ preserva meet arbitrari, ovvero

∀B] ⊆ D]P , infDP γ(d]) | d] ∈ B] = γ(infD]P

B]),

• α preserva join arbitrari (e addittiva), ovvero

∀B ⊆ DP , supD]Pα(d) | d ∈ B = α(supDPB).

L’analisi di un programma e condotta calcolando una sequenza finitaE]n

P (⊥D]P )n∈1,...,k

di approssimazioni, calcolabili finitamente, della soluzione semantica dell’e-quazione ricorsiva x = EP (x). La correttezza delle approssimazioni puoessere data in termini di una delle seguenti condizioni [13, 15]:

1. ∀d ∈ DP , α(EP (d)) ≤D]P E]P (α(d)),

2. ∀d] ∈ D]P , EP (γ(d])) ≤DP γ(E]

P (d])).

Proposizione 2.4.1 [13] La condizione 1 implica la condizione 2.

Nel caso in cui 〈α, γ〉 sia un’inserzione di Galois vale anche il viceversa.In tal caso le condizioni 1 e 2 sono equivalenti.

18

2.5 Lo schema CLP

Richiamiamo qui brevemente alcuni concetti base di CLP come sono stati de-finiti in [33]. Lo schema CLP e definito usando un linguaggio del prim’ordinemulti-sortato, che puo essere rappresentato con una “segnatura” del tipo:

sort S :s1, . . . , sn

opns Ω :ωi : si1 , . . . sili → shi i1, . . . , ili , hi ∈ 1, . . . , n...

...pred ΠC :

πCj : sj1 , . . . sjlj j1, . . . jlj ∈ 1, . . . , n...

...pred ΠP :

πPk : sk1 , . . . sklk k1, . . . klk ∈ 1, . . . , n...

...

Si assume ΠC ∩ ΠP = ∅ e Π = ΠC ∪ ΠP . Si definisce poi l’insieme S-sortatodi variabili

V =⋃

i∈1,...,n

Vsi ,

dove, ∀i = 1, . . . , n,|Vsi| = ℵ0,

∀i, j ∈ 1, . . . , n,i 6= j ⇒ Vsi ∩ Vsj = ∅.

e, infine,V ∩ (Ω ∪ ΠC ∪ ΠP ) = ∅.

Dunque Ω, Π e V sono insiemi numerabili di, rispettivamente, simboli difunzione, simboli di predicato e variabili, ciascuno con la propria segnatura.T (Ω∪V ) e T (Ω) denotano l’insieme dei termini e l’insieme dei termini ground(senza variabili) costruiti su Ω e V . Un (Π,Ω)-atomo e un oggetto del tipop(t1, . . . , tn) dove p ∈ Π e n-ario e ti ∈ T (Ω ∪ V ) per ogni i = 1, . . . , n. Un(Π,Ω)-vincolo e una congiunzione possibilmente vuota o infinita di (Π,Ω)-atomi. Il vincolo vuoto viene denotato con true.

Definizione 2.5.1 Un (Π,Ω)-programma (CLP) e un insieme finito di clau-sole della forma

H :− c . oppure H :− c B1, . . . , Bm.

19

dove c e un (ΠC ,Ω)-vincolo finito e H (la testa), B1, . . ., Bm (il corpo) sono(ΠP ,Ω)-atomi.

Nello schema CLP(X ), X denota uno specifico dominio di vincoli sulquale e eseguita la computazione. La nozione di struttura fornisce un’inter-pretazione semantica di tale dominio ed e l’elemento chiave della semanticaalgebrica dei linguaggi CLP.

Definizione 2.5.2 Una struttura X (Π,Ω) definita sugli alfabeti S-sortati Πe Ω di simboli di predicato e di funzione, dove Π contiene il simbolo speciale“=”, consiste:

• di una collezione S-sortata DX = DXss∈S di insiemi non vuoti;

• dell’assegnamento di una funzione

fX :DXs1 × · · · ×DXsn → DXs

ad ogni simbolo di funzione f : s1 · · · sn → s in Ω;

• dell’assegnamento di una funzione

pX :DXs1 × · · · ×DXsn → true, false

ad ogni simbolo di predicato in p ∈ ΠC, eccetto “=” che e interpretatocome uguaglianza sintattica.

Definizione 2.5.3 Una X (Π,Ω)-valutazione e una funzione θ:V → DXtale che, per ogni X ∈ V e per ogni s ∈ S

X ∈ Vs ⇒ θ(X) ∈ DXs.

La nozione di X (Π,Ω)-valutazione si estende in modo ovvio ai termini, aivincoli e agli insiemi di vincoli. Nel seguito denotiamo la struttura X (Π,Ω)semplicemente con X .

Definizione 2.5.4 Un (Π,Ω)-vincolo e X -soddisfacibile se e solo se esisteuna X -valutazione θ tale che X |= cθ (cθ e X -equivalente a true). In tal casosi dice che θ e una X -soluzione per c. Se C e un insieme di (Π,Ω)-vincoli siscrive X |= Cθ se e solo se ∀c ∈ C, X |= cθ.

Le strutture considerate nello schema CLP sono compatte rispetto allesoluzioni come definite in [33, 34]. Quando non ci si occupi della negazione esufficiente che le strutture soddisfino la seguente condizione: per ogni sorta se per ogni d ∈ DXs esiste un insieme C di vincoli sulla variabile X tale che,per ogni X -soluzione θ di C, risulta Xθ = d.

20

Definizione 2.5.5 Sia P un (Π,Ω)-programma. Un “X -passo di derivazio-ne” di un goal

G = (:− c A1, . . . , An),

nel contesto del programma P , risulta in un goal

G′ = (:− c B1, . . . , Bn),

ed e denotato da

(:− c A1, . . . , An)(P,X )−→ (:− c B1, . . . , Bn)

se esistono n varianti di clausole in P ,

Hi :− ci Bi, per i = 1, . . . , n,

senza variabili in comune tra loro e con G, tali che

c = c, c1, . . . , cn, A1 = H1, . . . , An = Hn

sia X -soddisfacibile.

Definizione 2.5.6 Una “X -derivazione” di un goal G nel contesto di unprogramma P e una sequenza finita o infinita di goal, tale che ogni goalnella sequenza, eccetto G, sia ottenuto da quello precedente per mezzo diun X -passo di derivazione. Una “X -derivazione con successo” e una “X -derivazione” finita tale che l’ultimo suo elemento e un goal della forma (:−c ). In tal caso c e detto “vincolo di risposta” della derivazione.

21

Capitolo 3

Semantica generalizzata di CLP

La programmazione logica con vincoli e una generalizzazione del paradigmadella programmazione logica pura, ed ha caratterizzazioni semantiche deltutto simili, sia model-theoretic che operazionali [33]. Dal momento peroche il passo operazionale base (nell’esecuzione di un programma) e il test disoddisfacibilita di un vincolo su una struttura algebrica, CLP ha anche unasemantica algebrica. In questo contesto, quando si consideri il paradigmaCLP nella sua generalita, e importante distinguere il calcolo delle soluzionidi un vincolo su un dato dominio dal semplice controllo di risolubilita delvincolo stesso. Nel caso della programmazione logica ordinaria entrambequeste operazioni corrispondono al processo di unificazione, che controllala soddisfacibilita di un vincolo calcolandone la soluzione piu generale (uninsieme di equazioni in forma risolta o mgu). In CLP il calcolo delle soluzionidi un vincolo e demandato ad un risolutore di vincoli che, purche sia corretto,non influenza la definizione semantica del linguaggio. Dal momento che gliaspetti linguistici fondamentali del paradigma CLP possono essere separatidai dettagli relativi al particolare sistema di vincoli sui quali e istanziato,viene spontaneo parametrizzare la semantica dei linguaggi CLP rispetto aisistemi di vincoli [52]. Una tale definizione semantica viene detta semanticageneralizzata. Questo approccio fornisce un potente strumento per trattarevarie applicazioni correlate con la semantica dei programmi CLP. Ad esempio,considerando un dominio di “vincoli astratti” invece dei “vincoli concreti”che sono manipolati nell’esecuzione dei programmi, si ottiene una definizionegenerale e formale dell’interpretazione astratta dei programmi CLP.

In questo capitolo definiremo due tipi di semantica algebrica generalizzatadei programmi CLP, top-down e bottom-up. Dal momento che le computa-zioni sono comunque svolte nell’algebra dei vincoli, i due tipi di semanticasono semplicemente due modi per rappresentare le computazioni. Il parti-colare approccio algebrico identifica un insieme di operatori che, opportuna-

22

mente istanziati, consentono di ottenere la definizione di svariate semantichenon standard. Un aspetto interessante di questa trattazione e che le in-terpretazioni non standard, quali l’interpretazione astratta, possono esseresviluppate completamente all’interno di uno schema algebrico. Ad esem-pio, la nozione di “astrazione” puo essere caratterizzata semplicemente comel’aggiunta di assiomi che specifichino quali oggetti semanticamente rilevantidebbano essere considerati “uguali”. La relazione tra diverse intepretazioniastratte puo invece essere caratterizzata per mezzo di morfismi tra le algebrecorrispondenti.

Il materiale di questo capitolo e, in larga misura, tratto da [27]. Le di-mostrazioni dei principali risultati sono in [28]. Va osservato che la scelta dibasarsi sulla trattazione in [27] non era l’unica possibile. Esistono infatti altrecaratterizzazioni algebriche di particolari sistemi di vincoli [52, 12]. Ad esem-pio in [52] vengono introdotte delle strutture algebriche, dette informationsystems per la specifica semantica della classe (piu complessa di CLP) deilinguaggi concorrenti con vincoli basati sul paradigma ask/tell . Lo schemapresentato in [52] e molto elegante, ma e orientato allo sviluppo di semantichestandard per i linguaggi concorrenti con vincoli. In questa tesi siamo invecepiu interessati a semantiche non standard (principalmente l’interpretazioneastratta) che consentano di generalizzare i risultati semantici classici di CLP.Un’altra considerazione da fare e che, mentre in [52] vengono amalgamatitermini, vincoli e costruzione della semantica, in [27] questi tre componentidi una definizione semantica vengono mantenuti distinti. Cio risulta in unamaggiore semplicita di definizione delle interpretazioni astratte. Infatti, in[27], i sistemi di vincoli sono parametrizzati rispetto ai sistemi di termini.L’approccio alla costruzione di sistemi di vincoli non standard e quindi, con-sistendo di due passi distinti, piu strutturato. Inoltre l’indipendenza dellacostruzione semantica dal sistema di vincoli permette di concentrarsi sulladefinizione di quest’ultimo, rendendo piu semplice la specifica di semantichenon standard quali l’interpretazione astratta.

Il presente capitolo e cosı suddiviso: nella sezione 3.1 viene data una spe-cifica algebrica dei sistemi di vincoli. Nella sezione 3.2 sono definite le seman-tiche, parametrizzate rispetto al sistema di vincoli, operazionale (top-down)e di punto fisso (bottom-up) per i programmi logici con vincoli. Infine, nellasezione 3.3, lo schema di semantica generalizzata viene applicato all’analisidata-flow dei programmi CLP mediante interpretazione astratta.

23

3.1 Algebre di vincoli

Seguendo la trattazione in [33], la semantica dei vincoli di un linguaggio CLPe definita in termini di una struttura algebrica che intepreta le formule divincoli , mentre la semantica di un programma logico con vincoli e data intermini delle usuali caratterizzazioni di punto fisso, model-theoretic e opera-zionale. In questa sezione introduciamo una specifica algebrica incrementaleper i sistemi di vincoli.

3.1.1 Sistemi di termini

Come primo passo della specifica incrementale dei sistemi di vincoli, definia-mo ora un sistema di termini come un’algebra di termini1 con una famigliadi operatori binari che realizza le sostituzioni [11].

Definizione 3.1.1 Un “sistema di termini” Υ e un’algebra

Υ = (Υ, sx, x)sx∈S;x∈V ,

dove Υ, S e V sono insiemi. Gli elementi di Υ sono detti “Υ-termini”, Ve un insieme numerabile di “Υ-variabili” mentre S e un insieme numerabiledi operatori binari su Υ indicizzati con elementi di V . Il sistema di terminiΥ soddisfa i seguenti assiomi, ∀x, y ∈ V e ∀t, t′, t′′ ∈ Υ:

T1 : sx(t, x) = t, [identita]

T2 : sx(t, y) = y, se x 6= y, [annichilazione]

T3 : sx(t, sx(y, t′)) = sx(y, t

′), se x 6= y, [ridenominazione]

T4 : sx(t′, sy(t

′′, t)) = sy(sx(t′, t′′), sx(t

′, t)), se x 6= y e y ind t′,[composizione indipendente]

dove un Υ-termine t e “indipendente” dalla Υ-variabile x, scritto x ind t, see soltanto se

∀t′ ∈ Υ, sx(t′, t) = t.

Diremo invece che la Υ-variabile x “occorre” nel Υ-termine t se e solo se¬(x ind t). L’insieme delle variabili che occorrono in t sara indicato convars(t).

1Nulla a che vedere con “l’algebra dei termini” su una segnatura.

24

Nel seguito prenderemo la liberta di indicare un sistema di termini Υ conla tripla (Υ, S, V ). Inoltre, quando sia chiaro dal contesto a quale sistemadi termini Υ si faccia riferimento, chiameremo, per brevita, termini i Υ-termini e variabili le Υ-variabili. La nozione di sistema di termini e del tuttogenerale; in realta siamo interessati ai sistemi di termini localmente finitio finitari ovvero nei quali i termini dipendono solo da un numero finito divariabili.

Definizione 3.1.2 Un sistema di termini Υ = (Υ, S, V ) e “finitario” se esolo se ∀t′ ∈ Υ,

x ∈ V | ∃t ∈ Υ . sx(t, t′) 6= t′ ⊆f V.

Intuitivamente sx(t, t′) denota l’elemento di Υ ottenuto sostituendo nel

termine t′ tutte le occorrenze della variabile x con il termine t. Si noti peroche, nel contesto della semantica generalizzata che stiamo costruendo, leparole termine e sostituzione non vanno necessariamente interpretate con illoro significato classico. Qui un termine e un qualunque oggetto, le variabilisono particolari termini e le sostituzioni sono operatori binari che soddisfanogli assiomi della definizione 3.1.1. Le interpretazioni classiche di termini,variabili e sostituzioni sono casi particolari di questa definizione.

Esempio 3.1.1 Sia Ω un insieme numerabile di simboli di funzione di unasegnatura mono-sortale Σ, e sia Vars un insieme numerabile di simboli divariabile. Allora TΩ(Vars) denota l’insieme dei termini, non necessariamenteground, su Ω e Vars. Se Sub e l’insieme delle sostituzioni idempotenti suVars e Ω [38], allora

Υst = (TΩ(Vars), Sub,Vars)

e un sistema di termini finitario secondo le definizioni 3.1.1 e 3.1.2 (e anchesecondo l’intuizione classica). La necessita dell’idempotenza delle sostituzioniin Sub e implicata dall’assioma di ridenominazione (T3) della definizione3.1.1. Υst viene detto “sistema di termini standard”.

Vediamo ora un’istanza non standard della struttura algebrica “sistemadi termini”.

Esempio 3.1.2 Sia Φ un insieme possibilmente infinito e numerabile di sim-boli e sia S = (sφ)φ∈Φ la famiglia degli operatori binari tali che, ∀φ ∈ Φ e∀∆1,∆2 ∈ ℘f (Φ),

sφ(∆1,∆2) =

(∆2 \ φ) ∪∆1 se φ ∈ ∆2,∆2 altrimenti.

25

In questo caso, ∀φ ∈ Φ e ∀∆ ⊆f Φ, risulta φ ind ∆ se e solo se φ /∈ ∆. Siaora Φ1 cosı definito:

Φ1 = φ | φ ∈ Φ ⊆ ℘f (Φ),

e consideriamo l’algebra

ΥΦ = (℘f (Φ), S,Φ1).

Si dimostra [28] che ΥΦ e un sistema di termini finitario.

Nel seguito considereremo solo sistemi di termini finitari. Si osservi inoltreche i sistemi di termini qui introdotti sono tutti one-sorted , ovvero i terminisono tutti dello stesso “tipo”. Questa caratterizzazione e pero sufficienteper il presente lavoro di tesi, poiche vi si considerano solo linguaggi, istanzedel paradigma CLP, definiti su un unico dominio numerico. Nel prosieguoassumeremo implicitamente la restrizione al caso one-sorted . Per convenienzadi notazione, denoteremo sx(t, t

′) con [t/x]t′. Questa notazione puo essereestesa a sostituzioni di piu variabili scrivendo

sx1(t1, sx2(t2, . . . , sxk(tk, t) · · ·))

come[t1/x1, . . . , tk/xk]t,

dove xi 6= xj per ogni i, j ∈ 1, . . . , k tali che i 6= j.

3.1.2 Uno schema algebrico per i sistemi di vincoli

Diamo ora una specifica algebrica formale per il linguaggio dei vincoli suun dato sistema di termini. Questo linguaggio consente di identificare quel-le strutture che devono essere definite in ogni caratterizzazione semanticastandard o non standard. Innanzitutto, il processo di costruzione dei vin-coli, in ogni valutazione basata sul punto fisso di un appropriato operatoredelle conseguenze immediate, e principalmente fondato sulla congiunzionee disgiunzione (usualmente l’unione insiemistica). La specifica algebrica dellinguaggio dei vincoli deve quindi definire gli operatori che astraggono questedue operazioni fondamentali.

Una definizione semantica supporta la nozione di comportamento osser-vabile dei programmi. Nelle semantiche dei vincoli di risposta di CLP, leproprieta osservabili dei programmi logici con vincoli sono, appunto, i vinco-li di risposta [26]. In tali semantiche, quando risolviamo un goal nel contesto

26

di un programma, siamo interessati solo ai vincoli sulle variabili che compa-iono nel goal: ogni ulteriore vincolo che sia stato imposto su altre variabilinon deve comparire nella rappresentazione del vincolo di risposta. Per questomotivo le soluzioni (astratte o concrete) devono essere ristrette (proiettate)sulle variabili della query corrispondente. Questa operazione di proiezione ecatturata, nello schema algebrico che segue, da una famiglia di operatori diquantificazione indicizzati sulle variabili del sistema di termini.

Infine, la caratterizzazione semantica di un linguaggio CLP deve consi-derare quei particolari vincoli che consentono il cosiddetto “passaggio deiparametri” [52]. Nella programmazione logica con vincoli, il simbolo diuguaglianza, “=”, e inteso come unificazione tra termini.

Definiamo ora il linguaggio dei vincoli su un sistema di termini Υ e su uninsieme di simboli di predicato

ΠC =⋃n∈N

ΠnC ,

dove ΠnC e l’insieme dei simboli di predicato in ΠC di arieta n.

Definizione 3.1.3 Sia Υ = (Υ, S, V ) un sistema di termini e ΠC un insiemedi simboli di predicato. L’insieme dei vincoli atomici su Υ e ΠC e dato da

Ca = Ca(Υ,ΠC) = π(t1, . . . , tn) | π ∈ ΠnC , t1, . . . , tn ∈ Υ .

Definiamo ora la sintassi astratta del linguaggio dei vincoli per mezzo dellasegnatura Σ = Σ(Υ,ΠC) che risulta essere mono-sortale con l’unica sorta Cdei vincoli e i simboli di operatore

true : → C,false : → C,t = t′ : → C, ∀t, t′ ∈ Υ,

ci : → C, ∀ci ∈ Ca,∃∆ : C → C, ∀∆ ⊆ V∧ : CC → C,∨ : CC → C.

Si osservi che Σ, incorporando tutti i vincoli atomici in Ca come simboli dicostante, ha un’infinita numerabile di operatori. A questo punto, il linguag-gio dei vincoli C(Υ,ΠC) e l’insieme dei termini su Σ, ovvero, seguendo ladefinizione 2.2.4,

C(Υ,ΠC) = TΣ.

Inoltre, l’algebra dei termini su Σ, TΣ, sara denotata con

Λ(Υ,ΠC) =(C(Υ,ΠC),∧,∨, true, false, ci,∃∆, t = t′

)ci∈Ca; ∆⊆V ; t,t′∈Υ

.

27

Le semantiche (standard e non-standard) di un linguaggio di vincoli C(Υ,ΠC)sono tutte univocamente determinate da particolari scelte di Σ-algebre sullequali interpretare le formule (ovvero i vincoli) del linguaggio stesso. Dicia-mo univocamente perche, per il teorema di inizialita, l’algebra di terminiΛ(Υ,ΠC) e iniziale nella classe delle Σ-algebre. Dunque, fissata una qualsia-si Σ-algebra A, esiste un solo morfismo da Λ(Υ,ΠC) in A. Tale morfismoe, per l’appunto, il morfismo di interpretazione, e dunque la semantica, dellinguaggio di vincoli C(Υ,ΠC).

Naturalmente non tutte le Σ-algebre, pur essendo interpretazioni del lin-guaggio dei vincoli, consentono di completare il processo di generalizzazionedella semantica. Il secondo passo di questo processo e la costruzione dei mo-delli di programmi con tecniche standard, ad esempio mediante punti fissidi funzioni continue. Inoltre siamo interessati ad ottenere, per le definizionisemantiche, risultati classici quali l’equivalenza tra semantica model-theoretice operazionale. Occorre dunque definire ulteriormente lo schema algebricodelle strutture sulle quali interpretare i vincoli.

Vediamo ora una struttura algebrica che si presta a modellare le opera-zioni di congiunzione e disgiunzione nel processo di costruzione dei vincoli.

Definizione 3.1.4 Un “semianello chiuso” [1] e una struttura algebrica

(C,⊗,⊕, 1, 0)

con due operatori binari e due operatori nullari che soddisfa:

S1 : (C,⊕, 0) e un (join) monoide idempotente e commutativo;

S2 : (C,⊗, 1) e un (meet) monoide;

S3 : 0 e un annichilatore per ⊗, ovvero ∀c ∈ C, c⊗ 0 = 0⊗ c = 0;

S4 : se a1, a2, . . . , an, . . . e una successione di elementi di C, allora l’elementoa1 ⊕ a2 ⊕ · · · ⊕ an ⊕ · · · esiste in C ed e unico. Inoltre l’associativita,commutativita e idempotenza di ⊕ valgono anche per join infiniti;

S5 : ⊗ “distribuisce” su join finiti ed infiniti.

Si osservi che non viene richiesto che l’operatore che modella la congiun-zione di vincoli, “⊗”, sia commutativo. Seguono ora due esempi tratti dallaletteratura.

Esempio 3.1.3 [1] Consideriamo le strutture algebriche

AR = (R+,+,min, 0,+∞),

28

dove R+ e l’insieme dei numeri reali non negativi esteso con il simbolo +∞,e

AΩ = (℘(Ω∗f ), ·,∪, λ, ∅),

dove Ω e un insieme finito, Ω∗f e l’insieme delle stringhe finite sull’alfabetoΩ, λ rappresenta la stringa vuota e “ ·” denota l’operatore di concatenazione.Si verifica facilmente che AR e AΩ sono semianelli chiusi. Si noti che in AΩ

l’operatore “ ·” non e commutativo.

Per alcune applicazioni di analisi statica mediante interpretazione astrat-ta, i semianelli chiusi sono strutture troppo forti . Una struttura piu debole,che sara utilizzata per l’analisi del capitolo 5, e il semianello chiuso nondistributivo.

Definizione 3.1.5 Un “semianello chiuso non distributivo” e una strutturaalgebrica

(C,⊗,⊕, 1, 0)

con due operatori binari e due operatori nullari che soddisfa gli assiomi S1,S2, S3 ed S4 della definizione 3.1.4.

Nel seguito, quando la distributivita sia inessenziale, prenderemo la li-berta di indicare con il termine “semianello chiuso” sia i semianelli chiusidistributivi (secondo la definizione 3.1.4), sia quelli non distributivi (secondola definizione 3.1.5).

Dato un semianello chiuso (C,⊗,⊕, 1, 0), possiamo indurre la relazionev⊕ su C tale che, ∀c1, c2 ∈ C,

c1 v⊕ c2 ⇐⇒ c1 ⊕ c2 = c2,

per la quale valgono alcuni importanti risultati [5, 21, 28].

Proposizione 3.1.1 v⊕ e una relazione d’ordine parziale su C.

Proposizione 3.1.2 Sia c1 v⊕ c′1 e c2 v⊕ c′2. Allora

c1 ⊕ c2 v⊕ c′1 ⊕ c′2.

Proposizione 3.1.3 Il poset (C,v⊕) e un reticolo completo.

29

Come abbiamo gia ricordato, dobbiamo modellare la restrizione di unvincolo su un certo insieme di variabili. Naturalmente i semianelli chiusi nonsono sufficientemente ricchi per catturare questa nozione di proiezione, chepuo invece essere modellata, come in [52], per mezzo di una famiglia di ope-ratori di “nascondimento” sull’algebra dei vincoli. Le algebre cilindriche [31]forniscono uno schema adeguato per aumentare le nostre strutture algebriche.Un’algebra cilindrica e ottenuta, nella teoria generale, estendendo un’algebraBooleana con una famiglia di operazioni dette cilindrificazioni . Per quanto ciriguarda, l’intuizione e che, dato un vincolo c, l’operazione di cilindrificazione∃∆(c) risulta nel vincolo ottenuto “eliminando”, o “proiettando fuori”, da cle informazioni circa le variabili in ∆. Tecnicamente le algebre cilindricheconsentono di eseguire proiezioni su insiemi finiti di variabili. Dal momentopero che la nostra formulazione semantica e basata, come si vedra in seguito,su unfolding infiniti, puo essere necessario consentire proiezioni su insiemiinfiniti di variabili. Le algebre cilindriche sono pertanto inadeguate a questoscopo, ma il problema puo essere risolto ricorrendo alle estensioni poliadiche[31], che permettono cilindrificazioni numerabili.

Le algebre cilindriche danno anche una risposta parziale al problema dimodellare il passaggio dei parametri. Con questo obiettivo, in [52] sonoconsiderati gli elementi diagonali [31] delle algebre cilindriche. Purtroppopero, le algebre cilindriche furono introdotte per dare una formalizzazionealgebrica della logica del primo ordine orientata a linguaggi senza simbolidi operazione, ignorando quindi tutti i termini tranne le semplici variabili.La definizione originale delle algebre cilindriche non e percio sufficiente perla costruzione di uno schema di semantica algebrica per programmi logicicon vincoli in senso generale. Seguendo l’approccio in [11], estendiamo lanozione di elemento diagonale definendolo su una coppia di termini generici.Gli elementi diagonali rappresentano cosı le equazioni su un dato sistema ditermini Υ.

Definizione 3.1.6 Dato un sistema di termini Υ = (Υ, S, V ), un “sistemadi vincoli su Υ” e una struttura algebrica

(C,⊗,⊕, 1, 0,∃∆, dt,t′)∆⊆V ; t,t′∈Υ ,

dove C e un insieme detto “universo del sistema di vincoli”; 1, 0 e dt,t′ sonoelementi distinti di C, per ogni t, t′ ∈ Υ; ∃∆∆⊆V e una famiglia di operatoriunari su C, mentre ⊗ e ⊕ sono operatori binari su C. Sono inoltre soddisfattii seguenti assiomi, ∀c, c′ ∈ C, ∀∆,Ψ ⊆ V e ∀t, t′ ∈ Υ:

S0 : la struttura (C,⊗,⊕, 1, 0) e un semianello chiuso distributivo,

C1 : ∃∆0 = 0,

30

C2 : c⊕ ∃∆c = ∃∆c,

C3 : ∃∆(c⊗ ∃∆c′) = ∃∆(∃∆c⊗ c′) = ∃∆c⊗ ∃∆c

′,

C4 : ∃∆∃Ψc = ∃(∆∪Ψ)c,

C5 : ∃∆ “distribuisce” su join finiti ed infinitamente numerabili,

D1 : dt,t = 1,

D2 : dt,t′ = ∃x(dt,x ⊗ dx,t′), se x ind t, t′.

Il significato della cilindrificazione e dato dagli assiomi da C1 a C5, mentregli elementi diagonali sono specificati dagli assiomi D1 e D2.

Le nozioni di indipendenza e occorrenza delle variabili si estendono nellamaniera ovvia dai termini di Υ ai vincoli di C. Sia x1, . . . , xn ⊆ V , nelseguito denoteremo ∃vars(c)\x1,...,xnc, cioe il “nascondimento” di tutte le va-riabili in c eccetto x1, . . . , xn, con ∃(c)x1,...,xn. Denoteremo inoltre cond〈t1,...,tn〉,〈t′1,...,t′n〉 l’elemento dt1,t′1 ⊗ · · · ⊗ dtn,t′n , dove t1, . . . , tn, t

′1, . . . , t

′n ∈ Υ.

Ogni semianello chiuso puo essere esteso in un sistema di vincoli ponendo

dt,t′ = 1, ∀t, t′ ∈ Υ

e∃∆c = c, ∀c ∈ C, ∀∆ ⊆ V.

Seguendo [31] chiameremo i sistemi di vincoli cosı ottenuti, sistemi di vincolidiscreti .

Nella teoria generale delle algebre cilindriche le proprieta commutativa etransitiva degli elementi diagonali (ovvero dt,t′ = dt′,t e dt,t′ ⊗ dt′,t′′ = dt,t′′)sono derivabili dagli assiomi. I nostri sistemi di vincoli sono strutture piudeboli e queste proprieta non discendono dagli assiomi della definizione 3.1.6.D’altra parte non sono necessarie per dimostrare i risultati semantici che se-guono e gli assiomi mancanti potrebbero essere aggiunti qualora si desiderassefornire una teoria dell’uguaglianza.

Definizione 3.1.7 Dato un sistema di termini Υ, un “sistema di vincolinon distributivo su Υ” e una struttura algebrica che soddisfa tutte le condi-zioni imposte dalla definizione 3.1.6 eccettuato l’assioma S0, che si intendesostituito con

S ′0 : la struttura (C,⊗,⊕, 1, 0) e un semianello chiuso non distributivo.

31

La necessita di considerare sistemi di vincoli non distributivi e emersadurante lo sviluppo di questa tesi per una delle analisi presentate nel capitolo5 e, contemporaneamente, in [28] per la definizione di un sistema di vincolidi relazioni affini, volto all’inferenza di relazioni lineari tra le variabili di unprogramma [16, 36, 58]. Di nuovo, quando la distributivita del sistema divincoli sia ininfluente, indicheremo con il termine “sistema di vincoli” sia isistemi di vincoli distributivi (secondo la definizione 3.1.6), che quelli nondistributivi (secondo la definizione 3.1.7).

Definizione 3.1.8 Dato un sistema di vincoli A con universo C, un qualsiasielemento di C viene detto “A-vincolo”.

Quando il contesto chiarisca qual e il sistema di vincoli di riferimento,chiameremo semplicemente vincoli gli A-vincoli. La definizione di sistema divincoli e stata ispirata da [21], dove un adeguato schema algebrico supportala definizione di semantiche non standard dei programmi logici. Questa no-zione e stata applicata in uno schema di interpretazione astratta in [5, 37],dove l’identificazione di un insieme minimale di operatori ha consentito diottenere uno schema generale per la definizione di semantiche astratte deiprogrammi logici. Un fondamento algebrico di queste nozioni ha il vantaggiodi trattare le semantiche non standard come istanze particolari di uno schemagenerale, semplificando in tal modo le prove di correttezza e la specifica deglistrumenti software necessari. In programmazione logica i semianelli chiu-si caratterizzano, algebricamente, in modo adeguato tutti gli aspetti dellacomposizione di termini, quali l’unificazione e l’unione insiemistica. L’idem-potenza, l’associativita e la commutativita sono le proprieta minime [5, 21]che consentono all’operatore “⊕” di modellare l’operazione di unione insie-mistica. L’operatore “⊗” corrisponde invece alla congiunzione, e modellal’accumulazione dei vincoli nel corso della computazione. La distributivitadi “⊗” su “⊕” permette, qualora sussista, di rappresentare i vincoli comejoin possibilmente infiniti di meet finiti (detti anche vincoli semplici). L’as-sioma S4 della definizione 3.1.4 consente di denotare in modo univoco join,possibilmente infiniti e numerabili, di vincoli. Per queste ragioni i sistemidi vincoli forniscono un’adeguata caratterizzazione algebrica del processo dicostruzione dei vincoli nella computazione.

Esempio 3.1.4 Consideriamo un linguaggio CLP definito sui vincoli di C(Υst ,ΠC),dove Υst e il sistema di termini definito sulla segnatura mono-sortale Σ =(s,Ω) dell’esempio 3.1.1 e ΠC =

⋃n∈N Πn

C e un insieme di simboli di pre-dicato, ciascuno con la propria arieta. Sia X (Σ,ΠC) una struttura algebrica“compatta rispetto alle soluzioni” [33] consistente:

32

• di un insieme non vuoto DX ;

• dell’assegnamento di una funzione fX :

n︷ ︸︸ ︷DX × · · · ×DX → DX ad ogni

simbolo di funzione f :

n︷ ︸︸ ︷s · · · s→ s in Ω;

• dell’assegnamento di una funzione pX :

n︷ ︸︸ ︷DX × · · · ×DX → true, false

ad ogni simbolo di predicato in ΠnC, per ogni n.

Sia c un vincolo in C(Υst ,ΠC). Le variabili libere di c vengono denotate conFV (c). Se esiste una funzione ϑ: FV (c) → DX (la soluzione di c) tale cheX |= cϑ (c e X -equivalente a true), allora c si dice “soddisfacibile” e si scriveX |= c. Si suppone ovviamente che i connettivi logici ∧ e ∨, i quantificatoriesistenziali ∃· e le equazioni siano interpretati classicamente.

Si consideri l’algebra

Λ(Υst ,ΠC) =(C(Υst ,ΠC),∧,∨, true, false,∃X , t = t′

)X⊆Vars; t,t′∈TΩ(Vars)

ottenuta chiudendo l’algebra di vincoli Λ(Υst ,ΠC) della definizione 3.1.3 ri-spetto alla disgiunzione infinita e numerabile di formule in C(Υst ,ΠC). Λ(Υst ,ΠC)e detta “algebra libera dei vincoli su Υst e ΠC”. Siano

c1 =∨i∈I1

c′i e c2 =∨i∈I2

c′′i

due disgiunzioni possibilmente infinite di vincoli in Λ(Υst ,ΠC). La relazionedi equivalenza ≈X su Λ(Υst ,ΠC) definita da

c1 ≈X c2 ⇐⇒⋃i∈I1

ϑ | X |= c′i =⋃i∈I2

ϑ | X |= c′′i ,

e una relazione di congruenza su Λ(Υst ,ΠC). L’algebra quoziente

Ast = Λ(Υst ,ΠC)/≈X

e banalmente un sistema di vincoli distributivo, ed e chiamato “sistema divincoli standard”.

3.1.3 Correlazione dei sistemi di vincoli: correttezza

Un sistema di vincoli e, in generale, un’intepretazione (su un semianellochiuso) per le formule di vincoli. Per mettere i sistemi di vincoli in relazione

33

l’uno con l’altro si puo seguire l’approccio della “correttezza di semanticastatica” in [6]. La correttezza delle definizioni semantiche non standard puoessere trattata in modo algebrico per mezzo della nozione di morfismo [56].Questa nozione puo comunque essere resa meno restrittiva assumendo chegli insiemi base (carriers) delle algebre implicate siano insiemi parzialmenteordinati. Introduciamo dunque una nozione di morfismo debole che cattural’approssimazione possibilmente indotta dalle interpretazioni astratte o, piuin generale, dalle semantiche approssimate definite nello schema algebrico.

Definizione 3.1.9 Siano A e B due Σ-algebre con Σ = (S,Op), e, per ognisorta s ∈ S, sia (Bs,Bs) un poset. Un “morfismo debole” h:A

w→ B e unafamiglia di funzioni

hs:As → Bs, ∀s ∈ S,

tale che, per ogni s ∈ S e per ogni simbolo di costante f :→ s in Op

hs(fA) Bs fB,

e, per ogni simbolo di operazione f : s1 · · · sm → s in Op, per ogni ei ∈ Asicon i ∈ 1, . . . ,m,

hs(fA(e1, . . . , em)) Bs fB(hs1(e1), . . . , hsm(em)).

Dato un sistema di vincoli con universo C e operatore di disgiunzione “⊕”,la definizione 3.1.6 e la proposizione 3.1.1 implicano che (C,v⊕) e un poset,dove “v⊕” e l’ordinamento parziale indotto da “⊕”. Dunque ha senso parlaredi morfismi deboli tra sistemi di vincoli. Vediamo ora a quali condizioni.Innanzitutto perche possa esistere un morfismo debole tra due sistemi divincoli A e A′ occorre che A e A′ siano compatibili . Cio accade se A e nonditributivo oppure se sia A che A′ sono distributivi. In caso contrario, comesi vedra nel capitolo 5, occorre ricorrere a una diversa nozione di correttezzadi A′ rispetto ad A.

Un morfismo tra i sistemi di termini Υ = (Υ, S, V ) e Υ′ = (Υ′, S ′, V ′) euna funzione κ: Υ→ Υ′ tale che, ∀t1, t2 ∈ Υ e ∀x ∈ V ,

κ(sx(t1, t2)) = s′κ(x)(κ(t1), κ(t2)).

Ora, seA = (C,⊗,⊕, 1, 0,∃∆, dt1,t2)∆⊆V ; t1,t2∈Υ

eA′ =

(C ′,⊗′,⊕′, 1′, 0′,∃′∆, d′t1,t2

)∆⊆V ′; t1,t2∈Υ′

34

sono sistemi di vincoli compatibili, allora esiste un morfismo debole α:A w→A′ se e solo se esiste un morfismo tra sistemi di termini κ: Υ→ Υ′ e valgonole seguenti condizioni, ∀c, c1, c2 ∈ C, ∀∆ ⊆ V e ∀t1, t2 ∈ Υ:

α(0) = 0′,

α(1) v⊕′ 1′,

α(c1 ⊕ c2) v⊕′ α(c1)⊕′ α(c2),

α(c1 ⊗ c2) v⊕′ α(c1)⊗′ α(c2),

α(∃∆c) v⊕′ ∃′κ(∆)α(c),

α(dt1,t2) v⊕′ d′κ(t1),κ(t2).

Un morfismo debole tra sistemi di vincoli sara talvolta denotato dalla coppia〈α, κ〉.

Definizione 3.1.10 Dato un sistema di vincoli A sull’universo C, un siste-ma di vincoli A′ sull’universo C ′ e compatibile con A′ e “corretto” rispettoad A se e soltanto se esiste un morfismo debole αc:A

w→ A′ che sia unafunzione suriettiva e monotona tra i poset (C,v⊕) e (C ′,v⊕′), ovvero deveessere αc(C) = C ′ e, ∀c1, c2 ∈ C,

c1 v⊕ c2 ⇒ αc(c1) v⊕′ αc(c2).

Si osservi che αc, essendo monotono, si comporta come un morfismoalgebrico rispetto all’operatore “⊕”, cioe risulta, ∀c1, c2 ∈ C,

αc(c1 ⊕ c2) = αc(c1)⊕′ αc(c2).

Inoltre, la composizione di due morfismi deboli monotoni e ancora un mor-fismo debole e monotono e, dal momento che αc e un ⊕-morfismo di semia-nelli chiusi, ovvero e un join-morfismo di reticoli completi, αc e una funzionecontinua di (C,v⊕) in (C ′,v⊕′) [7].

Proposizione 3.1.4 Siano A e A′ due sistemi di vincoli con universi, ri-spettivamente, C e C ′. Se αc:A

w→ A′ e un morfismo debole monotono esuriettivo, allora la funzione γc: C ′ → C, definita ∀c′ ∈ C ′ da [15]

γc(c′) =

⊕ c ∈ C | αc(c) v⊕′ c′

e tale che 〈αc, γc〉 e un’inserzione di Galois di (C ′,v⊕′) in (C,v⊕).

35

3.2 Semantica generalizzata

Definiamo ora, nella maniera usuale, i programmi logici con vincoli genera-lizzati. Sia A un sistema di vincoli sul sistema di termini Υ e sia ΠP uninsieme di simboli di predicato tale che

ΠP =⋃n∈N

ΠnP ,

dove ΠnP e l’insieme dei simboli di predicato in ΠP di arieta n. Analoga-

mente a quanto visto nella definizione 3.1.3 un (Υ,ΠP )-atomo e un elementodell’insieme

π(t1, . . . , tn) | π ∈ ΠnP , t1, . . . , tn ∈ Υ .

Una A-clausola e una formula del tipo

H :− c B1, . . . , Bn

con n ≥ 0 e dove H, la testa, e B1, . . . , Bn, il corpo, sono (Υ,ΠP )-atomi, ce un A-vincolo, “:−” e “,” denotano, rispettivamente l’implicazione logicae la congiunzione. Se il corpo e vuoto (n = 0), la clausola e detta clausolaunitaria. Un A-goal e un formula del tipo

c B1, . . . , Bn,

dove c e un A-vincolo e ogni Bi e un (Υ,ΠP )-atomo. Un programma logicocon vincoli (generalizzato), o A-programma, e un insieme finito di definizionidi predicato, ognuna delle quali consiste di un insieme finito di clausole.

La caratterizzazione algebrica che abbiamo introdotto nella prima partedi questo capitolo viene qui applicata al fine di ottenere una struttura ingrado di supportare ogni definizione semantica per la programmazione logicacon vincoli. Il meccanismo introdotto in [24] per modellare le sostituzioni dirisposta calcolata viene generalizzato al paradigma CLP costruendo la basedelle interpretazioni come un insieme di atomi vincolati [26].

Definizione 3.2.1 Siano A un sistema di vincoli e ΠP un insieme di simbolidi predicato. Un “atomo vincolato” (su A e ΠP ) e un oggetto della forma

p(x1, . . . , xn) :− c

dove c e un A-vincolo e p(x1, . . . , xn) e un (Υ,ΠP )-atomo.

Ogni atomo vincolato p(x) :− c rappresenta l’insieme delle istanze p(x)ϑ,dove ϑ e una soluzione del vincolo c.

36

Definizione 3.2.2 Siano A un sistema di vincoli, ΠP un insieme di simbolidi predicato e C il corrispondente insieme di atomi vincolati. E definita larelazione su C tale che

p(x1) :− c1 p(x2) :− c2

se e soltanto se esiste una tupla di variabili (di ridenominazione) x′ tale chex′ 6= x1, x′ 6= x2 e

∃x1(dx′,x1 ⊗ c1) v⊕ ∃x2(dx′,x2 ⊗ c2).

Proposizione 3.2.1 e una relazione di ordinamento parziale su C.

La relazione di equivalenza indotta dall’ordinamento parziale e deno-tata con ≈C.

Definizione 3.2.3 La “A-base delle interpretazioni” e B = C/≈C.

Definizione 3.2.4 I ⊆ ℘(B) e la collezione degli insiemi di atomi vincolatiI tali che

I ∈ I ⇐⇒ I ] ∅ = ∅ ] I = I,

dove ]:℘(B)× ℘(B)→ ℘(B) e dato da:

λI1, I2 .

p(x) :−

⊕j

∃xj(dx,xj ⊗ cj)∣∣∣∣ p(xj) :− cj ∈ I1 ∪ I2

∀j, x 6= xj

.

Definizione 3.2.5 Una “A-interpretazione” e un qualsiasi elemento di I.

Si osservi che dalle definizioni discende che ogni A-interpretazione con-tiene al piu un atomo vincolato p(x) :− c per ogni predicato p ∈ ΠP . Dalmomento che ogni programma logico con vincoli, e quindi ogniA-programma,e costituito da un insieme finito di clausole che definiscono un numero fini-to di predicati in ΠP , ogni A-interpretazione e un insieme finito di atomivincolati.

Sia p(x) :−⊕

j∈W cj ∈ I. Per ogni j ∈ W , cj rappresenta un insiemedi soluzioni ammissibili, ovvero calcolabili nel programma, per il predicato psulle variabili x. Siccome un predicato puo ammettere, in un programma, unnumero infinito di soluzioni ed essendo limitato, in generale, il potere espres-sivo del linguaggio dei vincoli, negli atomi vincolati devono necessariamenteessere consentiti join infiniti di vincoli. Questa possibilita e diretta conse-guenza della definizione 3.1.6 di sistema di vincoli e, in definitiva, dell’assiomaS4 della definizione 3.1.4 di semianello chiuso.

37

L’operatore binario “]” e fortemente correlato a “⊕” e si dimostra che larelazione v] su I definita, ∀I1, I2 ∈ I, da

I1 v] I2 ⇐⇒ I1 ] I2 = I2

e una relazione di ordinamento parziale. Inoltre, ricordando la proposizione3.1.3, si puo mostrare che vale il seguente risultato.

Proposizione 3.2.2 (I,v]) e un reticolo completo.

3.2.1 Semantica operazionale

In questa sezione presentiamo una caratterizzazione operazionale della se-mantica generalizzata di CLP.

Definizione 3.2.6 Sia A un sistema di vincoli, l’insieme dei goal su A edenotato con A-Goals. Sia inoltre P un A-programma. Definiamo la rela-zione ;P⊆ A-Goals × A-Goals (un “passo di A-derivazione) come la piupiccola relazione tale che, dati GA, G

′A ∈ A-Goals, risulta GA ;P G′A se e

soltanto se

• GA = c0 p1(t1), . . . , pn(tn),

• esistono, in PA, n versioni ridenominate di clausole

pi(xi) :− ci Gi,

per i = 1, . . . , n,

• G′A = c0 ⊗ c1 ⊗ · · · ⊗ cn G1, . . . , Gn, dove, per ogni i = 1, . . . , n,ci = dxi,ti ⊗ ci.

Una A-derivazione da un A-goal GA e una successione finita o infinita diA-goal tale che ogni elemento nella successione e ottenuto da quello che loprecede per mezzo di un singolo passo di A-derivazione. Una derivazione consuccesso e una A-derivazione finita il cui ultimo elemento ha il corpo vuoto,ovvero non contiene atomi ma soltanto un vincolo. La semantica operazionalepuo quindi essere definita in termini delle derivazioni (computazioni) consuccesso specificate dalla chiusura transitiva ;∗

P della relazione ;P .

Definizione 3.2.7 Siano A un sistema di vincoli e P un A-programma. La“semantica operazionale di P su A” e l’insieme

OA(P ) =p(x) :−

⊕ ∃(c)vars(x) | 1 p(x) ;∗

P c | p ∈ ΠP

,

dove si assume che⊕∅ = 0.

38

La semantica operazionale goal-dipendente e definita in termini di unafunzione G che associa ad ogni A-goal il corrispondente vincolo di rispostacalcolata.

Definizione 3.2.8 La funzione G:A-Goals → C e definita per ogni A-goalGA e risulta

G(GA) =⊕ ∃(c)vars(GA) | GA ;∗

P c .

Il seguente teorema mostra come la semantica definita in questa sezionecaratterizzi compiutamente il comportamento operazionale dei programmi.

Teorema 3.2.1 Siano P un programma e GA = c0 p1(t1), . . . , pn(tn) ungoal. Allora si ha G(GA) = c se e soltanto se, ∀i = 1, . . . , n,

pi(xi) :− ci ∈ OA(P )

ec = ∃(c0 ⊗ dx1,t1 ⊗ ci ⊗ · · · ⊗ dxn,tn ⊗ cn)vars(GA).

3.2.2 Semantica di punto fisso

In questa sezione definiamo una semantica di punto fisso che, nel caso disistemi di vincoli distributivi, e mostrata essere equivalente alla semanticaoperazionale.

Definizione 3.2.9 Siano A un sistema di vincoli e P un A-programma,ovvero un insieme finito di A clausole. E definita la funzione TAP : I→ I taleche, ∀I ∈ I,

TAP (I) =⊎

C∈PA

p(x) :− ∃(c)vars(x)

∣∣∣∣∣∣∣∣∣∣C = p(t) :− c p1(t1), . . . , pn(tn);∀i = 1, . . . , n :

pi(xi) :− ci ∈ I, c′i = dxi,ti ⊗ ci;c = dx,t ⊗ c⊗ c′1 ⊗ · · · ⊗ c′n;x ind C, c1, . . . , cn.

.

Teorema 3.2.2 Siano A un sistema di vincoli e P un A-programma, alloraTAP e una funzione monotona sul reticolo completo (I,v]).

Teorema 3.2.3 Siano A un sistema di vincoli distributivo e P un A-programma,allora TAP e una funzione continua sul reticolo completo delle A-interpretazioni(I,v]).

39

Sia f una funzione monotona su un reticolo completo L, allora, per unnoto risultato dovuto a Tarski, f ha un minimo punto fisso lfp(f). Se L haelemento minimo ⊥ e sup t ed f e anche continua, allora, posto, ∀i ∈ N,

f ↑ 0 = ⊥,f ↑ i = f(f ↑ (i− 1))

e f ↑ ω =⊔i<ω f

i(⊥), risulta lfp(f) = f ↑ ω. Si osservi che le proprieta dimonotonia e continuita di f si equivalgono nal caso in cui L non ammettacatene ascendenti infinite. Ne consegue, per il teorema 3.2.2, che la funzioneTAP puo essere continua anche se A e un sistema di vincoli non distributivo.Sfrutteremo questo fatto nella prossima sezione dedicata all’intepretazioneastratta.

Definizione 3.2.10 Siano A un sistema di vincoli e P un A-programma. Sela funzione TAP e continua, allora la “semantica di punto fisso di P rispettoad A” e l’insieme

FA(P ) = lfp(TAP ) = TAP ↑ ω.

Il seguente risultato stabilisce, per ogni sistema di vincoli distributivo,l’equivalenza tra la semantica operazionale e quella di punto fisso.

Teorema 3.2.4 Siano A un sistema di vincoli distributivo e P un A-programma,allora

FA(P ) = OA(P ).

La correttezza di una semantica non standard rispetto ad un’altra puoessere dimostrata imponendo certe condizioni sui rispettivi sistemi di vincoli.Siano A e A′ due sistemi di vincoli compatibili, e sia A′ corretto rispetto adA per mezzo del morfismo debole 〈α, κ〉. Sia poi P = C1, . . . , Cm un A-programma. Il programma corrispondente, P ′, sul sistema di vincoli A′ e uninsieme di clausole C ′1, . . . , C ′m tale che, ∀i = 1, . . . ,m, se

Ci = p(t) :− c p1(t1), . . . , pn(tn),

alloraC ′, i = p(κ(t)) :− α(c) p1(κ(t1)), . . . , pn(κ(tn)),

dove κ e considerato esteso, in modo ovvio, alle tuple di termini.Il seguente teorema correla la semantica di un programma con la seman-

tica del programma corrispondente definito su un sistema di vincoli correttorispetto a quello originario.

40

Teorema 3.2.5 Siano A un sistema di vincoli, P un A-programma e siaP ′ il programma corrispondente a P definito su A′. Supponiamo che A′ siacorretto rispetto ad A per mezzo del morfismo debole 〈αc, κ〉 e che I e I′ sianorispettivamente, gli insiemi delle A-interpretazioni e delle A′-intepretazioni.Allora la funzione α: I→ I′ definita, ∀I ∈ I, da

α(I) =p(κ(x)) :− αc(c)

∣∣∣ p(x) :− c ∈ I

e tale cheα(OA(P )) v]′ OA

′(P ′).

Inoltre, se TAP e TA′

P sono continue, si ha

α(FA(P )) v]′ FA′(P ′).

Nella sezione successiva introdurremo l’interpretazione astratta come unospeciale tipo di semantica non standard per i programmi CLP. La correttezzadell’approccio seguito discende dal teorema 3.2.5.

3.3 Interpretazione astratta di CLP

Un sistema di vincoli definisce un’interpretazione per le formule del linguag-gio dei vincoli. Questa struttura e sufficientemente generale per catturarele proprieta algebriche di svariate “tecniche” di costruzione dei vincoli: adesempio l’operatore di congiunzione “⊗” non e richiesto essere commutativo.Dal momento che, sia la semantica operazionale che quella di punto fisso sonodefinite sulla stessa struttura algebrica, ogni interpretazione generalizzata diun dato programma CLP puo essere vista come una valutazione non stan-dard del programma in un opportuno sistema di vincoli. Di conseguenza, ilprocesso di interpretazione dei programmi e parametrizzato rispetto ad uninsieme di operatori che modellano la “manipolazione dei dati” durante lacomputazione. Dunque i sistemi di vincoli, poiche riassumono in modo ade-guato l’essenza del processo interpretativo per diverse computazioni di tipoCLP (cioe basate sull’accumulazione di vincoli), rappresentano uno schemagenerale per lo sviluppo di strumenti di analisi data-flow .

La definizione di un sistema di vincoli astratto e suddivisa in due passi:astrazione dei termini e astrazione dei vincoli . Nel primo passo si definiscononuovi oggetti sintattici che rappresentino i termini concreti. Nel secondo sidefinisce l’astrazione dei vincoli sul sistema di termini astratto. Dal momentoche il reticolo completo delle interpretazioni e indotto dalla struttura del si-stema di vincoli, ogni interpretazione astratta corrispondera ad un’opportuna

41

definizione del sistema di vincoli associato alla particolare applicazione. Co-me abbiamo visto in precedenza la relazione tra i sistemi di vincoli concretoe astratto puo essere data per mezzo di un morfismo debole.

Se si considerano semantiche concrete di punto fisso, le analisi data-flowrichiedono, normalmente, il calcolo del limite di una catena ascendente (o diKleene) su un reticolo completo [13]. La terminazione di tali analisi e statatradizionalmente imposta richiedendo che tutte le catene ascendenti fosserofinite o, ed e lo stesso, che il reticolo fosse Noetheriano.

Definizione 3.3.1 Sia A un sistema di vincoli sull’universo C. Un insiemedi vincoli C ⊆ C e “limitato rispetto alle variabili libere” se e solo se esisteun insieme finito di variabili W tale che, ∀c ∈ C si ha FV (c) ⊆ W .

Definizione 3.3.2 Un sistema di vincoli A sull’universo C si dice “Noethe-riano” se e soltanto se non contiene catene infinite di vincoli limitati rispettoalle variabili.

Dato un sistema di vincoli Noetheriano A, si dimostra che il reticolocompleto (I,v]) e Noetheriano. Chiameremo “sistema di vincoli astratto”ogni sistema di vincoli Noetheriano, e denoteremo un qualsiasi sistema divincoli astratto con A].

L’interpretazione astratta dei programmi logici con vincoli corrispondealla definizione di un sistema di vincoli astratto e di una strategia di valuta-zione dei programmi. Il primo definisce la computazione astratta, mentre ilsecondo stabilisce quali tecniche sono usate per l’accumulazione delle infor-mazioni astratte. L’interpretazione astratta di tipo top-down corrisponde al-l’astrazione della semantica operazionale standard. Quella di tipo bottom-upconsente invece di calcolare approssimazioni finite della semantica di puntofisso associata ad un dato programma logico con vincoli. L’indipendenza dalgoal e una caratteristica positiva delle valutazioni bottom-up. L’analisi glo-bale dei programmi puo essere definita come una valutazione bottom-up suun opportuno sistema di vincoli astratto.

Definizione 3.3.3 Sia A un sistema di vincoli. Una “interpretazione astrat-ta corretta” per i vincoli di A e una coppia 〈A], αc〉, dove A] e un sistemadi vincoli astratto e αc:A

w→ A] e un morfismo debole e monotono.

L’esistenza di αc garantisce, per il teorema 3.2.5 la correttezza del pro-cesso di astrazione.

Dato un sistema di vincoli astratto A], il corrispondente operatore delleconseguenze immediate, TA

]

P e definito come nel caso concreto, ovvero se-condo la definizione 3.2.9, considerando gli operatori astratti anziche quelli

42

concreti. Dal momento che (I],v]]) e Noetheriano, per quanto visto nellaprecedente sezione, TA

]

P e continuo, sia o no A] distributivo.

Proposizione 3.3.1 Dato un sistema di vincoli astratto A] e un A]-pro-gramma P esiste un numero naturale k tale che

FA](P ) = TA]

P ↑ k.

Come nel caso della programmazione logica [5], la correttezza di un op-portuno insieme di operatori assicura la correttezza dell’intero schema diinterpretazione astratta (sia top-down che bottom-up). Nel caso della pro-grammazione logica con vincoli, la correttezza dell’analisi e ricondotta allacorrettezza del sistema di vincoli, come mostrato nel teorema 3.2.5.

L’insieme dei vincoli astratti puo essere specificato definendo un operatoredi chiusura superiore ρ su (C,v⊕). Come viene mostrato in [15] il processodi approssimazione consiste essenzialmente nel partizionamento dello spaziodei vincoli in modo che non sia fatta alcuna distinzione tra i vincoli conside-rati equivalenti, tutti approssimati da un rappresentante della loro classe diequivalenza. La relazione di equivalenza e indotta, appunto, da un operatoredi chiusura superiore ρ. Se c1 e c2 sono due vincoli, allora

c1 ≈ρ c2 ⇐⇒ ρ(c1) = ρ(c2).

Nel seguito introduciamo le proprieta fondamentali degli operatori dichiusura superiore sui sistemi di vincoli. Queste proprieta fanno sı che lastruttura algebrica costituita dagli elementi chiusi secondo ρ sia essa stessaun sistema di vincoli.

Definizione 3.3.4 Un “operatore di chiusura superiore”, o semplicemente“chiusura”, ρ su un sistema di vincoli A con universo C e una funzioneρ: C → C tale che, ∀c, c1, c2 ∈ C, ∀∆ ⊆ V , sono soddisfatte le seguenticondizioni:

R1 : c1 v⊕ c2 ⇒ ρ(c1) v⊕ ρ(c2), [monotonia]

R2 : c v⊕ ρ(c), [estensivita]

R3 : ρ(ρ(c)) = ρ(c), [idempotenza]

R4 : ρ(∃∆c) = ∃∆ρ(c) [compatibilita con ∃·]

R5 : ρ(c1)⊗ ρ(c2) = ρ(ρ(c1)⊗ c2) = ρ(c1 ⊗ ρ(c2)),

R6(a) : ρ(dt,t′) = ∃x(ρ(dt,x)⊗ ρ(dx,t′)), se x ind t, t′,

43

R6(b) : ρ(dz,[t/x]t′) = ∃x(ρ(dz,t′)⊗ ρ(dx,t)), se z 6= x e x ind t, z ind t′.[compatibilita con d·,·]

Si osservi che ogni operatore di chiusura superiore e un join-morfismoquasi-completo, ovvero ∀C ∈ C, risulta [15, 14, 61]

ρ(⊕c∈C

c)

= ρ(⊕c∈C

ρ(c)).

Naturalmente questa proprieta continua a valere anche per le chiusure suisistemi di vincoli.

Esempio 3.3.1 Si dimostra che le cilindrificazioni sono operatori monoto-ni, mentre l’idempotenza e l’estensivita sono specificate, rispettivamente, da-gli assiomi C4 e C5 della definizione 3.1.6. La compatibilita con ∃· seguedall’assioma C4. Inoltre l’assioma R5 della definizione 3.3.4 corrisponde al-l’assioma C3 della definizione 3.1.6. Dunque, se ∃∆ e un operatore di ci-lindrificazione su un sistema di vincoli A, allora e un operatore di chiusurasuperiore su A.

Consideriamo la definizione 3.3.4. Gli assiomi da R1 a R3 specificano leproprieta standard degli operatori di chiusura superiore [14, 15, 61]. La com-patibilita di un operatore di chiusura superiore con le cilindrificazioni (R4)assicura che la composizione di ∃· e ρ e ancora una chiusura (una risulta-to classico di teoria delle chiusure e che la composizione di due chiusure eun chiusura se e solo se le due chiusure originarie commutano [49]). L’ulti-ma proprieta consente di definire l’operatore di congiunzione sugli elementichiusi.

Teorema 3.3.1 Sia ρ un operatore di chiusura superiore sul sistema di vin-coli

A = (C,⊗,⊕, 1, 0,∃∆, dt1,t2)∆⊆V ; t1,t2∈ Term.

La struttura algebrica

ρ(A) = (ρ(C),⊗, ⊕, 1, ρ(0),∃∆, ρ(dt1,t2))∆⊆V ; t1,t2∈Υ,

dove

ρ(C) = c ∈ C | c = ρ(c) ,ρ(c1)⊕ρ(c2) = ρ(c1 ⊕ c2),

e un sistema di vincoli.

44

Proposizione 3.3.2 Sia ρ un operatore di chiusura superiore su un sistemadi vincoli A, allora ρ e un morfismo debole di A in ρ(A).

In [15] sono presentati diversi metodi equivalenti per la specifica dei do-mini astratti (tra i quali gli operatori di chiusura superiore). Inoltre vi sonotecniche standard di specifica algebrica che permettono di definire sistemidi vincoli astratti. Ad esempio, le cilindrificazioni possono essere interpre-tate come astrazioni sull’algebra dei vincoli. Come e mostrato nell’esempio3.3.1, la chiusura per mezzo della quantificazione esistenziale e un metodo perdefinire domini astratti. Uno spazio di vincoli approssimati A] puo anche es-sere specificato aggiungendo ulteriori assiomi al sistema di vincoli A. Questiassiomi addizionali estendono il significato degli elementi diagonali dt,t′ del-l’algebra, specificando quali oggetti devono essere considerati “equivalenti”dal punto di vista dell’analisi.

I matematici sono come i Francesi:quando gli dici qualcosa

essi lo traducono nel loro linguaggio,

e, d’un tratto, e qualcosa di completamente diverso.

— GOETHE, in Massime e Riflessioni (1829)

45

Capitolo 4

Il linguaggio CLP(FD)

In questo capitolo descriviamo brevemente il linguaggio CLP(FD), per ilquale svilupperemo, nel seguito, una tecnica di analisi statica mediante in-terpretazione astratta.

4.1 Motivazioni

Molti problemi reali possono essere convenientemente descritti come proble-mi di soddisfacimento di vincoli . Questa classe di problemi e importante indiverse aree dell’informatica quali la ricerca operativa, e l’intelligenza artifi-ciale (AI). Un problema di soddisfacimento di vincoli consiste essenzialmentedi un insieme di variabili X1, . . ., Xn e di un certo numero vincoli che im-pongono limitazioni ai valori che le variabili possono assumere. Risolvere unproblema in questa classe significa trovare un assegnamento (o piu d’uno) divalori alle variabili, tale che tutti i vincoli siano simultaneamente soddisfatti.

Una sottoclasse di particolare importanza e quella dei problemi di soddi-sfacimento di vincoli su domini finiti (CSP). La caratteristica essenziale diquesta classe e che i valori che ogni variabile puo assumere sono finiti. Piuformalmente un CSP e definito da un insieme

V = X1, . . . , Xn

di variabili che assumono valori, rispettivamente, sugli insieme finiti

D1, . . . , Dn

e da un insieme di vincoli C. Un vincolo

c(Xi1 , . . . , Xik)

46

tra k variabili in V e un sottoinsieme del prodotto cartesiano

Di1 × · · · ×Dik

che specifica quali valori delle variabili coinvolte siano compatibili tra loro.Naturalmente questo sottoinsieme non deve necessariamente essere dato inmodo esplicito ma puo essere definito da equazioni o disuguaglianze. Lasoluzione di un CSP e definita, come nella classe generale, da un assegna-mente di valori a tutte le variabili in modo che tutti i vincoli siano soddisfatti[45, 40, 46]. Cio che rende interessanti i CSP su domini finiti e che, oltre adessere un formalismo sufficientemente espressivo [57], sono teoricamente de-cidibili . E cioe possibile esibire un algoritmo che, dato in CSP, o ne fornisceuna soluzione o, in tempo finito, ne certifica l’insolubilita. Il vero problema etrovare algoritmi efficienti che risolvano problemi in questa classe. Natural-mente, poiche il problema della soddisfattibilita booleana e esprimibile comeCSP sul dominio 0, 1 ed e NP-completo, un algoritmo generale progetta-to per risolvere l’intera classe dei CSP su domini finiti non puo che averecomplessita asintotica nel caso peggiore esponenziale.

Lo schema CLP ha piu di un’attrattiva per la specifica dei problemi disoddisfacimento di vincoli. In particolare lo schema consente naturalmentedi formulare i CSP in modo dichiarativo (per l’esplicita presenza dei vincolinel linguaggio e per la forma relazionale dei predicati) e strutturato (con lanozione di clausola).

4.2 Definizione del linguaggio

Il linguaggio CLP(FD) e definito su particolari domini finiti, e cioe i sot-toinsiemi finiti degli interi. In modo informale possiamo darne la seguentecaratterizzazione sintattica “concreta”:

• un termine e una qualunque espressione costruita a partire dai simbolidi costante e dalle variabili per mezzo degli operatore binari “+”, “−”e “∗”;

• un vincolo e un costrutto del tipo e1 ./ e2, dove e1 ed e2 sono terminie ./ e un simbolo di relazione aritmetica in =, 6=,≤, <,≥, >;

• il dominio di ogni variabile e specificato da un costrutto del tipo

domain(X, d),

dove X e una variabile e d e (denota) un sottoinsieme finito di simbolidi costante.

47

Un esempio di programma CLP(FD), dove si e scelta la notazione degliintervalli chiusi per specificare i domini, e il sequente:

mc(N,M) :− domain(N, [0, 200]), domain(M, [0, 200]),

N > 100, M = N − 10.

mc(N,M) :− domain(N, [0, 200]), domain(M, [0, 200]),

N ≤ 100, T = N + 11 mc(T, U), mc(U,M).

Definizione 4.2.1 Il linguaggio CLP(FD) e definito sul linguaggio “one-sorted” del primo ordine indotto dalla seguente “segnatura”:

sort S :D

opns Ω :ηi : → D+ : DD → D− : DD → D∗ : DD → D

pred ΠC := : DD6= : DD≤ : DD< : DD≥ : DD> : DD

pred ΠP :πk : ak ∀k ∈ Kπ

P , ak ∈ D∗f

Abbiamo dunque la sorta D delle espressioni su domini numerici finiti,il relativo insieme dei simboli di costante e di operazione Ω e gli insiemi disimboli di predicato ΠC e ΠP . ΠC contiene gli usuali simboli di relazionearitmetica, mentre ΠP contiene i simboli di predicato definiti nei programmi.Ovviamente ΠP e parametrizzato rispetto al programma P , poiche i πk sonoi simboli di predicato per i predicati definiti in P come insiemi di clausole.

L’insieme delle variabili Vars e definito come nella sezione 2.5, con ladifferenza che ad ogni simbolo di variabile e associato un insieme di simbolidi costante (il dominio). Se X ∈ Vars il dominio (sintattico) di X e denotatocon d(X). In realta si puo pensare al simbolo di variabile X come ad unacoppia 〈X, d(X)〉. Denoteremo con TΩ(Vars) l’insieme dei termini su Ω eVars .

48

Definizione 4.2.2 Una FD-sostituzione e un insieme finito della forma

[e1/X1], . . . , [en/Xn],

dove, per ogni i = 1, . . . , n, le Xi sono variabili tutte distinte e ei e un terminedistinto da Xi tale che ei e una costante c ∈ Xi oppure e una variabile Yicon d(Yi) ⊂ d(Xi).

La composizione delle FD-sostituzioni si definisce l’operazione di compo-sizione in modo classico, e si dimostrano i risultati standard quali l’associa-tivita della composizione e dell’applicazione di sostituzioni [39, 57]. Sia Subl’insieme delle FD-sostituzioni idempotenti. L’algebra

Υst = (TΩ(Vars), Sub,Vars)

e banalmente un sistema di termini finitario.Per quanto riguarda la definizione semantica del linguaggio, dato un

programma P , la struttura FD di interpretazione dei vincoli consiste

• dell’insieme Z (il dominio della computazione);

• dell’assegnamente ai simboli di costante dei relativi elementi di Z, e,conseguentemente, dell’assegnamento ad ogni variabileX di un dominiodX ⊆f Z;

• dell’assegnamento ai simboli di operatore “+”, “−” e “∗” delle normalioperazioni su Z;

• dell’assegnamento ai simboli di relazione “=”, “6=”, “≤”, “<”, “≥” e“>” delle corrispondenti relazioni su Z.

Definizione 4.2.3 Una FD-valutazione e una funzione finitaria θ: Vars →Z tale che ∀X ∈ Vars, X ∈ dom(θ)⇒ θ(X) ∈ dX .

Le nozioni di soluzione e di soddisfacibilita sono definite come nella se-zione 2.5. Nel prossimo capitolo denoteremo con Θ l’insieme di tutte leFD-valutazioni e con Sol(c) l’insieme

θ ∈ Θ | FD |= cθ .

49

Interfaccia

Motore Inferenziale

'

&

$

%• ricerca di clausole

Risolutore di Vincoli

'

&

$

%• test di soddisfacibilita dei vincoli

?

6

Figura 4.1: Struttura di un sistema CLP

4.3 Risoluzione di vincoli

La struttura generale di un sistema CLP riflette il suo obiettivo: l’integrazio-ne tra programmazione logica e risoluzione di vincoli. La figura 4.1 mostral’organizzazione interna di un tipico sistema CLP. Essenzialmente vi si pos-sono distinguere due componenti: un motore inferenziale per la parte logica eun risolutore di vincoli incrementale che puo essere considerato una procedu-ra di decisione per una classe di vincoli. I due moduli comunicano attraversoun’interfaccia. Il motore inferenziale gestisce la ricerca e l’invocazione delleclausole, riconosce i vincoli e li passa al risolutore. Quest’ultimo accumulai vincoli, ne controlla la soddisfacibilita e riporta i risultati al motore infe-renziale. Nel caso in cui il vincolo accumulato sia insoddisfacibile, il motoreinferenziale deve cercare clausole alternative (backtracking), mentre il risolu-tore di vincoli deve eliminare, dalle sue strutture dati, ogni traccia dei vincoliche gli siano stati passati dal momento in cui e stata effettuata l’ultima scelta.

Nel caso specifico di CLP(FD), come abbiamo gia osservato, la procedu-ra generale di controllo della soddisfacibilita non puo che avere complessitaesponenziale. Cio significa che il risolutore dovra includere una fase di ricer-ca. Dovra cioe ”fare delle scelte” per i valori della variabili, verificandone poila consistenza. La tecnica piu usata per implementare questa fase e quella

50

della ricerca con backtracking1. Le variabili vengono cioe istanziate sui ri-spettivi domini, una per volta in un certo ordine. Quando non e possibileistanziare la variabile corrente in modo consistente con i vincoli, si sceglie unaltro valore per la variabile istanziata piu recentemente. Questa tecnica puoessere molto inefficiente, principalmente per i seguenti motivi:

• i fallimenti vengono riconosciuti in ritardo rispetto alla scelta che li haoriginati;

• le stesse soluzioni parziali vengono “riscoperte” piu volte;

• vengono generati nodi inutili nell’albero di ricerca.

Per rimediare a questa inefficienza si puo ricorrere agli algoritmi di consisten-za locale. Questi algoritmi prendono in considerazione un piccolo gruppo divariabili, con i vincoli che le legano, ed eliminano, una volta per sempre, leinconsistenze locali che non possono contribuire ad alcuna soluzione. Que-ste inconsistenze sarebbero state ripetutamente scoperte in ogni soluzioneottenuta con la sola tecnica di backtracking. Un ruolo degli algoritmi diconsistenza e dunque quello di realizzare una fase di pre-elaborazione primadi procedere alla fase di ricerca con backtracking. Esempi di algoritmi diconsistenza locale sono quelli noti sotto il nome di arc-consistency [40] (chelavora su due variabili per volta), path-consistency [45] (tre variabili per vol-ta) e k-consistency [25] (k variabili per volta). Nel caso di CLP(FD) unatecnica di consistenza locale, piu complessa di quelle citate, che permette dirisolvere completamente i CSP via via accumulati dal risolutore di vincoli equella detta di rilassamento perfetto [46].

Quello che ci interessa osservare qui, e il fatto che, quale che sia la tecnicaimpiegata dal risolutore di vincoli, la sua efficienza dipende strettamente dallecardinalita iniziali dei domini delle variabili. Tanto piu saranno piccoli questidomini, tanto piu potra essere efficiente il controllo della soddisfacibilita diun insieme di vincoli.

1Non bisogna confondere il backtracking del motore inferenziale con quello interno alrisolutore di vincoli.

51

Capitolo 5

Interpretazioni basate sullebounding box

In questo capitolo viene definita un’interpretazione astratta mirata ad ot-tenere approssimazioni quantitative dell’insieme di successo dei predicati inCLP(FD). L’idea e la seguente: sia p/n un predicato di un qualche pro-gramma P in CLP(FD). La semantica model-theoretic di P conterra l’atomovincolato p(X1, . . . Xn) :− c, l’insieme delle soluzioni di c definisce un insiemedi punti in uno spazio n-dimensionale. Questi punti saranno disposti nellospazio in qualche modo, secondo una certa forma: la semantica standard cidice quale. Nella semantica astratta cerchiamo un’approssimazione spazialedi questo insieme di punti. Intuitivamente un’approssimazione spaziale deveavere due caratteristiche. In primo luogo l’approssimazione di un oggetto nel-lo spazio e una figura geometrica che racchiude, circoscrive l’oggetto stesso.Inoltre ogni oggetto nello spazio deve possedere un’approssimazione minima.

Esempi di approssimazioni spaziali sono il minimo politopo convesso circo-scritto, la copertura minima costruita su una griglia regolare, le approssima-zioni ordine-Z [30] in cui una regione spaziale viene approssimata medianteun insieme di segmenti di una curva che riempie lo spazio (ad esempio lacurva di Peano), ed infine le bounding box. Nelle figure 5.1 e 5.2 sono mo-strate le approssimazioni spaziali di un medesimo insieme di punti mediante,rispettivamente, politopi convessi e bounding box.

Una bounding box e una forma molto semplice di approssimazione spa-ziale. Le bounding box sono essenzialmente regioni rettangolari con i latiparalleli agli assi coordinati. Ovviamente questa semplicita rende le boun-ding box piuttosto imprecise rispetto ad altre approssimazioni, ma l’impre-cisione e largamente compensata dalla facilita con la quale le bounding boxpossono essere ricavate, manipolate e usate per dedurre informazioni utilisulla regione spaziale approssimata. Come vedremo nel seguito, una boun-

52

-

6

X

Y

0

ss s ss ss

PPPPPP

bb

bbb

bb

bbb

Figura 5.1: Approssimazione mediante politopi convessi

-

6

X

Y

0

ss s ss ss

Figura 5.2: Approssimazione mediante bounding box

53

ding box e descritta da un insieme di intervalli associati alle variabili, o, sesi preferisce, agli assi coordinati di uno spazio cartesiano. Una boundingbox n-dimensionale richiede percio, per la sua memorizzazione, 2n parole dimemoria: una per ogni estremo degli n intervalli che la caratterizzano. Ve-dremo anche come le operazioni di composizione delle bounding box sianoparticolarmente semplici.

5.1 Motivazioni

Quando si vogliano ricavare informazioni da un programma in un linguaggiodefinito su un dominio numerico e spesso necessario ricorrere ad approssi-mazioni quantitative. Ad esempio nel contesto di CLP(FD) un’analisi digroundness per le variabili deve in qualche modo approssimare le soluzionidei vincoli in modo da determinare quali variabili e in quali contesti di ese-cuzione siano forzate a poter assumere un solo valore. Nei casi in cui questovalore sia noto e fissato la variabile puo essere eliminata dal programma, congli ovvi vantaggi che ne conseguono.

Sempre nel contesto di CLP(FD) e importante, per quanto detto nellasezione 4.3, che i domini delle variabili siano quanto piu ristretti possibile.La memorizzazione dei domini e infatti costosa a causa del fatto che il ri-solutore di vincoli, nella sua componente di ricerca, puo dover salvare piuvolte il dominio di una variabile, per poterlo ripristinare, nel backtracking,in caso di fallimento. Inoltre, seppure la riduzione dei domini venga effettua-ta anche a tempo di esecuzione mediante tecniche di consistenza, e evidenteche la riduzione preventiva effettuata una volta sola a tempo di compilazionepuo essere particolarmente redditizia in termini di efficienza. Si consideri cheun’implementazione di CLP(FD), un linguaggio che vuole essere dichiara-tivo, non dovrebbe richiedere al programmatore di specificare, per ottenereun’esecuzione efficiente, i domini piu ristretti possibili. Questa operazionedeve invece essere effettuata dal compilatore per mezzo dell’analisi staticadel programma.

L’interpretazione approssimata presentata in questo capitolo si presta aquesti scopi. Naturalmente, data la loro semplicita, le bounding box sonopiuttosto imprecise, soprattuto in programmi in cui l’insieme delle soluzionidei predicati sia “sparso”, ovvero contenga punti molto distanti tra loro. Inogni caso il rimpiazzamento di un vincolo con una bounding box comportaun’ovvia perdita di informazione. Ad esempio, consideriamo la seguenteclausola CLP(FD):

p(X, Y ) :− domain(X, 1, 2, 3), domain(Y, 2, 3, 4), X = Y.

54

La bounding box che riusciremo a derivare per il predicato p conterra i punti(2, 2), (2, 3), (3, 2) e (3, 3). Questo consente di ridurre i domini delle variabiliX e Y , ma non consente piu di dedurre che, in ogni soluzione per p, risultaX = Y . Visto in termini geometrici intuitivi, un vincolo rappresenta un in-sieme di punti in un certo spazio n-dimensionale, mentre una bounding boxrappresenta una “scatola” che contiene questi punti. La perdita di informa-zione risiede nel considerare tutto il “volume” della scatola anziche i punticontenuti.

55

5.2 Intervalli

L’obiettivo di questa e della successiva sezione e quello di definire formal-mente le bounding box, che costituiranno la base per il sistema di vincoli chespecifica l’analisi alla quale siamo interessati. Iniziamo dunque con la defini-zione delle proiezioni delle bounding box sugli assi coordinati rappresentatidalle variabili: gli intervalli.

Definizione 5.2.1 Sia Z l’insieme degli interi. Un “boundary” e un ele-mento dell’insieme

Z = Z ∪ +∞,−∞.L’insieme dei boundary, Z, e totalmente ordinato rispetto alla relazioned’ordine ottenuta estendendo la corrispondente relazione su Z con gli elementi

z ≤Z +∞, ∀z ∈ Z;−∞ ≤Z z, ∀z ∈ Z.

Proposizione 5.2.1 Il poset (Z,≤Z) e completo.

Dim. Per la definizione di ≤Z , Z ha −∞ come elemento minimo. Sia oraS ⊆ Z e S 6= ∅, essendo Z totalmente ordinato rispetto a ≤Z , vi sono duecasi: o ∃u ∈ S tale che ∀s ∈ S risulta s ≤Z u e in tal caso supZ(S) = u,oppure, essendo Z discreto, supZ(S) = +∞. Tanto basta per concludere cheZ e completo.

Definizione 5.2.2 L’algebra dei boundary, Z, e cosı definita:

Z = (Z,min,max,+∞,−∞)

dove, ∀x, y ∈ Z,

min(x, y) =

x se x ≤Z y,y se y ≤Z x;

max(x, y) =

x se y ≤Z x,y se x ≤Z y.

Proposizione 5.2.2 Z e un reticolo limitato e completo.

Dim. Infatti risulta, ∀z1, z2 ∈ Z,

min(z1, z2) = infZz1, z2,max(z1, z2) = supZz1, z2.

56

Per la proposizione 5.2.1 (Z,min,max) e un reticolo completo e dunquelimitato, con annichilatori +∞ e −∞, poiche valgono ∀z ∈ Z,

min(z,−∞) = −∞,max(z,+∞) = +∞.

A questo punto si definiscono gli intervalli come particolari coppie diboundary. Intuitivamente cio che si vuole caratterizzare sono gli intervallifiniti (in cui entrambi i boundary sono interi), gli intervalli superiormente edinferiormente illimitati, l’intervallo illimitato ovunque e l’intervallo vuoto.

Definizione 5.2.3 Un “intervallo” e un elemento dell’insieme

I = (zl, zh) | zl, zh ∈ Z, zl ≤Z zh \ (+∞,+∞), (−∞,−∞)∪(+∞,−∞).

Sugli intervalli e definita la relazione ≤I tale che, ∀(xl, xh), (yl, yh) ∈ I:

((xl, xh) ≤I (yl, yh)) ⇐⇒ ((yl ≤Z xl) ∧ (xh ≤Z yh)).

Nel seguito si utilizzeranno i pedici l e h come selettori, ovvero per ognix ∈ I e inteso che x = (xl, xh). Intuitivamente, dati due intervalli x e y siha x ≤I y se e solo se x e contenuto in y.

Proposizione 5.2.3 ≤I e una relazione di ordinamento parziale su I.

Dim. Infatti, ∀x, y, z ∈ I si ha x ≤I x poiche

(xl ≤Z xl) ∧ (xh ≤Z xh);

se x ≤I y e y ≤I x, allora x = y dal momento che

((yl ≤Z xl) ∧ (xh ≤Z yh))((xl ≤Z yl) ∧ (yh ≤Z xh))

⇒ ((xl = yl) ∧ (xh = yh));

infine, poiche

((yl ≤Z xl) ∧ (xh ≤Z yh))((zl ≤Z yl) ∧ (yh ≤Z zh))

⇒ ((zl ≤Z xl) ∧ (xh ≤Z zh)),

risulta che, se x ≤I y e y ≤I z, allora x ≤I z.

57

Proposizione 5.2.4 Il poset (I,≤I) e completo.

Dim. Si osservi innanzitutto che (+∞,−∞) e l’elemento minimo di I.Infatti, ∀x ∈ I, poiche risulta xl ≤Z +∞ e −∞ ≤Z xh, si ha (+∞,−∞) ≤Ix. Resta da mostrare l’esistenza di supI per ogni sottoinsieme non vuoto diI. Sia dunque S ⊆ I e S 6= ∅, e sia

w = (infZxl | (xl, xh) ∈ S , supZxh | (xl, xh) ∈ S ).

w esiste poiche Z e stato mostrato essere un reticolo completo. Inoltre, seS = (+∞,−∞) allora w = (+∞,−∞) ∈ I. Altrimenti risulta wl ≤Z whe dunque w ∈ I. Dalle definizioni di w e ≤I discende immediatamente che∀x ∈ S si ha x ≤I w e che per ogni altro maggiorante w′ risulta w ≤I w′.Ne consegue che w = supI(S).

Definiamo ora l’algebra degli intervalli, che risultera, per quanto abbiamoappena mostrato, essere un reticolo completo, esplicitando gli operatori dicomposizione. Intuitivamente il meet dell’algebra e la normale intersezione,mentre il join e l’unione convessa.

Definizione 5.2.4 L’algebra degli intervalli, I, e cosı definita:

I = (I,⊗I ,⊕I ,>I ,⊥I)

dove

>I = (−∞,+∞),

⊥I = (+∞,−∞);

e, ∀x, y ∈ I,

x⊗I y =

⊥I se max(xl, yl) > min(xh, yh),(max(xl, yl),min(xh, yh)) altrimenti;

x⊕I y = (min(xl, yl),max(xh, yh)).

Proposizione 5.2.5 I e un reticolo limitato e completo.

Dim. Nella dimostrazione della proposizione 5.2.4 si e gia visto che, ∀x, y ∈I,

x⊕I y = supIx, y,

mostriamo ora che si ha

x⊗I y = infIx, y.

58

Sia allora

z = x⊗I y =

⊥I se max(xl, yl) > min(xh, yh),(max(xl, yl),min(xh, yh)) altrimenti;

per definizione z ∈ I. Se z = (+∞,−∞), allora, essendo

xl ≤Z +∞, −∞ ≤Z xh,yl ≤Z +∞, −∞ ≤Z yh,

si ha che z ≤I x e z ≤I y. Se invece z 6= (+∞,−∞) si giunge alla stessaconclusione notando che

xl ≤Z max(xl, yl), min(xh, yh) ≤Z xh,yl ≤Z max(xl, yl), min(xh, yh) ≤Z yh.

Sia ora z′ un qualsiasi minorante di x e y. Se z′ = (+∞,−∞), allora z′ ≤I z.Altrimenti, essendo

max(xl, yl) ≤Z z′l,

z′h ≤Z min(xh, yh),

z non puo essere (+∞,−∞) e si ha ancora z′ ≤I z.In definitiva z = infIx, y,e, per la proposizione 5.2.4, I e un reticolo completo. Cio implica che e limi-tato e gli annichilatori sono >I e ⊥I . Valgono infatti, banalmente, ∀x ∈ I,le uguaglianze x⊗I ⊥I = ⊥I e x⊕I >I = >I .

Nota 5.2.1 Il reticolo degli intervalli non e distributivo, infatti:

(5, 8)⊗I ((1, 3)⊕I (9, 12)) = (5, 8)⊗I (1, 12) = (5, 8),

ma((5, 8)⊗I (1, 3))⊕I ((5, 8)⊗I (9, 12)) = ⊥I ⊕I ⊥I = ⊥I .

Gli intervalli sono stati introdotti per astrarre (o, meglio, approssimare)i sottoinsiemi degli interi, e cioe i domini e gli insiemi di valutazioni delle va-riabli in CLP(FD). Vediamo ora le funzioni di astrazione e concretizzazioneche mettono in relazione i reticoli completi (I,≤I) e (℘(Z),⊆).

Definizione 5.2.5 Siano αI :℘(Z) → I e γI : I → ℘(Z) le funzioni cosıdefinite, ∀S ⊆ Z e ∀x ∈ I:

αI(S) = (infZ(S), supZ(S)),

γI(x) = z ∈ Z | xl ≤Z z ≤ xh .

Si osservi che dalla definizione discendono:

αI(∅) = ⊥I ,γI(⊥I) = ∅.

59

Verifichiamo ora che le funzioni di astrazione e concretizzazione sono cor-rette, ovvero soddisfano le proprieta delle inserzioni di Galois riguardanti lastruttura geometrica (basata sugli ordinamenti) dei domini.

Proposizione 5.2.6 La coppia di funzioni 〈αI , γI〉 e un’inserzione di Galoisdi (I,≤I) in (℘(Z),⊆).

Dim. Occorre mostrare che le funzioni αI e γI sono monotone, ovvero che,∀S, T ∈ ℘(Z) e ∀x, y ∈ I:

S ⊆ T ⇒ αI(S) ≤I αI(T ),

x ≤I y ⇒ γI(x) ⊆ γI(y);

inoltre deve essere, ∀S ∈ ℘(Z) e ∀x ∈ I:

S ⊆ γI(αI(S)),

x = αI(γI(x)).

Per la monotonia di αI , siano S, T ∈ ℘(Z) tali che S ⊆ T , allora valgono

infZ(T ) ≤Z infZ(S),

supZ(S) ≤Z supZ(T ),

ovveroαI(S) ≤I αI(T ).

Per la monotonia di γI , siano x, y ∈ I tali che x ≤I y, risulta

yl ≤Z xl,

xh ≤Z yh,

e dunque

γI(x) = z ∈ Z | xl ≤Z z ≤Z xh ⊆ z ∈ Z | yl ≤Z z ≤Z yh = γI(y).

Per quanto riguarda l’estensivita di γI αI risulta, ∀S ∈ ℘(Z),

γI(αI(S)) = γI

((infZ(S), supZ(S))

)= z ∈ Z | infZ(S) ≤Z z ≤Z supZ(S) ⊇ S.

60

Resta da mostrare che αI γI e la funzione identita su I, e infatti, ∀x ∈ I,risulta

αI(γI(x)) = αI( z ∈ Z | xl ≤Z z ≤Z xh )= (infZ z ∈ Z | xl ≤Z z ≤Z xh , supZ z ∈ Z | xl ≤Z z ≤Z xh )= (xl, xh)

= x.

Il lavoro della piu alta facoltache e nell’uomo — la ragione —

mira appunto ad una continua limitazione dell’infinitoe alla suddivisione dell’infinito in porzioni comode,

facilmente assimilabili. . .

— EVGENIJ ZAMJATIN, in Noi (1922)

61

5.3 Bounding box

Come abbiamo gia accennato, una bounding box rappresenta, per qualche nfinito, una regione rettangolare n-dimensionale (possibilmente infinita) coni lati paralleli agli assi coordinati, ed e pertanto univocamente determinatadalle sue proiezioni sugli n assi. Queste proiezioni sono ben rappresentateda intervalli, nel senso che abbiamo dato a questo termine nella sezione 5.2.Tenendo presente questa intuizione, definiamo ora le bounding box comeparticolari assegnamenti di intervalli a variabili. Faremo questo in due passi:prima definiremo le valutazioni su intervalli , le bounding box saranno poidefinite come particolare classi di equivalenza di queste valutazioni.

Definizione 5.3.1 Sia B ⊆ Vars → I l’insieme delle “valutazioni su inter-valli” cosı definito:

∀b ∈ B, X ∈ Vars | b(X) 6= >I ⊆f Vars

Dal momento che, per la proprieta appena vista, una valutazione su in-tervalli assume valori differenti da >I per al piu un numero finito di variabili,e possibile usare la seguente notazione, per ogni b ∈ B:

b = [I1]X1 , . . . , [In]Xn

dove

X1, . . . , Xn ⊆ Vars ,

I1, . . . , In ⊆ I \ >I,

significa

b(X) =

Ik se X = Xk, k ∈ 1, . . . , n,>I se X /∈ X1, . . . , Xn.

Inoltre, nelle stesse ipotesi, le funzioni dom:B → ℘f (Vars) e cod :B → ℘f (I\>I) sono date da:

dom(b) = X1, . . . , Xn,cod(b) = I1, . . . , In,

e b viene detta essere di cardinalita n, scritto |b| = n.Nell’insieme B appena definito vi sono piu elementi nulli , ovvero che

hanno ⊥I nel proprio codominio. In altre parole, tra i parallelepipedi del-l’insieme B ve ne sono infiniti di volume nullo, ovvero che hanno proiezionevuota su almeno un asse. Vogliamo invece un’algebra nella quale tutti questi

62

elementi minimali siano collassati in un unico elemento minimo. A questoscopo viene introdotta una relazione di equivalenza su B. Intuitivamenteconsidereremo equivalenti tutte le valutazioni su intervalli che hanno ⊥I nelproprio codominio (tutti i parallelepipedi di volume nullo).

Definizione 5.3.2 Su B e definita la relazione ≈B⊂ B ×B tale che:

≈B = (b1, b2) ∈ B ×B | b1 = b2 ∪ (b1, b2) ∈ B ×B | ⊥I ∈ cod(b1) ∩ cod(b2) ,

doveb1 = b2 ⇐⇒ ∀X ∈ Vars , b1(X) = b2(X).

Proposizione 5.3.1 ≈B e una relazione di equivalenza su B.

Dim. E banalmente riflessiva, simmetrica e transitiva.

Siamo ora in grado di definire l’insieme delle bounding box come l’insiemedella classi di equivalenza di valutazioni su intervalli modulo ≈B.

Definizione 5.3.3 L’insieme delle bounding box, B e cosı definito:

B = B/≈B ;

sono inoltre definiti i seguenti elementi di B:

>B = [ε]/≈B , dove ∀X ∈ Vars , ε(X) = >I ,⊥B =

[[⊥I ]W

]/≈B

, dove W ∈ Vars .

A questo punto definiamo una relazione d’ordine parziale che cattura lanozione (geometrica) dell’essere una bounding box contenuta in un’altra.

Definizione 5.3.4 Su B e definita la relazione ≤B, tale che, ∀b1, b2 ∈ B:

b1 ≤B b2 ⇐⇒ (b1 = ⊥B) ∨ (∀X ∈ Vars , b1(X) ≤I b2(X)).

Proposizione 5.3.2 ≤B e una relazione di ordinamento parziale su B.

Dim. E chiaro dalla definizione che, ∀b ∈ B, risulta b ≤B b. Inoltre,∀b1, b2 ∈ B, se b1 ≤B b2 e b2 ≤B b1 vi sono due casi: se b1 = ⊥B deve essereanche b2 = ⊥B. Se invece b1 6= ⊥B allora si ha che

∀X ∈ Vars , b1(X) ≤I b2(X),∀X ∈ Vars , b2(X) ≤I b1(X);

63

essendo ≤I una relazione d’ordine da cio si conclude che ∀X ∈ Vars ,

∀X ∈ Vars , b1(X) = b2(X),

ovvero che b1 = b2. Infine, ∀b1, b2, b3 ∈ B, se b1 ≤B b2 e b2 ≤B b3 vi sonoancora due casi: se b1 = ⊥B allora b1 ≤B b3 per definizione. Altrimenti, seb1 6= ⊥B risulta

∀X ∈ Vars , b1(X) ≤I b2(X),

e dunque b2 6= ⊥B, ma allora anche

∀X ∈ Vars , b2(X) ≤I b3(X).

Per la transitivita di ≤I si conclude che

∀X ∈ Vars , b1(X) ≤I b3(X),

ovvero che b1 ≤B b3.

Proposizione 5.3.3 Il poset (B,≤B) e completo.

Dim. L’elemento ⊥B e il minimo di B, per definizione di ≤B. Sia ora S ⊆ B,S 6= ∅, e sia

c =[

[supI b(X) | b ∈ S \ ⊥B ]X∣∣∣ X ∈ Vars

]/≈B

.

La definizione di c e ben posta, poiche I e un reticolo completo. Inoltrec ∈ B, dal momento che, se c 6= ⊥B,

dom(c) =⋂

b∈S\⊥B

dom(b),

e dunque|dom(c)| ≤ min

b∈S\⊥B|dom(b)| .

Ne consegue che X ∈ Vars | c(X) 6= >I e un sottoinsieme finito di Vars .E chiaro che

∀b ∈ S, b ≤B c.Sia ora c′ un altro limite superiore per S, ovvero tale che

∀b ∈ S, b ≤B c′,

cio implica, per la definizione di ≤B, che

∀b ∈ S,(

(b = ⊥B) ∨ (∀X ∈ Vars , b(X) ≤I c′(X))),

64

ovvero che

(S = ⊥B) ∨ (∀X ∈ Vars , supI b(X) | b ∈ S \ ⊥B ≤I c′(X)).

Ora, se il primo disgiunto e vero, allora c = ⊥B e c ≤B c′. Se il secondodisgiunto e vero si ha che

∀X ∈ Vars , c(X) ≤I c′(X),

e ancora c ≤B c′. Tanto basta per concludere che c = supB(S) e dunque cheil poset (B,≤B) e completo.

Come ultima osservazione si noti che infB e cosı definito: ∀S ⊆ B, posto

µ(S) =∣∣∣⋃b∈S

dom(b)∣∣∣,

si ha

infB(S) =

⊥B se µ(S) = ℵ0,[[infI b(X) | b ∈ S ]X

∣∣∣ X ∈ Vars]

/≈Bse µ(S) < ℵ0.

Infatti, se µ(S) = ℵ0 significa che in S sono infinite le variabile alle quali eassegnato un intervallo diverso da quello illimitato ovunque. Dunque nessunelemento di B\⊥B puo essere minorante di S, poiche in B vi sono solo (classidi equivalenza di) assegnamenti finitari di intervalli a variabili. D’altra parte⊥B e, per definizione, il minimo di B e quindi infB(S) = ⊥B. Se inveceµ(S) < ℵ0 allora infB(S) e chiaramente la classe di equivalenza di B cheassocia ad ogni variabile X ∈ Vars l’intervallo infI b(X) | b ∈ S . Si notiche |S| = ℵ0 e condizione solo necessaria perche si abbia µ(S) = ℵ0. Adesempio, per

S =⋃i∈N

bi,

dovebi =

[[(−i, i)]X

]/≈B

,

si ha |S| = ℵ0, ma µ(S) = 1.

Siamo ora in grado di definire l’algebra delle bounding box esplicitandogli operatori di composizione.

Definizione 5.3.5 L’algebra delle bounding box, B, e cosı definita:

B = (B,⊗B,⊕B,>B,⊥B)

65

-

6

X

Y

0

r r

rrr

r

rr rrr rrrr

r

rr

-

6

X

Y

0

r r

rrr

r

rr rrr rrrr

r

rr

Figura 5.3: Congiunzione di due bounding box

dove, ∀b1, b2 ∈ B,

b1 ⊗B b2 =[

[b1(X)⊗I b2(X)]X

∣∣∣ X ∈ Vars]

/≈B;

b1 ⊕B b2 =

b1 se b2 = ⊥B,b2 se b1 = ⊥B,[

[b1(X)⊕I b2(X)]X

∣∣∣ X ∈ Vars]

/≈Baltrimenti.

Un’idea intuitiva del significato degli operatori “⊗B” e “⊕B” puo esserericavata dalle figure 5.3 e 5.4. Le bounding box operandi sono rappresentatecon linee sottili mentre la bounding box risultante e tracciata con linee piuspesse. La congiunzione (“⊗B”, figura 5.3) di due bounding box e la sem-plice intersezione, e la disgiunzione (“⊕B”, figura 5.4) corrisponde all’unioneconvessa. Si osservi che mentre la disgiunzione di due bounding box mini-me e una bounding box minima, lo stesso non e vero per la congiunzione(figura 5.3).

Proposizione 5.3.4 B e un reticolo limitato e completo.

Dim. Per quanto visto nella dimostrazione della proposizione 5.3.3 eevidente che, ∀b, c ∈ B,

b⊕B c = supBb, c,b⊗B c = infBb, c,

dunque B e un reticolo completo. Cio implica che e limitato e gli annichilatorisono >B e ⊥B. Valgono infatti, banalmente, ∀b ∈ B, le uguaglianze b⊗B⊥B =⊥B e b⊕B >B = >B.

66

-

6

X

Y

0

rrr rr r rr r r

-

6

X

Y

0

rrr rr r rr r r

Figura 5.4: Disgiunzione di due bounding box

Chiudiamo questa sezione mettendo in relazione le bounding box con lesoluzioni dei vincoli di CLP(FD), e cioe con le FD-valutazioni.

Definizione 5.3.6 Siano αB:℘(Θ) → B e γB:B → ℘(Θ) le funzioni cosıdefinite, ∀θ ∈ Θ, ∀S ⊆ Θ e ∀b ∈ B, b 6= ⊥B:

αB(θ) =[

αI(θ(X))]X

∣∣∣ X ∈ dom(θ),

αB(S) = supB

αB(θ)

∣∣∣ θ ∈ S ,γB(⊥B) = ∅,

γB(b) =θ ∈ Θ

∣∣∣ dom(θ) ⊇ dom(b), ∀X ∈ dom(θ), θ(X) ∈ γI(b(X)).

Si osservi che dalla definizione discende:

αB(∅) = ⊥B,

e che inoltre si ha

X ∈ dom(θ) ⇒ αI(θ(X)) = (θ(X), θ(X)).

Proposizione 5.3.5 La coppia di funzioni 〈αB, γB〉 e un’inserzione di Galoisdi (B,≤B) in (℘(Θ),⊆).

Dim. Dalla definizione discende immediatamente che, se S1, S2 ⊆ Θ conS1 ⊆ S2, allora, per le proprieta di supB, risulta αB(S1) ≤B αB(S2). DunqueαB e monotona. Per la monotonia di γB, siano b1, b2 ∈ B tali che b1 ≤B b2.Se b1 = ⊥B allora

γB(b1) = ∅ ⊆ γB(b2).

67

Altrimenti, se b1 6= ⊥B, deve essere b2 6= ⊥B e la condizione b1 ≤B b2 diviene,per la definizione 5.3.4,

∀X ∈ Vars , b1(X) ≤I b2(X),

il che implica dom(b1) ⊇ dom(b2) e, per la monotonia di γI mostrata nellaproposizione 5.2.6,

∀X ∈ Vars , γI(b1(X)) ⊆ γI(b2(X)).

Sia ora θ ∈ γB(b1), ovvero

dom(θ) ⊇ dom(b1) e ∀X ∈ dom(θ), θ(X) ∈ γI(b1(X)),

allora, per quanto visto sopra, risulta

dom(θ) ⊇ dom(b1) ⊇ dom(b2)

e∀X ∈ dom(θ), θ(X) ∈ γI(b1(X)) ⊆ γI(b2(X),

dunque θ ∈ γB(b2). Da cio discende che γB(b1) ⊆ γB(b2), e quindi la mo-notonia di γB. Occorre ora mostrare che γB αB e estensiva. Si inizi conl’osservare che, per θ ∈ Θ, poiche non puo essere αB(θ) = ⊥B, si ha

γB(αB(θ)) = γB

( [αI(θ(X))

]X

∣∣∣ X ∈ dom(θ))

= ϑ ∈ Θ | dom(ϑ) ⊇ dom(θ), ∀X ∈ dom(θ), ϑ(X) = θ(X) ⊇ θ.

Siano ora S ⊆ Θ e θ ∈ S, per le proprieta di supB si ha

αB(θ) ≤B supBαB(ϑ) | ϑ ∈ S = αB(S),

e, per la monotonia di γB,

θ ∈ θ ⊆ γB(αB(θ)) ⊆ γB(αB(S)).

Ne consegue che S ⊆ γB(αB(S)) e dunque l’estensivita di γBαB. Verifichiamoora che αB γB e la funzione identita. Intanto risulta

αB(γB(⊥B)) = αB(∅) = ⊥B.

68

Sia ora b ∈ B, b 6= ⊥B. Per le definizioni di αB, γB, supB e per la proposizione5.2.6, risulta

αB(γB(b)) = supB

αB(θ)

∣∣∣ θ ∈ γB(b)

= supB

[

αI(θ(X))]X

∣∣∣ X ∈ dom(θ) ∣∣∣∣∣∣∣∣

θ ∈ Θ,dom(θ) ⊇ dom(b),∀X ∈ dom(θ) :θ(X) ∈ γI(b(X))

=

[αI(γI(b(X)))

]X

∣∣∣ X ∈ dom(b)

=

[b(X)]X

∣∣∣ X ∈ dom(b)

= b.

Quando una scatola piu piccola s e situata, in quiete relativa,dentro lo spazio cavo di una scatola piu grande S,

allora lo spazio cavo di s e una parte dello spazio di S,

e lo stesso “spazio” che le contiene entrambe appartiene a ciascuna delle due.

— ALBERT EINSTEIN, in Relativita e Problema dello Spazio (1952)

69

5.4 Dai vincoli alle bounding box

In questa sezione ci occupiamo della soluzione del seguente problema: datoun vincolo, come ottenere una bounding box che approssimi il suo insiemedi soluzioni? Piu formalmente, dato un vincolo c vogliamo determinare unabounding box b tale che

ϑ | FD |= cϑ ⊆ γB(b),

o, ragionando equivalentemente sugli intervalli, tale che

∀X ∈ Vars , θ ∈ ϑ | A |= cϑ ⇒ θ(X) ∈ γI(b(X)).

Come accennato all’inizio del capitolo, il problema si puo vedere in termi-ni geometrici nel seguente modo: consideriamo un vincolo c con k variabili.L’insieme delle k-ple di valori che lo soddisfano definisce una sagoma nellospazio k-dimensionale. Il problema e quello di determinare delle approssi-mazioni per le proiezioni di questa sagoma sugli assi coordinati associati allevariabili. In altre parole si vuole ottenere un parallelepipedo k-dimensionaleil cui volume circoscriva, o comunque copra, la sagoma definita dal vincolo.

5.4.1 Possibili soluzioni

Esistono vari metodi in letteratura che potrebbero essere buoni candidatiper la risoluzione del nostro problema. Seppure questi non siano utilizzatinella presente tesi, sono certamente da tenere in considerazione per esten-sioni o sviluppi futuri. Di seguito ne vengono citati due che consideriamopromettenti.

Il metodo SUP-INF

Il metodo SUP-INF, originariamente presentato in [8], consente di dimostrareteoremi di una classe di formule logiche che si incontrano frequentemente nelcampo della verifica dei programmi. Le formule di Presburger sono le formuleben formate che si possono costruire a partire da: interi, variabili intere,addizione, moltiplicazione per una costante, le usuali relazioni aritmetiche ei connettivi della logica del primo ordine. Ad esempio, (∀x)(∃y)3x + y =2 ⇒ x < y e una formula di Presburger. La sottoclasse sulla quale opera ilmetodo SUP-INF e quella delle formule di Presburger che, una volta postein forma prenessa, contengano solo quantificatori universali.

La procedura di prova consiste di due passi. Nel primo, la formula Fda dimostrare e ricondotta ad un insieme di problemi di programmazione

70

lineare intera (ILP), con la proprieta che F e valida se e solo se nessuno deiproblemi ha soluzione. Nel secondo passo i problemi ILP sono controllati,uno alla volta, per verificare se ammettano soluzioni. Il nostro interesse per ilmetodo SUP-INF viene dalla tecnica utilizzata per realizzare questo secondopasso. Sono infatti impiegati due algoritmi, SUP e INF, che calcolano unalimitazione, rispettivamente, superiore e inferiore dei valori che una varia-bile reale puo assumere rispetto ad un insieme di vincoli lineari. Dato uninsieme di vincoli lineari S, per ogni variabile x che occorre in S vengonocalcolati INFS(x) e SUPS(x). Se per qualche x in S risulta che l’intervallochiuso [INFS(x), SUPS(x)] non contiene interi, se ne conclude che il sistemadi partenza S non ha soluzioni intere. Nulla si puo invece concludere in casocontrario. In [8] e dimostrato che i due algoritmi sono conservativi , vale a di-re che SUP non calcola mai un valore “troppo piccolo” e che INF non calcolamai un valore “troppo grande”. Tanto basta per garantire la correttezza delmetodo. In [53] e mostrato che non solo le limitazioni calcolate da SUP e INFsono corrette, ma sono anche esatte, nel senso che calcolano il massimo e ilminimo valore che una variabile puo assumere su un dato insieme di vincoli.

Una possibile soluzione al nostro problema e dunque, per quanto dettosopra, quella di utilizzare gli algoritmi SUP e INF per calcolare la boundingbox che approssima lo spazio di soluzioni di un insieme di vincoli lineari.Gli algoritmi SUP e INF possono trattare anche problemi ILP non esplicita-mente limitati, e dunque calcolare intervalli infiniti. Vedremo che l’algoritmoutilizzato in questa tesi non gode di questa proprieta.

Varianti del metodo di Fourier–Motzkin

Un metodo per la risoluzione dei problemi di programmazione lineare e quel-lo di eliminazione delle variabili di Fourier–Motzkin [17]. L’idea di base delmetodo e quella di ridurre progressivamente il numero delle variabili del pro-blema combinando opportunamente le disequazioni che vi compaiono. Intui-tivamente l’algoritmo di Fourier–Motzkin calcola, ad ogni iterazione, l’ombra(n− 1)-dimensionale proiettata da un oggetto n-dimensionale.

Una recente variante del metodo di Fourier–Motzkin va sotto il nomedi Omega Test [50, 51], ed e stata sviluppata nell’ambito della ricerca suicompilatori ottimizzanti per i linguaggi imperativi, in particolare per quantoriguarda le analisi che consentono un’efficiente vettorizzazione dei programmiFORTRAN. Come il metodo di Fourier–Motzkin, l’algoritmo Omega Teste basato sul concetto di proiezione, ma per problemi di programmazionelineare intera. Essenzialmente Omega Test ha come input un problema ILPP su un certo insieme di variabili V , e un altro insieme di variabili V ⊆ V .L’algoritmo restituisce un problema P sulle variabili in V . P descrive, in

71

modo conservativo, i possibili valori delle variabili in V tali che esiste unasoluzione intera di P con quei valori. Ad esempio, la proiezione di 0 ≤a ≤ 5, b < a ≤ 5b su a risulta in 2 ≤ a ≤ 5. Il metodo Omega Teste stato effettivamente implementato e viene utilizzato in alcuni prototipi dicompilatori ottimizzanti.

5.4.2 Una soluzione offerta dall’AI

Il metodo che utilizzeremo in questo lavoro per inferire le bounding boxdai vincoli viene dal campo dell’intelligenza artificiale, dove le tecniche dideduzione approssimata sono oggetto di ricerca da lungo tempo. Infattimolti problemi trattati in AI (tra i quali l’inferenza induttiva che qui piu ciinteressa) sono, dal punto di vista della complessita computazionale, difficilise non intrattabili in generale. Ciononostante tali problemi vanno in qualchemodo risolti dai sistemi di AI, per basi di conoscenza anche complesse e intempi ragionevoli. Vi sono solo due sole possibilita per raggiungere questoobiettivo: o scoprire che il particolare problema ha caratteristiche speciali chelo rendono trattabile, o accontentarsi di soluzioni approssimate calcolabili daalgoritmi efficienti. E questo dilemma che ha condotto alla messa a puntodi svariate tecniche di inferenza approssimata, una delle quali, sara l’oggettodella seguente trattazione.

Il tipo di inferenza che qui ci interessa e quella di tipo quantitativo suipossibili valori delle variabili dati i vincoli che le legano. Problemi del tuttoanaloghi si incontrano in intelligenza artificiale. Buona parte della cono-scenza in diversi “sistemi esperti” puo essere espressa in termini di relazionimatematiche tra quantita numeriche. E questo il caso dei sistemi che imple-mentano forme di ragionamento temporale, basato su relazioni tra tempi edurate [3], oppure nel ragionamento spaziale, basato su relazioni tra lunghez-ze o angoli [43, 54, 55]. Spesso la gestione di queste relazioni e l’inferenza sudi esse puo essere demandata ad un modulo distinto, chiamato base di cono-scenza quantitativa. Un’architettura usata per l’implementazione di questebasi di conoscenza e la rete di vincoli e le tecniche di inferenza usate su talearchitettura sono note con il nome generico di propagazione di vincoli [19].

5.4.3 Reti e propagazione di vincoli

Una rete di vincoli e una struttura dichiarativa che esprime relazioni traparametri, ed e costituita da un certo numero di nodi connessi da vincoli.Un nodo rappresenta un singolo parametro al quale e associato un particolarevalore, noto o ignoto. Un vincolo rappresenta una relazione tra i valori deinodi che esso connette. Tipicamente un vincolo connette solo pochi nodi. Ad

72

esempio, nel programma di Waltz per l’interpretazione delle linee in scenecon ombreggiature, ogni nodo e un elemento dell’immagine, i suoi valori sonole possibili interpretazioni e i vincoli sono regole che stabiliscono la coerenzadell’interpretazione [60].

L’inferenza forward su una rete di vincoli, chiamata assimilazione e rea-lizzata per mezzo della tecnica di propagazione dei vincoli . Questa tecnicaconsiste, in generale, nell’applicazione ripetuta dei seguenti tre passi:

1. selezionare un piccolo gruppo di nodi e vincoli in una sezione connessadella rete;

2. dedurre nuove informazioni da quelle presenti nei nodi e vincoli sele-zionati;

3. aggiornare le informazioni in questa sezione della rete.

Si osservi che, ad ogni iterazione, le informazioni dedotte sono registratecome modifiche alla rete. Le iterazioni successive utilizzeranno queste modi-fiche per eseguire ulteriori deduzioni e produrranno nuovi cambiamenti nellarete di vincoli. In questo modo le conseguenze di ogni dato si diffondonogradualmente attraverso la rete. Il procedimento e ripetuto fino a che nonvi sono piu modifiche; quando cio avviene la rete e detta essere in quiete ostabile. Le reti di vincoli possono essere interrogate richiedendo il valore diun termine o il valore di verita di una proposizione in base allo stato dellarete. Normalmente le reti di vincoli sono strutturate in modo da eseguire lamaggior parte delle inferenze nella fase di assimilazione, e le interrogazionipossono cosı essere gestite rapidamente a partire dallo stato finale della rete.In genere le interrogazioni non producono modifiche nello stato della rete.

I diversi sistemi di propagazione di vincoli hanno in comune alcune ca-ratteristiche positive:

1. la propagazione di vincoli e realizzabile da una semplice struttura dicontrollo (iterazione) applicata ad un semplice modulo di aggiornamen-to, e quindi facile da codificare, analizzare ed estendere. Le sue azionisono inoltre di semplice spiegazione, il che facilita la generazione digiustificazioni per le deduzioni effettuate.

2. Qualora siano imposte limitazioni sul tempo di esecuzione, il sistemapuo essere semplicemente interrotto: le informazioni dedotte fino a quelmomento sono valide ed utilizzabili.

3. I sistemi si possono facilmente implementare in forma parallela, dalmomento che le deduzioni e gli aggiornamenti possono essere effettua-ti simultaneamente su tutta la rete. In certi casi e concettualmente

73

possibile implementare ogni vincolo con un processore che aggiorna leinformazioni sui nodi che connette non appena alcuni di questi cambinostato.

4. Sono naturalmente incrementali . Un vincolo puo essere aggiunto in-corporandolo nella rete, aggiornando i nodi che esso connette, e propa-gando le conseguenze di queste modifiche.

Riguardo all’ultima caratteristica citata, si rammenti che l’incrementalita euna delle caratteristiche principali richieste per il risolutore di vincoli di unsistema CLP.

Nelle applicazioni di intelligenza artificiale si possono distinguere diversecategorie di propagazione di vincoli, basando la distinzione sul tipo delleinformazioni che vengono aggiornate. Sistemi che appartengono a due diqueste categorie sono utilizzati in questo lavoro, altri due tipi di inferenzavengono citati per mostrare la generalita del paradigma.

• Nella inferenza di etichette ogni nodo e etichettatto con un insieme dipossibili valori che esso puo assumere. Nel processo di assimilazione ivincoli vengono usati per restringere gradualmente questi insiemi. Ilsistema usato nell’analisi presentata in questo capitolo per ottenerele bounding box dai vincoli ricade in questa classe: nel nostro casole etichette sono intervalli e i valori possibili che una variabile puoassumere sono quelli contenuti negli intervalli.

• Nella inferenza di vincoli si deducono nuovi vincoli e li si aggiungonoalla rete.

• Nella inferenza di valori i nodi sono etichettati con valori costanti o conl’indicazione di valore ignoto. I vincoli sono usati per trovare valori deinodi il cui valore e ignoto a partire da quelli il cui valore e noto.

• L’inferenza di espressioni e una generalizzazione dell’inferenza di valorinella quale i nodi possono essere etichettati con un valore espresso intermini dei valori di altri nodi. Quando a un nodo sono assegnate duediverse etichette queste sono uguagliate e l’equazione risultante vienerisolta.

Le categorie qui presentate sono tutte deduttivamente corrette, ma ve nesono altre, usate in AI, che non lo sono.

Ogni tecnica di propagazione di vincoli ha anche degli svantaggi, ovvia-mente. Per quanto riguarda le categorie di cui sopra, l’inferenza di valori el’inferenza di espressioni possono essere utilizzate solo con vincoli di ugua-glianza e non di disuguaglianza. L’inferenza di etichette e l’inferenza di

74

vincoli sono invece difficili da controllare. La prima puo non terminare (ve-dremo come questo non sia il caso se si considerano domini finiti), mentrenell’inferenza di vincoli puo essere difficile o addirittura impossibile accertarsiche i vincoli dedotti abbiano un qualche rilevanza ed utilita. D’altra partel’inferenza di etichette ha il pregio di essere applicabile con vincoli di formaarbitraria.

5.4.4 Inferenza di etichette

Come abbiamo gia accennato, nei sistemi di inferenza di etichette ogni nodoe etichettato con l’insieme dei suoi possibili valori. Nelle interrogazioni iltermine da valutare e espresso come funzione di un certo numero di nodie il sistema deve calcolare i possibili valori di questa funzione in base alleetichette dei nodi argomento. Nell’assimilazione gli insiemi che etichettanoi nodi vengono aggiornati con un procedimento detto di raffinamento delleetichette, che consiste nel restringere l’insieme etichetta di un nodo in basea un vincolo e alle etichette di tutti gli altri nodi collegati dal vincolo stesso.Ad esempio, se abbiamo il vincolo X + Y = Z e le etichette X ≥ 3 eY = 1 per i nodi X e Y , allora possiamo dedurre che Z ≥ 4 ed eliminaredall’insieme etichetta di Z tutti quei valori che sono inconsistenti rispetto aquesta deduzione.

Il raffinamento, nella sua forma piu generale, puo essere cosı definito:

Definizione 5.4.1 Sia C un vincolo sui nodi X1, . . ., Xk, e sia, per ognii = 1, . . . , n, Si l’insieme etichetta per Xi. Allora, ∀j = 1, . . . , k,

REFINE(C,Xj) = vj ∈ Sj | ∀i = 1, . . . , k, i 6= j,

∃vi ∈ Si . C(v1, . . . , vj, . . . , vk) .

In altre parole, REFINE(C,Xj) e l’insieme dei valori nell’etichetta di Xj

che sono consistenti con il vincolo C e con le etichette Xi dei restanti nodicollegati da C. Un valore vj e in REFINE(C,Xj) se e in Sj e se e elementodi una k-pla (v1, . . . , vk) che soddisfa C e tutte le etichette Si. Si osserviche il raffinamento e deduttivamente corretto, ovvero se una k-pla soddisfail vincolo e le etichette iniziali, allora soddisfa anche le etichette raffinate.

Il passo elementare di raffinamento dell’etichetta di un nodo deve essereripetuto, propagando, attraverso i vincoli, le conseguenze del raffinamentosu tutta la rete. Questo si ottiene per mezzo di un’opportuna struttura dicontrollo che applica iterativamente la funzione REFINE, fino a che non siproducono piu modifiche nella rete, ovvero e stata raggiunta la quiescenza.Questo procedura e nota come algoritmo di Waltz ed e stata presentata per

75

la prima volta in [60]. Siccome il raffinamento e deduttivamente corretto,cosı e anche l’algoritmo di Waltz, che non fa altro che iterarlo. Cio vale adire che, se un dato assegnamento ai parametri soddisfa tutti i vincoli e leetichette iniziali, allora soddisfera anche le etichette calcolate dall’algoritmodi Waltz. Se l’algoritmo termina assegnando a qualche parametro l’insiemevuoto, allora lo stato iniziale era inconsistente.

Prima di introdurre la particolare implementazione dell’algoritmo di Wal-tz che risolve il nostro problema di derivazione delle bounding box, precisiamomeglio il tipo di inferenza che ci interessa. Tre caratteristiche fondamentalidi un sistema di inferenza di etichette sono: il linguaggio dei vincoli, il tipodi termini usati come nodi e il tipo dei predicati usati come etichette. Nelnostro caso i vincoli sono le relazioni aritmetiche di CLP(FD) cosı come so-no state definite nella sezione 4.2, i nodi rappresentano le variabili e l’unicopredicato usato nelle etichette e quello di appartenenza ad un intervallo.

Vedremo tra breve come si puo definire la funzione di raffinamento pergli intervalli e i vincoli di CLP(FD). Faremo questo direttamente nel no-stro contesto, ovvero parlando di raffinamento di bounding box, essendo unabounding box nient’altro se non un assegnamento di intervalli a variabili.

5.4.5 Normalizzazione dei vincoli

Nel seguito sara utile fare riferimento ad una opportuna forma normalizzatadei vincoli atomici. A questo scopo, non e restrittivo supporre l’esistenza diun relazione di ordinamento totale definita su Vars : sia dunque ≤V una talerelazione.

Definizione 5.4.2 Un vincolo e normalizzato se non e lineare, oppure se edella forma:

n∑i=1

aiXi = (a1X1 + (a2X2 + · · ·+ (an−1Xn−1 + anXn) · · ·)) ./ b

dove

./ ∈ =, 6=,≤,ai ∈ Z, ∀i = 1, . . . , n,

b ∈ Z,

i ≤ j ⇒ Xi ≤V Xj, ∀i, j = 1, . . . , n.

egcda1, . . . , an = 1.

76

E sempre possibile ricondursi al caso di vincoli normalizzati. Innanzituttoun vincolo che non contenga variabili e sempre eliminabile dai programmi. Siainfatti c un tale vincolo: se FD |= c allora c puo essere eliminato dalle clausolenelle quali compare. Se invece FD 6|= c allora possono essere eliminate dalprogramma le clausole che contengono il vincolo c.

Per quanto riguarda i vincoli lineari con variabili, questi sono tutti ricon-ducibili alla forma canonica equivalente

n∑i=1

aiXi ./ b,

dove ./∈ =, 6=,≤, <,≥, >. Essenzialmente si tratta di distribuire la molti-plicazione sull’addizione e di raccogliere le costanti. Algoritmi che realizzanoquesta trasformazione sono ben noti in letteratura [29, 9, 59]. Il buon ordina-mento degli addendi, consentito dalla commutativita della somma, e otteni-bile mediante un qualunque algoritmo di sort. Fatto questo, se ./∈ <,≥, >si trasforma

n∑i=1

aiXi ./ b in

∑n

i=1 aiXi ≤ b− 1, se ./∈ <,∑ni=1(−ai)Xi ≤ −b, se ./∈ ≥,∑ni=1(−ai)Xi ≤ −b− 1, se ./∈ >.

Ora, per ottenere la forma normalizzata si calcola il massimo divisore comunedei coefficienti ai, sia questo g. I coefficienti vanno comunque divisi per g,ma, a questo punto, possono darsi piu casi: se il vincolo e di uguaglianza eg | b (g divide b), allora si trasforma

n∑i=1

aiXi = b inn∑i=1

aigXi =

b

g;

se invece g 6 | b allora il vincolo e insoddisfacibile, e dunque

n∑i=1

aiXi = b equivale a false.

Consideriamo ora un vincolo in cui il simbolo di relazione sia 6=, in mododuale si trasforma

n∑i=1

aiXi 6= b inn∑i=1

aigXi 6=

b

g

se g | b, se invece g 6 | b si trasforma

n∑i=1

aiXi 6= b in true.

77

Per quanto riguarda i vincoli di disuguaglianza, che abbiamo tutti ricondottia relazioni di ≤, basta trasformare

n∑i=1

aiXi ≤ b inn∑i=1

aigXi ≤

⌊b

g

⌋.

Si osservi che il considerare la parte intera inferiore del termine costanterafforza il vincolo. Se un vincolo ha soluzioni razionali, ma non intere, lasua normalizzazione puo condurre ad un vincolo senza soluzioni razionali,rendendo in tal modo piu semplice il riconoscimento del fatto che tale vincolonon ha nemmeno soluzioni intere.

Per comodita di presentazione incapsuliamo tutto il procedimento di cuisopra nella funzione

norm:C → C,

che, dato un vincolo atomico, restituisce la sua forma normalizzata. Conti-nueremo a denotare con Ca l’insieme dei vincoli atomici normalizzati. Dallacostruzione effettuata e evidente che il procedimento di normalizzazione ecorretto rispetto alle soluzioni. Vale a dire che, per ogni vincolo atomico crisulta

Sol(c) = Sol(norm(c)).

Dunque, senza alcuna perdita di generalita, nel seguito considereremo soloprogrammi CLP(FD) nei quali tutti i vincoli atomici siano (stati) normaliz-zati.

5.4.6 Raffinamento delle bounding box

In questa sezione definiamo una funzione refine che ha come parametri:

1. un vincolo atomico normalizzato c;

2. una bounding box b;

3. una variabile X della quale si vuole raffinare l’intervallo associato.

Con questi dati in ingresso la funzione refine restituisce un intervallo per lavariabile X, possibilmente contenuto in (e comunque non piu grande di) quel-lo associato da b ad X. Questo intervallo puo essere utilizzato per restringerela bounding box b.

Consideriamo innanzitutto i vincoli lineari del tipo∑k

i=1 ciXi = z oppu-

re∑k

i=1 ciXi ≤ z, per i quali esiste una formula generale non iterativa diraffinamento degli intervalli associati alle variabili [19].

78

Definizione 5.4.3 Sia c un vincolo lineare nella forma generale∑i∈P

aiXi −∑i∈N

aiXi ./ z,

dove ./∈ =,≤, P e N sono gli insiemi degli indici cui corrispondono,rispettivamente, coefficienti positivi e negativi. Quindi si ha, ∀i ∈ P ∪ N ,ai ∈ Z, ai > 0 e z ∈ Z. Si pone

(zl, zh) =

(z, z) se ./ e la relazione =,(−∞, z) se ./ e la relazione ≤.

Sia poi b una bounding box tale che, ∀i ∈ P ∪N ,

b(Xi) = (xli, xhi ).

Se b non e finita per le variabili in c, ovvero se

∃j ∈ P ∪N . (xlj, xhj ) /∈ Z2,

allora refine(c, b,X) = b(X). Altrimenti, sia X ∈ Vars tale che

X = Xk con k ∈ P ∪N.

Se k ∈ P , allora si pone

(xlk, xhk) =

(⌈ 1

ak

(zl +

∑i∈N

aixli −

∑i∈P,i6=k

aixhi

)⌉,

⌊ 1

ak

(zh +

∑i∈N

aixhi −

∑i∈P,i 6=k

aixli

)⌋),

se invece k ∈ N , allora

(xlk, xhk) =

(⌈ 1

ak

(∑i∈P

aixli − zh −

∑i∈N,i6=k

aixhi

)⌉,

⌊ 1

ak

(∑i∈P

aixhi − zl −

∑i∈N,i6=k

aixli

)⌋).

Si noti che, per non allungare ulteriormente la definizione, si e implicita-mente utilizzata un’algebra dei “boundary” (definiti nella sezione 5.2) sullaquale risulta, per ogni n ∈ Z e per ogni numero razionale q ∈ Q, q > 0:

+∞± n = +∞,−∞± n = −∞,

+∞ · (±q) = ±∞,−∞ · (±q) = ∓∞.

79

Siano ora xlk = max(xlk, xlk) e xhk = min(xhk, x

hk), dove min e max sono gli

operatori definiti sui boundary nella sezione 5.2. Se risulta xlk > xhk, allorail sistema di partenza (vincolo e bounding box) era inconsistente. Il risultatodi refine(c, b,X) e, finalmente, dato da

refine(c, b,X) =

⊥I se xlk > xhk,(xlk, x

hk) altrimenti.

Dalla definizione discende che i vincoli di ≤ consentono di raffinare solo ilimiti superiori delle variabiliXk con k ∈ P e i limiti inferiori delle variabiliXk

con k ∈ N . I vincoli di uguaglianza permettono invece di raffinare entrambii limiti di ogni variabile.

Formule analoghe a quella appena vista esistono anche per alcuni semplicivincoli non lineari. Una di queste e la seguente [18].

Esempio 5.4.1 Si consideri il vincolo

X2 + Y X + Z = 0,

e sia b una bounding box tale che

b(X) = (xl, xh), b(Y ) = (yl, yh), b(Z) = (zl, zh).

I limiti inferiore e superiore, al e ah, per |Y | sono dati da

(al, ah) =

(yl, yh) se yl > 0,(−yh,−yl) se yl ≤ 0, yh < 0,(0,max(−yl, yh)) altrimenti.

I limiti Dl e Dh per Y 2 − 4Z si calcolano con

Dl = max(a2l − 4zh, 0), Dh = a2

h − 4zl.

Se Dh < 0 il sistema era inconsistente, altrimenti si pone

v1 = 12(−yh −

√Dh), v2 = 1

2(−yl −

√Dl),

v3 = 12(−yh −

√Dl), v4 = 1

2(−yl −

√Dh).

A questo punto l’intervallo risultato di refine(X2 +Y X+Z = 0, b,X) e datoda

(dmax(xl, v3)e, bmin(xh, v4)c),se xl > v2, altrimenti, se xh < v3, si ha come risultato

(dmax(xl, v1)e, bmin(xh, v2)c),

80

altrimenti il nuovo intervallo per X e

(dmax(xl, v1)e, bmin(xh, v4)c).

Se i limiti calcolati per X sono tali che il limite inferiore e maggiore dellimite superiore, allora il sistema di partenza (vincolo e bounding box) erainconsistente.

La teoria aritmetica degli intervalli [2] fornisce parecchie formule che pos-sono essere utili per il raffinamento di altri tipi di vincoli. Nel seguito cilimiteremo comunque a vincoli lineari escludendo la relazione 6=. Resta dun-que inteso che, se c e un vincolo normalizzato E1 ./ E2 dove ./ e la relazione6=, oppure E1 − E2 non e un’espressione lineare, allora

refine(c, b,X) = b(X)

per ogni b ∈ B e per ogni X ∈ vars(c).

5.4.7 L’algoritmo di Waltz per le bounding box

Presentiamo una versione efficiente dell’algoritmo di Waltz adattata ai nostriscopi. L’adattamento e dall’algoritmo AC-3 in [40, 41] e presentato anche,nella versione per la propagazione di vincoli su etichette, in [19]. L’algoritmo,in figura 5.5, fa uso del tipo di dato astratto “coda di vincoli” per il qualesono definite tre funzioni:

• initqueue(C) restituisce una coda contenente i vincoli dell’insieme C,

• remove(Q) restituisce un vincolo selezionato e rimosso dalla coda Q,

• enqueue(Q, c) restituisce la coda ottenuta inserendo il vincolo c in Q,a meno che c non vi sia gia presente, nel qual caso viene restituita Q.

vars(c) rappresenta, come sempre, l’insieme di variabili che compaiono nelvincolo c. Le bounding box sono rappresentate nella notazione “array” b[X],anziche in quella funzionale b(X). Cio dovrebbe rendere piu intuitivo ilsignificato di un assegnamento del tipo b[X] ← i, la cui semantica e: qualeche fosse l’intervallo associato dalla bounding box b a X (l’etichetta di X),dall’istante dell’assegnamento, fino ad un eventuale nuovo assegnamento, isara l’intervallo associato da b a X (i sara l’etichetta di X).

L’algoritmo usa la funzione ausiliaria revise con parametri una boundingbox b (la bounding box corrente) e un vincolo c. revise applica il raffinamen-to a tutte le variabili di c (linee 2–9) per mezzo della funzione refine della

81

function revise(inout b : bounding box,in c : constraint) : set of vars;

var changed : set of vars;i, inew : interval;X : variable;

begin changed ← ∅; (1)foreach X ∈ vars(c) do (2)

begin i← b[X]; (3)inew ← refine(c, b,X); (4)if inew 6= i then (5)

begin b[X]← inew ; (6)changed ← changed ∪ X (7)

end (8)end (9)

return changed (10)end.

function waltz (in b : bounding box,in C : set of constraints) : bounding box;

var Q : queue of constraints;changed : set of vars;bnew : bounding box;c, c′ : constraint;X : variable;

begin Q← initqueue(C); (1)bnew ← b; (2)while Q 6= ∅ and bnew 6= ⊥B do (3)

begin c← remove(Q); (4)changed ← revise(bnew , c); (5)foreach X ∈ changed do (6)

foreach c′ ∈ C \ c suchthat X ∈ vars(c′) do (7)Q← enqueue(Q, c′) (8)

end (9)return bnew (10)

end.

Figura 5.5: L’algoritmo di Waltz

82

Vincoli

Nodi

c1 : X + Y = Z

c2 : Y ≤ X

b[Z] = (2, 7)

b[Y ] = (3, 8)

b[X] = (1, 10)

J

JJJJJJ]JJJJJJJ

Z

ZZ

ZZZ

ZZ

ZZZZZZZZZZZZ~ B

BBBBBBMBBBBBBBN

Figura 5.6: Rete di vincoli

definizione 5.4.3. revise restituisce (linea 10) la bounding box, possibilmentemodificata, e l’insieme delle variabili delle quali e stata modificata l’etichetta(l’intervallo associato). Si osservi che refine puo ritornare (nel caso il siste-ma di partenza fosse inconsistente) l’intervallo vuoto ⊥I . In tal caso reviserestituira (linea 5) una bounding box nulla secondo le definizioni 5.3.2 e 5.3.3.

La funzione principale waltz , data una bounding box b e un insieme divincoli C, crea un coda (linea 1) contenente tutti i vincoli in C ed applicarevise (linea 5) ad ognuno di essi. Se un’applicazione di revise ha successo(modifica gli intervalli associati ad almeno una variabile), allora (linee 6–8)tutti i vincoli che contengono almeno una delle variabili modificate vengonoinseriti nuovamente nella coda (qualora non vi siano gia presenti). Il proce-dimento (linee 3–9) viene ripetuto fintanto che la coda non e vuota oppuresi e ottenuta una bounding box nulla. Finalmente viene restituita (linea 10)la bounding box modificata.

Vediamo ora, con un esempio, qual e una possibile sequenza di esecuzionedell’algoritmo in figura 5.5.

Esempio 5.4.2 Supponiamo che la funzione waltz di figura 5.5 sia invocatacon argomenti la bounding box b tale che

b[X] = (1, 10), b[Y ] = (3, 8), b[Z] = (2, 7),

e con l’insieme di vincoli C contenente

c1 : X + Y = Z, c2 : Y ≤ Z.

L’algoritmo parte inizializzando la coda di vincoli con c1 e c2. La rete risul-tante puo essere visualizzata come in figura 5.6. Poi l’algoritmo procede nelseguente modo:

1. c1 (X + Y = Z) e estratto dalla coda:

83

• siccome X ≥ 1 e Y ≥ 3, c1 permette di inferire (via refine) unnuovo intervallo per Z, ovvero (4, 7);

• essendo Z ≤ 7 e Y ≥ 3, si ottiene il nuovo intervallo (1, 4) perX;

• dal momento che gli intervalli per X e Z sono stati modificati, c2,che contiene X, sarebbe inserito in coda se non fosse per il fattoche c’e gia.

2. c2 (Y ≤ X) e estratto dalla coda:

• siccome X ≤ 4, c2 da Y ≤ 4 e il nuovo intervallo per Y e (3, 4);

• essendo Y ≥ 3, c2 da X ≥ 3 l’intervallo per X diventa (3, 4);

• dal momento che gli intervalli per X e Y sono cambiati, c1, checontiene X e Y , viene inserito in coda.

3. c1 (X + Y = Z) e estratto dalla coda:

• siccome X ≥ 3 e Y ≥ 3, c1 consente di dedurre l’intervallo (6, 7)per Z;

• dal momento che solo l’intervallo per Z e stato modificato e Znon compare in altri vincoli oltre a c1, in coda non viene aggiuntoalcun vincolo.

4. La coda e vuota: la procedura termina restituendo la nuova boundingbox b′ tale che

b′[X] = (3, 4), b′[Y ] = (3, 4), b′[Z] = (6, 7).

L’algoritmo di figura 5.5 puo essere modificato per gestire l’aggiunta divincoli a quelli eventualmente gia presenti in coda, mettendo cosı in risaltola natura incrementale della tecnica usata. Se C e l’insieme dei nuovi vincolida aggiungere, basta sostituire la linea (1) della funzione waltz con foreachc ∈ C do Q← enqueue(Q, c).

La terminazione e la complessita dell’algoritmo di Waltz sono state stu-diate estensivamente nel caso in cui il dominio dei parametri (nel nostro caso,variabili) sia finito [41, 40, 25]. In particolare, Mackworth e Freuder hannomostrato che, nel caso i vincoli siano solo su una o due variabili, l’algoritmotermina dopo O(ae) invocazioni alla funzione ausiliaria revise, dove a e lamassima cardinalita dei domini dei parametri ed e e il numero di vincoli. Ilfatto di considerare solo vincoli su una o due variabili non e restrittivo, dal

84

momento che una rete con vincoli qualsiasi e approssimabile con una rete disoli vincoli unari o binari [45, 25].

Nel nostro caso i vincoli sono su un numero qualsiasi di variabili e la com-plessita computazionale dell’algoritmo, in termini del numero di raffinamenti,e data dal seguente teorema.

Teorema 5.4.1 Siano b una bounding box e C un insieme di vincoli atomici.Allora l’algoritmo di figura 5.5, applicato ai parametri b e C, termina dopoaver invocato un numero O(n2ae) di volte la funzione refine, dove

n = |vars(c)|,e = |C|,a = max zh − zl + 1 | X ∈ vars(C), b(X) = (zl, zh) ∈ Z2 .

Dim. Verifichiamo innanzitutto che l’algoritmo di si arresta dopo aver invo-cato un numero O(nae) di volte la funzione revise. La coda Q della funzionewaltz contiene inizialmente (linea 1) e vincoli. Il numero di invocazioni arevise e pari al numero di elementi estratti da Q (linee 4–5). La funzioneausiliaria revise puo modificare la bounding box bnew e corrispondentementeritornare un insieme di variabili i cui intervalli sono stati modificati (linea 5)al piu na volte. Questo e il caso (pessimo) in cui ogni invocazione di reviseprovoca il restringimento di una sola unita dell’intervallo associato ad unasola variabile. Per ognuna di queste na volte vengono reinseriti in coda (li-nee 6–8) al piu e − 1 vincoli. Il numero di vincoli estratti da Q e pertantosuperiormente limitato da

e+ na(e− 1),

ovvero il numero di vincoli iniziali piu il numero delle nuove entrate. Dunquela funzione ausiliaria revise e invocata O(nae) volte.

La funzione refine viene chiamata da revise per ogni variabile del vincolo,cioe al piu n volte. In totale, l’algoritmo di figura 5.5 invoca la funzione refineun numero di volte superiormente limitato da ne+n2a(e−1) ∈ O(n2ae).

Il risultato di terminazione non e applicabile quando l’insieme delle possi-bili etichette e infinito. In questi casi l’analisi dell’algoritmo dipende stretta-mente dal tipo di vincoli usati. Ad esempio, potremmo pensare di modificareper CLP(<) lo schema di interpretazione astratta presentato in questo capi-tolo. La teoria delle bounding box sarebbe facilmente estesa al caso reale,le funzioni di raffinamento presentate nella definizione 5.4.3 e nell’esempio5.4.1 sarebbero applicabili con il solo accorgimento di eliminare gli opera-tori di parte intera, ma l’algoritmo di Waltz entrerebbe in un ciclo infinito

85

anche per insiemi di vincoli particolarmente semplici. Si considerino infat-ti l’insieme di vincoli X = Y,X = 2Y e la bounding box iniziale b taleche b(X) = b(Y ) = (0, 100). Il sistema e consistente con l’unica soluzioneX = Y = 0, ma l’algoritmo di figura 5.5 dedurrebbe dalla seconda equazioneche Y ∈ [0, 50], dalla prima X ∈ [0, 50], poi ancora Y ∈ [0, 25], X ∈ [0, 25],. . . Ne consegue che, in questo caso, la quiescenza della rete non e criteriosufficiente ad assicurare la terminazione, che dev’essere forzata in altro modo.Come abbiamo gia accennato la terminazione forzata non intacca la corret-tezza delle deduzioni affettuate fino al momento dell’arresto1. Ad esempiola propagazione puo essere arrestata dopo un certo tempo massimo, oppuresi puo imporre un limite superiore al numero di raffinamenti nei quali ognisingolo vincolo e coinvolto, oppure ancora si puo fissare una soglia minimasotto la quale l’entita del raffinamento di un’etichetta viene considerata nonsignificativa2.

I seguenti risultati riguardo l’algoritmo di Waltz saranno utili nel pro-sieguo. In realta, in forza del teorema 5.4.1, possiamo fare riferimento allafunzione

waltz :B × ℘f (Ca)→ B,

dove Ca e l’insieme dei vincoli atomici normalizzati, come definiti nella sezione5.4.5. Dato un insieme di vincoli atomici C e una bounding box b, si ponewaltz (b, C) = b se

∃X ∈ vars(C) . |γI(b(X))| = ℵ0,

ovvero se non sono verificate le condizioni del teorema 5.4.1, altrimentiwaltz (b, C) e la bounding box risultato dell’esecuzione (finita) dell’algoritmodi figura 5.5 su b e C.

Alcuni risultati circa l’algoritmo che abbiamo appena presentato sarannoutili nel seguito.

Proposizione 5.4.1 Risulta ∀C ⊆f Ca,

waltz (⊥B, C) = ⊥B.

Dim. Basta osservare l’algoritmo di figura 5.5 (in particolare le linee 2, 3 e9 della funzione waltz ).

1Non e pero detto che, cosı facendo, le proprieta dell’algoritmo che ci serviranno nelseguito restino tutte valide.

2Di fatto in ogni sistema “reale” questa misura sara applicata automaticamente, essendola soglia fissata dalla precisione dei numeri di macchina.

86

Proposizione 5.4.2 Per ogni insieme di vincoli C ⊆f Ca, se ∀X ∈ vars(C)dX ⊆f Z e il dominio di X, allora, posto

b =

[αI(dX)]X

∣∣∣ X ∈ vars(C),

si ha θ | FD |=

∨c∈C

cθ ⊆ γB(waltz (b, C)).

Dim. E semplicemente la correttezza dell’algoritmo di Waltz, che discendeda quella di refine.

Proposizione 5.4.3 Per ogni b1, b2 ∈ B e per ogni C1, C2 ⊆f Ca risulta

waltz (waltz (b1, C1)⊗B b2, C1 ∪ C2) = waltz (waltz (b2, C2)⊗B b1, C1 ∪ C2)

= waltz (b1 ⊗B b2, C1 ∪ C2).

Dim. Questo risultato rappresenta l’incrementalita dell’algoritmo di figu-ra 5.5. Questo comportamento e dovuto al fatto che, ogniqualvolta l’interval-lo associato ad una variabile viene ristretto, tutti i vincoli su quella variabilevengono reinseriti in coda e quindi riesaminati. Inoltre l’algoritmo procedefinche non e piu possibile restringere alcun intervallo. Cio implica che labounding box restituita da waltz dipende solo dalla bounding box iniziale edall’insieme di vincoli e non dall’ordine in cui i vincoli vengono considerati.

In termini algoritmici la scrittura

waltz (waltz (b, C1), C1 ∪ C2)

significa iterare il raffinamento dapprima solo sui vincoli in C1, fino allaquiescenza, poi considerando anche quelli in C2, di nuovo fino alla quiescenza.Cio equivale a raffinare gli intervalli delle variabili finquando possibile usandoindifferentemente i vincoli in C1 o in C2, per cui

waltz (waltz (b, C1), C1 ∪ C2) = waltz (b, C1 ∪ C2).

La tesi della proposizione e una semplice generalizzazione di questo fatto.

Per la formalizzazione dell’analisi di CLP(FD) basata sulle boundingbox abbiamo bisogno di un ultimo risultato. In termini intuitivi, puo es-sere esposto in questo modo: dal punto di vista delle deduzioni effettuatedall’algoritmo di Waltz il vincolo t = t′ e equivalente alla coppia di vincolit = X,X = t′, a patto che X non compaia ne in t ne in t′ e l’intervallo di

87

[xl, xu] + [yl, yu] ≡ [(xl + yl), (xu + yu)]

[xl, xu]− [yl, yu] ≡ [(xl − yu), (xu − yl)]−[xl, xu] ≡ [−xu,−xl]

[xl, xu] ∗ [yl, yu] ≡ [min(xl ∗ yl, xl ∗ yu, xu ∗ yl, xu ∗ yu),max(xl ∗ yl, xl ∗ yu, xu ∗ yl, xu ∗ yu)]

Figura 5.7: Assiomi per il calcolo degli intervalli di variazione

X non vincoli ulteriormente i valori che le espressioni t e t′ possono assumere.Questa condizione si puo imporre assumendo che l’intervallo iniziale per Xcontenga gli intervalli di variazione di t e t′. Gli intervalli di variazione perun’espressione si possono ottenere mediante il calcolo degli intervalli, i cuiassiomi sono riportati in figura 5.7. Denoteremo l’intervallo di variazione diun’espressione t con int(t).

Proposizione 5.4.4 Date due espressioni t e t′ di CLP(FD), se X e unavariabile che non compare ne in t ne in t′ e bX e una bounding box [i]Xtale che

int(t) ∩ int(t′) ⊆ γI(i),

allora, se risultawaltz (b0, norm(t = t′)) = b,

si ha anche

waltz (b0 ⊕B bX , norm(t = X), norm(X = t′)) = b ∪ [i′]X.

Dim. Discende dalla definizione di refine.

88

5.5 Astrazione dell’algebra dei vincoli

Ora che abbiamo risolto il problema di determinare una bounding box da-to un insieme di vincoli, possiamo procedere alla definizione del sistema divincoli che costituisce la base della nostra interpretazione astratta. In pri-ma istanza potremmo pensare di utilizzare come universo dei vincoli l’in-sieme B delle bounding box. In tal caso dovremmo modellare l’operazionedi congiunzione di due vincoli ricavando le rispettive bounding box, e poieffettuandone l’intersezione per mezzo dell’operatore “⊗B” della sezione 5.3.Purtroppo pero questo approccio e poco produttivo, nel senso che non sfruttala potenzialita dell’algoritmo di Waltz. Si consideri la congiunzione di vincoli

X + Y = Z ∧ Y ≤ Z,

con i domini delle variabili approssimati dalla bounding box iniziale

b0 = [1, 10]X , [3, 8]Y , [2, 7]Z,

Le astrazioni del primo e secondo vincolo sarebbero, ripettivamente,

waltz (b0, X + Y = Z) = [1, 4]X , [3, 8]Y , [4, 7]Z

ewaltz (b0, Y ≤ Z) = [1, 10]X , [3, 7]Y , [3, 7]Z,

che, intersecate, danno

[1, 4]X , [3, 7]Y , [3, 7]Z.

Ma, ricordando l’esempio 5.4.2, si ha

waltz (b0, X + Y = Z, Y ≤ Z) = [3, 4]X , [3, 4]Y , [6, 7]Z,

ovvero una bounding box risultante che approssima in modo nettamente mi-gliore l’insieme delle soluzioni della congiunzione dei due vincoli. Un’altrapossibilita sarebbe quella di invocare l’algoritmo di Waltz sul secondo vin-colo sfruttando la bounding box ottenuta dal primo vincolo. L’operazionedi congiunzione non sarebbe commutativa, ma cio non costituirebbe proble-ma, poiche l’operazione astratta di congiunzione non deve necessariamenteesserlo. Il fatto e che comunque otterremmo approssimazioni piu grossolane,rispetto a quelle che possiamo ottenere con l’algoritmo di Waltz operando suentrambi i vincoli.

Le nostre astrazioni dei vincoli saranno percio costituite da una boun-ding box e da un vincolo (in realta da un insieme di vincoli), che chiameremo

89

residuo. Nell’esempio di cui sopra il vincolo X ≥ Y sara mantenuto come re-siduo fintanto che l’astrazione dei vincoli di dominio non consenta di dedurneinformazioni. Questo accorgimento permette di sfruttare appieno l’incremen-talita dell’algoritmo di Waltz. Il vincolo residuo rappresenta infatti una retedi vincoli che, eventualmente, sara incrementata con l’aggiunta di altri vin-coli. La disgiunzione di due vincoli astratti sara invece trattata calcolandol’unione convessa delle relative bounding box, e trattenendo come vincoloresiduo l’intersezione dei due residui originari. Gli operatori di quantificazio-ne esistenziale effettuano la proiezione delle bounding box e l’eliminazionedi vincoli dai residui. Gli elementi diagonali sono, semplicemente, i vincolidi uguaglianza. Si rammenti che, in base a quanto detto nella sezione 5.4.5,tutti i vincoli si considerano normalizzati.

5.5.1 Vincoli residui

Definiamo ora l’insieme dei vincoli residui, che, insieme alle bounding box,ci permetteranno di definire i vincoli astratti. Si rammenti che Ca e l’insiemedei vincoli atomici (normalizzati) di CLP(FD).

Definizione 5.5.1 L’insieme dei “vincoli residui” e

R = ℘f (Ca) ∪ Ca.

Proposizione 5.5.1 (R,⊇) e un cpo.

Dim. Chiaramente per ogni R ∈ R risulta Ca ⊇ R, e quindi Ca e l’elementominimo di R. Inoltre, l’estremo superiore di ogni catena di elementi di R

R1 ⊇ · · · ⊇ Rn ⊇ · · ·

esiste in R ed e dato da⋂iRi.

L’elemento Ca di R va considerato come un simbolo. In quanto seguesi sfruttano soltanto le sue proprieta rispetto alle operazioni insiemistiche,semplificando cosı la presentazione.

Proposizione 5.5.2 L’algebra dei residui

R = (R,∪,∩, ∅, Ca)

e un reticolo limitato.

90

Dim. E chiaro cheR e chiuso rispetto alle operazioni di unione e intersezioneinsiemistica. Tali operazioni soddisfano notoriamente le leggi commutative,associative, di idempotenza e di assorbimento. Inoltre Ca e un annichilatoreper l’unione, cosı come ∅ lo e per l’intersezione.

Si osservi che gli insiemi di vincoli (i residui) in R, sono da considerarsi,dal punto di vista delle soluzioni, come congiunzioni. Se R ∈ R denoteremol’insieme di FD-valutazioni

Sol(∨c∈R

c)

con Sol(R). Definiamo ora una prima approssimazione di quello che risulteraessere l’universo del nostro sistema di vincoli astratto.

Definizione 5.5.2 E definito l’insieme

D = B ×R.

Siano poi σ1:D → B e σ2:D → R i selettori cosı definiti, ∀〈b, R〉 ∈ D:

σ1(〈b, R〉) = b,

σ2(〈b, R〉) = R.

Indicheremo inoltre, per ogni elemento d di D,

σ1(d) con dB e

σ2(d) con dR.

91

Il seguente (facile) risultato preliminare sara immediatamente utile nelseguito.

Proposizione 5.5.3 L’algebra

D = (D,⊗D,⊕D,>D,⊥D)

dove, ∀d1, d2 ∈ D,

d1 ⊗D d2 = 〈dB1 ⊗B dB2 , dR1 ∪ dR2 〉,d1 ⊕D d2 = 〈dB1 ⊕B dB2 , dR1 ∩ dR2 〉,

>D = 〈>B, ∅〉,⊥D = 〈⊥B, Ca〉.

e un reticolo limitato.

Dim. E il prodotto diretto di due reticoli limitati.

5.5.2 Vincoli approssimati

Siamo ora in posizione tale da poter introdurre l’algebra astratta che modellala congiunzione e disgiunzione di vincoli di CLP(FD). Il carrier di quest’al-gebra e costituito dagli elementi di D dai quali l’algoritmo di Waltz non e ingrado di dedurre piu nulla.

Definizione 5.5.3 E definita l’algebra

D = (D, ⊗D,⊕D,>D,⊥D),

doveD = 〈b, C〉 ∈ D | waltz (b, C) = b ,

e, ∀d1, d2 ∈ D,

d1 ⊗D d2 = 〈waltz (dB1 ⊗B dB2 , dR1 ∪ dR2 ), dR1 ∪ dR2 〉,d1 ⊕D d2 = 〈dB1 ⊕B dB2 , dR1 ∩ dR2 〉,

>D = 〈>B, ∅〉,⊥D = 〈⊥B, Ca〉.

Teorema 5.5.1 D e un semianello chiuso non distributivo.

92

Dim. Il fatto che (D,⊕D,⊥D) sia un monoide idempotente e commutativodiscende immediatamente dalla proposizione 5.5.3. Bisogna ora mostrare che(D, ⊗D,>D) e un monoide. Per l’associativita risulta

d1 ⊗D (d2 ⊗D d3) = 〈dB1 , dR1 〉 ⊗D 〈waltz (dB2 ⊗B dB3 , dR2 ∪ dR3 ), dR2 ∪ dR3 〉[def. 5.5.3] = 〈waltz (dB1 ⊗B waltz (dB2 ⊗B dB3 , dR2 ∪ dR3 ), dR1 ∪ (dR2 ∪ dR3 )),

dR1 ∪ (dR2 ∪ dR3 )〉[prop. 5.4.3] = 〈waltz (waltz (dB1 ⊗B dB2 , dR1 ∪ dR2 )⊗B dB3 , (dR1 ∪ dR2 ) ∪ dR3 ),

(dR1 ∪ dR2 ) ∪ dR3 〉[def. 5.5.3] = 〈waltz (dB1 ⊗B dB2 , dR1 ∪ dR2 ), dR1 ∪ dR2 〉 ⊗D 〈dB3 , dR3 〉[def. 5.5.3] = (d1 ⊗D d2) ⊗D d3.

Inoltre >D e l’identita per “⊗D”, infatti

d ⊗D >D = 〈dB, dR〉 ⊗D 〈>B, ∅〉[def. 5.5.3] = 〈waltz (dB ⊗B >B, dR ∪ ∅), dR ∪ ∅〉

[propp. 5.3.4 e 5.5.2] = 〈waltz (dB, dR), dR〉[def. 5.5.3] = 〈dB, dR〉

= d.

Inoltre

d ⊗D ⊥D = 〈dB, dR〉 ⊗D 〈⊥B, Ca〉[def. 5.5.3] = 〈waltz (dB ⊗B ⊥B, dR ∪ Ca), dR ∪ Ca〉

[propp. 5.3.4 e 5.5.2] = 〈waltz (⊥B, Ca), Ca〉[prop. 5.4.3] = 〈⊥B, Ca〉

= ⊥D,

e dunque ⊥D e un annichilatore per “⊗D”.Sia ora (di)i∈N una successione di elementi di D, allora⊕

i∈N

Ddi = 〈

⊕i∈N

BdBi ,⋂i∈N

dRi 〉

= 〈supB dBi | i ∈ N , supR dRi | i ∈ N 〉= supD di | i ∈ N .

Le equazioni hanno senso, poiche B e, per le proposizioni 5.3.3 e 5.3.4, unreticolo completo. Inoltre, per la proposizione 5.5.1, R e un cpo. Per con-cludere, osserviamo che D non e distributivo per il fatto, gia visto nella nota5.2.1, che l’intersezione non distribuisce sull’unione convessa.

93

Definiamo ora gli operatori astratti di quantificazione esistenziale. Questioperatori non fanno altro che rilasciare le bounding box ed eliminare vincolidai residui, e precisamente quelli che coinvolgono le variabili che si vogliono“nascondere”.

Definizione 5.5.4 La famiglia di operatori astratti di quantificazione esi-stenziale ∃]∆ e cosı definita, ∀∆ ⊆ Vars e ∀b ∈ B, b 6= ⊥B:

∃]∆〈⊥B, R〉 = 〈⊥B, r〉,∃]∆〈b, R〉 = 〈b′, R′〉,

dove

b′ = b \ [b(X)]X | X ∈ ∆ ,R′ = r ∈ R | r ind ∆ .

Veniamo ora agli elementi diagonali dell’algebra che, nel nostro caso sonole astrazioni dei vincoli di uguaglianza.

Definizione 5.5.5 Per ogni t, t′ ∈ Υst e definito l’elemento d]t,t′ ∈ D taleche, posto

c = norm(t = t′),

b =

[αI(dX)]X

∣∣∣ X ∈ vars(c),

risultad]t,t′ = 〈waltz (b, c), c〉.

Teorema 5.5.2 La struttura algebrica

A] =(D, ⊗D,⊕D,>D,⊥D,∃]∆, d

]t,t′

)∆⊆Vars; t,t′∈Υ

,

e un sistema di vincoli non distributivo.

Dim. Abbiamo gia mostrato che (D, ⊗D,⊕D,>D,⊥D) e un semianellochiuso non distributivo. Inoltre, per la definizione 5.5.4, si ha, ∀∆ ⊆ Vars ,

∃]∆ = ⊥D.

Per la stessa definizione si ha che, se ∃]∆〈b, C〉 = 〈b′, C ′〉, allora b ≤B b′ eC ′ ⊆ C. Percio risulta

〈b, C〉 ⊕D ∃]∆〈b, C〉 = 〈b, C〉 ⊕D 〈b′, C ′〉= 〈b⊕B b′, C ∩ C ′〉= 〈b′, C ′〉= ∃]∆〈b, C〉.

94

-

6

X

Y

0

r r

rrr

r

rr rrr rrrr

r

rr

-

6

X

Y

0

r r

rrr

r

rr rrr rrrr

r

rr

Figura 5.8: Congiunzione di vincoli astratti

Gli assiomi C3, C4 e C5 della definizione 3.1.6 valgono banalmente per leproprieta delle operazioni insiemistiche. L’assioma D1 vale in modo vacuo,poiche il procedimento di normalizzazione rimpiazza ogni vingolo del tipot = t con true. Infine l’assioma D2 vale per la proposizione 5.4.4 con leconsiderazioni ivi svolte.

In figura 5.8 e visualizzata l’operazione di congiunzione “⊗D” sui vincoliastratti. Nel grafico di sinistra sono mostrate le bounding box degli operandi.In quello di destra, i rettangoli con linee piu spesse rappresentano: quellopiu esterno, la bounding box intersezione, quello piu interno la bounding boxminima per i punti che stanno nell’intersezione. Il rettangolo intermedio conlinee tratteggiate rappresenta la bounding box risultato della congiunzione,ovvero quella derivata dall’algortimo di Waltz a partire dalla bounding boxintersezione, sfruttando i vincoli nei residui degli operandi.

I sistemi di vincoli che abbiamo introdotto, quello standard (o concreto)Ast , e quello approssimato (o astratto) A], non sono compatibili. Infatti Ast

e distributivo, mentre A] non lo e. Cio significa che non puo esistere unmorfismo debole da Ast in A]. Dobbiamo dunque dimostrare la correttezzadella nostra interpretazione in altro modo.

Per fare questo iniziamo con l’esplicitare il morfismo di interpretazione,che sappiamo esistere ed essere unico, dall’algebra di vincoli Λ(Υst ,ΠC) inA].Si ricordi che se X ∈ Vars allora dX ⊆f Z e il dominio di X.

Definizione 5.5.6 Il morfismo m: Λ(Υ,ΠC)→ A] e definito induttivamentecome segue. Per le basi di induzione si considerano innanzitutto i vincolicostanti, ponendo

m(true) = 〈>B, ∅〉,m(false) = 〈⊥B, Ca〉.

95

Vengono poi i vincoli atomici dove, ∀c ∈ Ca, posto

b =

[αI(dX)]X

∣∣∣ X ∈ vars(c),

risultam(c) = 〈waltz (b, c), c〉.

Tra i vincoli atomici vi sono ovviamente anche quelli ottenuti dai vincolidi uguaglianza usati per il passaggio dei parametri, ovvero i vincoli del tiponorm(t = t′) con t, t′ ∈ Υst . Ora i passi induttivi: per quanto riguarda lacongiunzione e disgiunzione di vincoli, ∀c1, c2 ∈ Λ(Υ,ΠC), se

d1 = 〈dB1 , dR1 〉 = m(c1),

d2 = 〈dB2 , dR2 〉 = m(c2),

allora, rispettivamente,

m(c1 ∧ c2) = d1 ⊗D d2 = 〈waltz (dB1 ⊗B dB2 , dR1 ∪ dR2 ), dR1 ∪ dR2 〉,

em(c1 ∨ c2) = d1 ⊕D d2 = 〈dB1 ⊕B dB2 , dR1 ∩ dR2 〉.

Infine, per la quantificazione esistenziale, ∀∆ ⊆ Vars e ∀c ∈ Λ(Υ,ΠC):

m(∃∆c) = ∃]∆m(c)

Nel seguito indicheremo σ1m con mB, e σ2m con mR. Con tale notazionepossiamo introdurre due espressioni per m(c1 ∧ c2) e m(c1 ∨ c2) equivalenti aquelle date nella definizione 5.5.6:

m(c1 ∧ c2) = 〈waltz (mB(c1)⊗B mB(c2),mR(c1) ∪mR(c2)),

mR(c1) ∪mR(c2)〉,m(c1 ∨ c2) = 〈mB(c1)⊕B mB(c2),mR(c1) ∩mR(c2)〉.

Il seguente risultato stabilisce che il vincolo residuo dell’astrazione e,rispetto alle soluzioni, un approssimazione corretta del vincolo “concreto”.

Lemma 5.5.1 Per ogni c ∈ Λ(Υ,ΠC) risulta

Sol(c) ⊆ Sol(mR(c)).

96

Dim. Per induzione strutturale. Per quanto riguarda le costanti true efalse si ha

Sol(true) = Θ

= Sol(∅)= Sol(mR(true)),

e

Sol(false) = ∅= Sol(Ca)= Sol(mR(false)).

Per i vincoli atomici c ∈ Ca risulta, banalmente,

Sol(c) = Sol(mR(c)).

Per i passi induttivi, assumendo che

Sol(c1) ⊆ Sol(mR(c1)),

Sol(c2) ⊆ Sol(mR(c2)),

risulta

Sol(c1 ∧ c2) = Sol(c1) ∩ Sol(c2)

[ip. induttiva] ⊆ Sol(mR(c1)) ∩ Sol(mR(c2))

[def. di Sol ] = Sol(mR(c1) ∪mR(c2))

[def. 5.5.6] = Sol(mR(c1 ∧ c2)),

per la congiunzione, mentre per la disgiunzione si ha

Sol(c1 ∨ c2) = Sol(c1) ∪ Sol(c2)

[ip. induttiva] ⊆ Sol(mR(c1)) ∪ Sol(mR(c2))

[def. di Sol ] ⊆ Sol(mR(c1) ∩mR(c2))

[def. 5.5.6] = Sol(mR(c1 ∨ c2)).

Infine, per la quantificazione esistenziale, se ∆ ⊆ Vars e c ∈ Λ(Υ,ΠC), siac′ il vincolo ottenuto rimpiazzando tutti i vincoli atomici in c in cui occorrealmeno una variabile in ∆ con true. Chiaramente risulta Sol(c′) ⊇ Sol(∃∆c),ma allora

Sol(∃∆c) ⊆ Sol(c′)

[ip. induttiva] ⊆ Sol(mR(c′))

[def. 5.5.4] = Sol(∃]∆mR(c))

[def. 5.5.6] = Sol(mR(∃∆c)).

97

Il seguente risultato fondamentale stabilisce che la nostra interpreta-zione e corretta. Ovvero che la bounding box ottenuta dal procedimen-to di astrazione e un’approssimazione corretta delle soluzioni del vincolo“concreto”.

Teorema 5.5.3 Per ogni c ∈ Λ(Υ,ΠC) risulta

Sol(c) ⊆ γB(mB(c)).

Dim. Per induzione strutturale. Per i vincoli costanti, true e false, risulta

Sol(true) = Θ

= γB(>B)

= γB(mB(true)),

e

Sol(false) = ∅= γB(⊥B)

= γB(mB(false)).

Per i vincoli atomici c ∈ Ca, per la definizione 5.5.6 e la proposizione 5.4.2,si ha immediatamente

Sol(c) ⊆ γB(mB(c)).

Ora i passi induttivi: siano c1, c2 ∈ Λ(Υ,ΠC) tali che

Sol(c1) ⊆ γB(mB(c1)),

Sol(c2) ⊆ γB(mB(c2)),

allora per la congiunzione risulta

Sol(c1 ∧ c2) = Sol(c1) ∩ Sol(c2)

[ip. ind. e lemma 5.5.1] ⊆ γB(mB(c1)) ∩ Sol(mR(c1)) ∩ γB(mB(c2)) ∩ Sol(mR(c2))

[def. di Sol e prop. 5.3.5] = γB(mB(c1)⊗B mB(c2)) ∩ Sol(mR(c1) ∪mR(c2))

[prop. 5.4.2] ⊆ γB(waltz (mB(c1)⊗B mB(c2),mR(c1) ∪mR(c2)))

[def. 5.5.6] = γB(mB(c1 ∧ c2)),

98

mentre per la disgiunzione si ha

Sol(c1 ∨ c2) = Sol(c1) ∪ Sol(c2)

[ip. induttiva] ⊆ γB(mB(c1)) ∪ γB(mB(c2))

[prop. 5.3.5] ⊆ γB(mB(c1)⊕B mB(c2))

[def. 5.5.6] = γB(mB(c1 ∨ c2)).

Infine, per la quantificazione esistenziale, si ragiona in modo analogo a quellodella dimostrazione del lemma 5.5.1.

Sia ora P = C1, . . . , Cm un programma CLP(FD). Il programma corri-spondente, P ′, sul sistema di vincoli A] e un insieme di clausole C ′1, . . . , C ′mtale che, ∀i = 1, . . . ,m, se

Ci = p(t) :− c p1(t1), . . . , pn(tn),

alloraC ′, i = p(t) :− m(c) p1(t1), . . . , pn(tn).

Definiamo ora la semantica bottom-up approssimata, ovvero quella che ciconsente di completare la definizione della nostra analisi globale di CLP(FD).L’operatore delle conseguenze immediate TA

]

P ′ e definito come nella sezione3.2.2, con l’unica differenza che alle variabili di ridenominazione, introdotte(e subito nascoste) nella definizione 3.2.9, deve essere assegnato un dominioiniziale opportuno, come discusso nella proposizione 5.4.4. Dal momento cheil sistema di vincoli A] e Noetheriano esistera un k ∈ N tale che

FA](P ′) = TA]

P ′ ↑ k,

dal che discende la finitezza dell’analisi. La correttezza e invece una sem-plice conseguenza del teorema 5.5.3. Indichiamo con A il sistema di vincolistandard di CLP(FD), definito come nell’esempio 3.1.4.

Corollario 5.5.1 Per ogni n ∈ N, se

p(X) :− c ∈ TAP ↑ n,

allorap(X) :− m(c) ∈ TA

]

P ′ ↑ n,

e risultaSol(c) ⊆ γB(mB(c)).

99

Dim. Si dimostra facilmente per induzione: sia il caso base n = 1, dove siconsiderano solo clausole unitarie, che il passo di induzione sono conseguenzedella definizione 3.2.9 e del teorema 5.5.3.

In definitiva si ha che, per ogni atomo vincolato

p(X) :− c in FA(P ),

esiste un atomo vincolato

p(X) :− mB(c) in FA](P ′),

tale cheSol(c) ⊆ γB(mB(c)).

5.6 Un esempio

Dal momento che l’analisi presentata e per un linguaggio CLP su dominifiniti ci si aspetterebbe che il classico problema delle 8 regine fosse portatoad esempio. Purtroppo pero le soluzioni di questo problema sono “sparse”,non ha cioe senso ragionare in termini di intervalli di variazione per le solu-zioni. Non solo, ma, come si e visto nella trattazione precedente, i vincoli delproblema delle 8 regine, che sono tutti di differenza, non sono utilizzati perla derivazione delle bounding box.

Sui classici esempi dei vincoli di precedenza per il problema dello sche-duling la nostra analisi si comporta invece molto bene, come e logico aspet-tarsi. Le tipiche clausole che li definiscono sono pero unitarie, e dunque nonsi tratta di esempi significativi. Vediamo invece un programma CLP(FD)che contiene una clausola doppiamente ricorsiva, adattata dalla funzione 91di McCarthy. Consideriamo dunque il seguente programma CLP(FD), P :

mc(N,M) :− domain(N, [0, 200]), domain(M, [0, 200]),

N > 100, M = N − 10.

mc(N,M) :− domain(N, [0, 200]), domain(M, [0, 200]),

N ≤ 100, T = N + 11 mc(T, U), mc(U,M).

Il predicato mc/2 esprime la relazione

(n, 91) | 0 ≤ n ≤ 101 ∪ (n, n− 10) | 101 < n ≤ 200 .

100

L’analisi bottom-up presentata in questo capitolo consente di dedurre, pro-gressivamente, le seguenti bounding box per mc/2:

[101, 200]X , [91, 190]Y in TA]

P ′ ↑ 0,

[100, 200]X , [91, 190]Y in TA]

P ′ ↑ 1,

[99, 200]X , [91, 190]Y in TA]

P ′ ↑ 2,...

...

[0, 200]X , [91, 190]Y in TA]

P ′ ↑ 101.

They are queensReckless

Blasting forthInsatiable

They need moreEver moreDimension

To conquerWhen they stop

PantingThey rest

Like drowsy cows

— R. de L. FURTADO, “Locomotives”, in The Centre (1955)

101

Capitolo 6

Conclusioni

In questa tesi abbiamo affrontato il problema dell’analisi globale di lin-guaggi logici con vincoli studiandone l’applicabilita a particolari casi con-creti. Le considerazioni che si possono trarre da questo lavoro forniscono unamigliore comprensione degli strumenti semantici necessari per formalizzarel’interpretazione astratta di CLP.

Un aspetto peculiare della tesi e l’integrazione di tecniche di deduzioneapprossimata, note nel campo dell’intelligenza artificiale, con uno schemaadeguato alla definizione di semantiche non standard di CLP. Questa inte-grazione si e dimostrata particolarmente appropriata per l’interpretazioneastratta di programmi logici con vincoli.

Sfruttando la generalita e la relativa efficienza degli algoritmi, noti in AI,di propagazione di vincoli e uno schema algebrico opportuno, siamo riusciti acongiungere la formalizzazione teorica dell’analisi in termini di interpretazio-ne astratta con la possibilita concreta di una sua efficiente implementazione.

In questa tesi abbiamo definito una semantica non standard per un lin-guaggio logico con vincoli su domini numerici finiti (CLP(FD)). La partico-lare analisi cosı ottenuta consente di ottenere delle approssimazioni “quan-titative” dell’insieme di successo dei programmi. Le informazioni ricavateda tale analisi sono direttamente impiegabili nel processo di compilazione,riducendo il costo del controllo di soddisfacibilita dei vincoli.

Nella semantica non standard che abbiamo definito, le soluzioni dei vin-coli di CLP(FD) sono approssimate “spazialmente” per mezzo di regionirettangolari dette bounding box . Intuitivamente le soluzioni di un vincolosu n variabili rappresenta una certa “sagoma” in uno spazio n-dimensionale.Questa sagoma puo essere approssimata con un parallelepipedo con i lati pa-ralleli agli assi (bounding box) che la contenga. Le bounding box sono formemolto semplici di approssimazione spaziale: sono facilmente memorizzabili emanipolabili.

102

La presente tesi ha inoltre permesso di osservare come alcune restrizio-ni (quali la distributivita degli operatori fondamentali di composizione deivincoli), introdotte in un sistema di vincoli appositamente studiato per l’in-terpretazione astratta di programmi CLP in [27, 28], fossero eccessive peralcune classi di analisi. Il rilasciamento di queste condizioni non pregiudicala sussistenza di alcune importanti proprieta (quali la monotonia dell’opera-tore astratto delle conseguenze immediate) della semantica utili nell’analisi.Questo approccio ha comunque evidenziato come le condizioni piu restrittiveintrodotte in [27] siano invece necessarie per assicurare la validita di altririsultati semantici standard quali l’equivalenza tra il modello operazionale equello di punto fisso associato al programma da analizzare.

In conclusione possiamo affermare che questo lavoro ha rafforzato l’ipo-tesi dalla quale ha avuto origine. E cioe che le tecniche di propagazione divincoli possano rivestire una certa importanza nel campo dell’analisi staticadei linguaggi CLP. L’approccio seguito in questa tesi si puo estendere a classidi analisi diverse da quella qui presentata. Una conferma di cio si e avutarecentemente con lo studio di uno schema di interpretazione astratta miratoalla deduzione della consistenza, inconsistenza e ridondanza di vincoli [4].Queste ottimizzazioni sono utili per guidare alcune importanti ottimizzazio-ni nel processo di compilazione. Una di queste ottimizzazioni, che riguardal’eliminazione dei vincoli ridondanti, consente un sorprendente aumento diefficienza nell’esecuzione di programmi CLP(<) [35]. L’analisi studiata in[4] si basa, per formalizzare l’interpretazione astratta, sullo stesso schemaalgebrico usato in questa tesi. La tecnica di inferenza utilizzata e, anche qui,quella di propagazione di vincoli nella sua versione di inferenza di vincoli ,cosı come e stata accennata nella sezione 5.4.3.

103

Bibliografia

[1] A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis ofComputer Algorithms. Addison Wesley Publishing Company, 1974.

[2] G. Alefeld and J. Herzberger. Introduction to Interval Computation.Academic Press, New York, 1983.

[3] J. F. Allen. Maintaining Knowledge About Temporal Intervals.Commun. of the ACM, 26(11):832–843, 1983.

[4] R. Bagnara, R. Giacobazzi, and G. Levi. Static analysis of CLP pro-grams over numeric domains. In M. Billaud, P. Casteran, MM. Corsini,K. Musumbu, and A. Rauzy, editors, Actes “Workshop on Static Ana-lysis ’92”, volume 81–82 of Bigre, pages 43–50, Bordeaux, September1992. Extended abstract.

[5] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework forSemantics-based Bottom-up Abstract Interpretation of Logic Programs.Technical Report TR 12/91, Dipartimento di Informatica, Universita diPisa, 1991. To appear in ACM Transactions on Programming Languagesand Systems.

[6] R. Barbuti and A. Martelli. A Structured Approach to SemanticsCorrectness. ”Science of Computer Programming”, 3:279–311, 1983.

[7] G. Birkhoff. Lattice Theory. In AMS Colloquium Publication, third ed.,1967.

[8] W. W. Bledsoe. The Sup-Inf Method in Presburger Arithmetic. MemoATP-18, Math. Dept., University of Texas at Austin, Austin, 1974.

[9] W. W. Bledsoe, R. S. Boyer, and W. H. Henneman. Computer Proofsof Limit Theorems. Artificial Intelligence, 3:27–60, 1972.

[10] S. Burris and H. P. Sankappanavar. A Course in Universal Algebra.Springer-Verlag, Berlin, 1981.

104

[11] J. Cirulis. An Algebraization of First Order Logic with Terms. ColloquiaMathematica Societatis Janos Bolyai, 54, 1991.

[12] P. Codognet and G. File. Computations, Abstractions and Constraints.Technical Report 13, Dipartimento di Matematica Pura e Applicata,Universita di Padova, Italy, 1991.

[13] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lat-tice Model for Static Analysis of Programs by Construction or Ap-proximation of Fixpoints. In Proc. Fourth ACM Symp. Principles ofProgramming Languages, pages 238–252, 1977.

[14] P. Cousot and R. Cousot. A constructive characterization of the latti-ces of all retracts. pre-closure, quasi-closure and closure operators on acomplete lattice. Portugaliæ Mathematica, 38(2):185–198, 1979.

[15] P. Cousot and R. Cousot. Systematic Design of Program AnalysisFrameworks. In Proc. Sixth ACM Symp. Principles of ProgrammingLanguages, pages 269–282, 1979.

[16] P. Cousot and N. Halbwachs. Automatic Discovery of Linear RestraintsAmong Variables of a Program. In Proc. Fifth ACM Symp. Principlesof Programming Languages, pages 84–96, 1978.

[17] G. B. Dantzig and B. C. Eaves. Fourier-Motzkin Elimination and itsDual. Journal of Combinatorial Theory (A), 14:288–297, 1973.

[18] E. Davis. Representing and Acquiring Geographic Knowledge. TechnicalReport 292, Yale University, New Haven, CT, 1984.

[19] E. Davis. Constraint Propagation with Interval Labels. ArtificialIntelligence, 32:281–331, 1987.

[20] R. Davis. Diagnosis via Casual Reasoning: Path of Interaction and theLocality Principle. In Proc. AAAI-83, pages 88–92, 1983.

[21] S. Debray and R. Ramakrishnan. Generalized Horn Clause Programs.Technical report, Dept. of Computer Science, The University of Arizona,1991.

[22] S.K. Debray and N.W. Lin. Automatic Complexity Analysis of LogicPrograms. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on LogicProgramming, pages 599–613. The MIT Press, Cambridge, Mass., 1991.

105

[23] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification I.EATCS Series. Springer-Verlag, Berlin, 1985.

[24] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. DeclarativeModeling of the Operational Behavior of Logic Languages. TheoreticalComputer Science, 69(3):289–318, 1989.

[25] E. C. Freuder. Synthesizing Constraint Expressions. Commun. of theACM, 21(11):958–966, 1978.

[26] M. Gabbrielli and G. Levi. Modeling Answer Constraints in ConstraintLogic Programs. In K. Furukawa, editor, Proc. Eighth Int’l Conf. onLogic Programming, pages 238– 252. The MIT Press, Cambridge, Mass.,1991.

[27] R. Giacobazzi, S. Debray, and G. Levi. A Generalized Semantics for Con-straint Logic Programs. In Proceedings of the International Conferenceon Fifth Generation Computer Systems 1992, 1992.

[28] R. Giacobazzi, S. K. Debray, and G. Levi. Generalized Semanticsand Abstract Interpretation for Constraint Logic Programs. Techni-cal report, Dipartimento di Informatica, Universita di Pisa, 1992. Inpreparation.

[29] A. C. Hearn. Reduce 2: A System and Language for Algebraic Ma-nipulation. In Proceedings of the Second Symposium on Symbolic andAlgebraic Manipulation, pages 128–133. ACM, 1971.

[30] R. Helm, K. Marriot, and M. Odersky. Spatial Query Optimization:from Boolean Constraints to Range Queries. Technical Report RC17231, IBM Research Division, T. J. Watson Research Center, YorktownHeights, 1991.

[31] L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I andII. North-Holland, Amsterdam, 1971.

[32] H. Herrlich and M. Husek. Galois Connections. In A. Melton, editor,Mathematical Foundation of Program Semantics, volume 239 of Lectu-re Notes in Computer Science, pages 122–134. Springer-Verlag, Berlin,1985.

[33] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. InProc. Fourteenth Annual ACM Symp. on Principles of ProgrammingLanguages, pages 111–119. ACM, 1987.

106

[34] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. Technicalreport, Department of Computer Science, Monash University, June 1986.

[35] N. Jørgensen, K. Marriot, and S. Michaylov. Some Global Compile-Time Optimizations for CLP(<). In Proc. 1991 Int’l Symposium onLogic Programming, pages 420–434, 1991.

[36] M. Karr. Affine Relationships Among Variables of a Program. ActaInformatica, 6:133–151, 1976.

[37] R. Kemp and G. Ringwood. An Algebraic Framework for the AbstractInterpretation of Logic Programs. In S. Debray and M. Hermenegildo,editors, Proc. North American Conf. on Logic Programming’90, pages506–520. The MIT Press, Cambridge, Mass., 1990.

[38] J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited.In J. Minker, editor, Foundations of Deductive Databases and LogicProgramming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

[39] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag,Berlin, 1987. Second edition.

[40] A. K. Mackworth. Consistency in Networks of Relations. ArtificialIntelligence, 8:99–118, 1977.

[41] A. K. Mackworth and E. C. Freuder. The Complexity of Some Po-lynomial Network Consistency Algorithms for Constraint SatisfactionProblems. Artificial Intelligence, 25:65–74, 1985.

[42] K. Marriott and H. Søndergaard. Bottom-up Abstract Interpretationof Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc.Fifth Int’l Conf. on Logic Programming, pages 733–748. The MIT Press,Cambridge, Mass., 1988.

[43] D. V. McDermott and E. Davis. Planning Routes Through UncertainTerritory. Artificial Intelligence, 22:107–156, 1984.

[44] A. Melton, D.A. Schmidt, and G.E. Strecker. Galois Connections andComputer Science Applications. In D. Pitt et al., editor, CategoryTheory and Computer Programming, volume 240 of Lecture Notes inComputer Science, pages 299–312. Springer-Verlag, Berlin, 1986.

[45] U. Montanari. Networks of Constraints: Fundamental Properties andApplications to Picture Processing. Inform. Sci., 7:95–132, 1974.

107

[46] U. Montanari and F. Rossi. Constraint Relaxation may be Perfect.Artificial Intelligence Journal, 48:143–170, 1991.

[47] S. Muchnick and N. Jones. Program Flow Analysis: Theory andApplications. Prentice-Hall, Englewood Cliffs, 1981.

[48] O. Ore. Galois Connections. In Trans. AMS, volume 55, pages 493–513,1944.

[49] Oystein Ore. Combinations of Closure Relations. Annals ofMathematics, 44(3):514–533, 1943.

[50] W. Pugh. The Omega Test: a Fast and Practical Integer ProgrammingAlgorithm for Dependence Analysis. In Supercomputing ’91, 1991. Toappear in Commun. of the ACM.

[51] W. Pugh and D. Wonnacott. Eliminating False Data Dependences Usingthe Omega Test. To appear at SIGPLAN PLDI ’92, 1992.

[52] V. A. Saraswat, M. Rinard, and P. Panangaden. Semantic foundation ofconcurrent constraint programming. In Proc. Eighteenth Annual ACMSymp. on Principles of Programming Languages. ACM, 1991.

[53] R. Shostak. On The Sup-Inf Method in for Proving Presburger Formulas.Journal of the ACM, 24(4):529–543, 1977.

[54] R. Simmons. Representing and Reasoning About Change in GeologicInterpretation. Technical Report 749, MIT AI Laboratory, 1983.

[55] R. Simmons. Commonsense Arithmetic Reasoning. In Proc. AAAI-86,pages 118–124, 1986.

[56] J. W. Thatcher, E. G. Wagner, and J. B. Wright. More on advice onstructuring compilers and proving them correct. Theoretical ComputerScience, 15:223–249, 1981.

[57] P. Van Hentenryck. Constraint Satisfaction in Logic Programming. LogicProgramming Series. The MIT Press, 1989.

[58] K. Verschaetse and D. De Schreye. Automatic Derivation of Linear SizeRelations. In Proc. of PLILP’92. Springer-Verlag, Berlin, 1992. Toappear.

[59] R. J. Waldinger and K. N. Levitt. Reasoning about Programs. AIJournal, 5:235–316, 1974.

108

[60] D. Waltz. Understanding Line Drawings of Scenes with Shadows. InP. Winston, editor, The Psychology of Computer Vision, chapter 2.McGraw-Hill, New York, 1975.

[61] M. Ward. The Closure Operators of a Lattice. Annals of Mathematics,43(2):191–196, 1942.

109