Esercizio 1
(a)
Cosa si intende per "semantica dei linguaggi di programmazione".
A cosa serve? Cosa si intende, in generale, per "semantica operazionale strutturata" e
per "semantica assiomatica"?
(b)
Descrivere in dettaglio il significato della seguente regola della semantica operazionale
del linguaggio WHILE:
ai ≠ aj a , begin δ end ⇓ b b , begin while Xi ≠ Xj do δ end ⇓ c
______________________________________________________
a begin while Xi ≠ Xj do δ end ⇓ c
Servono altre regole per completare la semantica delle istruzioni while del linguaggio? Se si, perche' e quali sono? se no, giustificare il motivo per cui
la regola sopra descritta e' sufficiente.
(c)
Supponiamo di voler introdurre nel linguaggio WHILE un nuovo tipo di istruzione della seguente forma:
for X1 do δ
La semantica informale di tale istruzione e' la seguente: si ripete l'esecuzione di
δ tante volte quanto e' il valore della variabile X1, ed ogni volta che si esegue δ
il valore di X1 viene decrementato, fino a diventare 0.
Per semplicita', si suppone che l'esecuzione di δ non debba contenere assegnamenti alla variabile X1.
Descrivere formalmente la semantica delle istruzioni for fornendo
una o piu' regole di inferenza.
Esercizio 2
(a)
Cos'e un sistema formale? Cos'e' un sistema formale alla Hilbert per la logica?
Cos'e' un sistema formale di deduzione naturale per la logica?
(b)
Dimostrare in deduzione naturale che A → B, A → C |- A → ((B/\C) \/ D)
(c)
Dimostrare il teorema di deduzione di Herbrand per la logica proposizionale.
Ricordiamo che gli assiomi per la logica proposizionale sono:
- α → (β → α)
- α → (β → γ) → ((α → β) → (α → γ))
- (not β → not α) → ((not β → α) → β)
Esercizio 3
Dimostrare che la stringa abaaba appartiene al linguaggio generato dalla grammatica G = ({a, b}, {S,A,B,A0,B0}, P, S),
dove P sono le produzioni
S --> T | ε
T --> aAT | bBT | A0a | A0b
Aa --> aA AA0 --> A0a
Ab --> bA BA0 --> A0b
Ba --> aB AB0 --> B0a
Bb --> bB BB0 --> B0b
A0 --> a
B0 --> b
Perche' non e' possibile fornire un albero di derivazione sintattica per la
stringa abaaba generata da G?