Interpretazione Astratta

[lordnergal]

Ciao a tutti,
qualcuno di voi riesce a darmi la soluzione di questo esercizio

Si consideri il linguaggio

E:: N | E/E | !(E)

dove N sono i naturali, / è la divisione tra naturali e ! è la funzione fattoriale.

1. Definire la semantica concreta;

2. Definire la semantica astratta quando si intende verificare se una espressione ha un valore uguale a 0, oppure uguale a 1 oppure una valore pari non nullo o un valore dispari;

3. Definire e dimostrare la correttezza locale di / e di ! ;

Mi interessa soprattutto il punto 2.
Grazie in anticipo.

[hamming_burst]

Ciao,
di solito in questo forum si cerca di presentare un abbozzo di soluzione, e insieme si cerca di chiarire i tuoi dubbi, non si chiede la soluzione completa

La semantica astratta e la semantica concreta le ho incontrate mentre studiavo un altro tipo di modello semantico (sem. denotazionale con operatore di punto fisso). Queste penso si basino su principi identici (utilizzeranno un tipo di dimostrazione differente), hai percaso delle slide a cui fai riferimento per studiarle, casomai vedo cosa si può fare.

[lordnergal]

Ciao,
hai ragione quello che mi interessa è capire l'esercizio, più che avere la soluzione.
Soprattutto vorrei capire il punto 2, perchè di solito gli esercizi che ho svolto richiedevano di definire la semantica astratta dei segni e non dei valori delle espressioni.
Questi sono gli appunti sulla semantica astratta : http://dl.dropbox.com/u/14152853/Interp ... tratta.pdf
E qui c'è un esercizio svolto: http://dl.dropbox.com/u/14152853/Esempi ... tratta.pdf

Grazie

[hamming_burst]

interessante
sì è come pensavo gli argomenti sono affini. Le strutture algebriche utilizzate si basano sui reticoli, invece quelli che ho utilizzato io si basano sui CPO (complete poset) con LUB. Informalmente la differenza è che nel tuo caso si tiene conto sia del LUB (lower upper bound) che del GLB (greatest lower bound) di un insieme, però vengono affrontati con altre proprietà con ho visto (i CPO con reticoli vengon definiti con teoremi di pre-punto fisso, in questo caso no).

Un'altra cosa che non conosco sono le "connessioni di Galois".

Non capisco perchè il codominio semantico è l'insieme della parti di \( \displaystyle \mathbb{Z} \). Non ha senso in questo contesto utilizzarlo, forse è per via della relazione di ordinamento (sub-set).

Per la dimostrazione di correttezza sembra utilizzare la continuità (o semplice monotonia) sulla funzione di interpretazione semantica (esiste qualcosa di simile anche nella sem. den.), ma qua è proposta con un approccio misto. Cioè usa un tipo di induzione che viene chiama "strutturale", ma secondo me non è corretto potrebbe essere l'induzione noetheriana che è simile (la vera induzione struttuale è tipo questa)

Darò meglio un'occhiata in un altro momento, se riescirò a darti qualche dritta; mi sembra molto interessante

[lordnergal]

si il dominio concreto è un reticolo completo sull'insieme delle parti di Z, con l'ordinamento parziale basato sull'inclusione insiemistica (P(\( \displaystyle \mathbb{Z} \)),\( \displaystyle \subseteq \) );
il domino astratto con il suo ordinamento (A, \( \displaystyle \le \)), è un reticolo completo definito nel seguente modo:

Come hai detto bene tu, si tiene conto del LUB e del GLB, usati per esprimere la funzione di astrazione e la funzione di concretizzazione.

La funzione di astrazione \( \displaystyle \alpha \) mappa un insieme X di valori concreti nel più preciso valore astratto che rappresenta X. Considera la “migliore approssimazione di X”, ovvero l’elemento più piccolo (= più preciso). Il massimo dei minoranti. GLB
es.: \( \displaystyle \alpha \)({1, 2}) = glb({+, \( \displaystyle \top \)} = +

La funzione di concretizzazione \( \displaystyle \gamma \) mappa un valore astratto in un insieme di valori concreti. Considera il minimo dei maggiornanti LUB.
es:
\( \displaystyle \gamma \)(+) = lub{\emptyset, {1}, {2}, {1, 2}, ...,\( \displaystyle {{Z}}^{+} \)} = \( \displaystyle {{Z}}^{+} \)

Per la correttezza delle analisi sono sufficienti se leguenti condizioni:
- la funzione di astrazione \( \displaystyle \alpha \) e la funzione di concretizzazione \( \displaystyle \gamma \) formano un'inserzione di Galois;
- \( \displaystyle \alpha \) e \( \displaystyle \gamma \) sono monotone;
- le operazioni astratte \( \displaystyle {O}{{P}}^{{A}} \) sono corrette localmente, ossia se eseguo una operazione astratta sui valori astratti, allora la concretizzazione di questa operazione mi dà un sovrainsieme degli elementi che avrei ottenuto eseguendo l'operazione concreta su tutte le concretizzazione dei valori astratti di partenza.

[hamming_burst]

allora ho guardato un po'.

Non riesco a comprendere in pieno certe strutturazioni, tipo le connessioni di Galois. Per i power-set penso sia una definizione standard per avere domini già definiti reticoli completi, ma per me ha un altro significato (power-domain).
Ho visto troppo poco sul tema dei reticoli, pensavo che non fossero utilizzati in modo così pesante, ma è tutta un'altra teoria. Anche se i CPO sono dei reticoli in sè, i teoremi hanno un'altra definizione. Dovrei vedermi come sono applicati, se sono validi, ecc... nella semantica astratta o concreta, ma ci vuole troppo tempo.