Fondamenti di Informatica, 14 Dicembre 2012

(appello straordinario: per ripetenti e fuori corso)

Non e' ammesso l'uso di alcun testo, appunti o calcolatrici. Le risposte vanno scritte nel foglio di bella copia. Si raccomanda la massima SINTETICITA'. L'eccessiva verbosita' verra' considerata negativamente. Occorre essersi prenotati sul portale studenti del nostro ateneo. Se cio' non e' stato fatto, comunicatelo immediatamente al docente o all'assistente in aula. I risultati verranno indicati nella pagina web del corso. Date ed orari degli orali, sul Forum.

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:

a_i ≠ a_j      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,A₀,B₀}, 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?