Roberto Zunino, 2014
Diamo qui sotto una piccola lista di esercizi per il corso di informatica. Se avete problemi di visualizzazione, o volete scaricarla, è disponibile anche in PDF.
Nota: dall'AA 2016/17 questo argomento è stato rimosso dal corso.
Sia \(U\) un insieme universo, e \(f : \powset(U) \rightarrow \powset(U) \)
una funzione continua secondo Scott.
1) Dimostrare che la funzione
\[
\begin{array}{l}
h : \powset(U) \rightarrow \powset(U) \\
h(X) = X \cup f(X)
\end{array}
\]
è continua.
2) Dimostrare che il minimo punto fisso di \(h\) esiste e che
coincide con quello di \(f\).
Sia \(U\) un insieme universo,
\(A\) un sottoinsieme di \(U\)
e \(f : \powset(U) \rightarrow \powset(U) \)
una funzione continua secondo Scott.
1) Dimostrare che la funzione
\[
\begin{array}{l}
h : \powset(U) \rightarrow \powset(U) \\
h(X) = A \cup f(X)
\end{array}
\]
è continua.
2) Indicando con \(fix\) il minimo punto fisso,
dimostrate che \(fix(h)\) esiste e vale
\[
fix(h) \supseteq fix(f)
\]
3) Definite \(A\) e \(f\) in modo che \( fix(h) \neq fix(f) \).
Sia \(U\) un insieme universo,
e \(f,g : \powset(U) \rightarrow \powset(U) \)
due funzione continue secondo Scott.
1) Dimostrare che la funzione
\[
\begin{array}{l}
h : \powset(U) \rightarrow \powset(U) \\
h(X) = f(X) \cup g(X)
\end{array}
\]
è continua.
2) Indicando con \(fix\) il minimo punto fisso,
dimostrate che \(fix(h)\) esiste e vale
\[
fix(h) \supseteq fix(f) \cup fix(g)
\]
3) [Più impegnativo] Stabilite se la seguente funzione è continua o meno:
\[
\begin{array}{l}
h' : \powset(U) \rightarrow \powset(U) \\
h'(X) = f(X) \cap g(X)
\end{array}
\]
[Impegnativo] Sia \(h : \powset(U)\times\powset(U) \rightarrow \powset(U)\) una funzione binaria tale che, per ogni \(A,B\) insiemi le funzioni \[ \begin{array}{l} f : \powset(U) \rightarrow \powset(U) \\ f_A(Y) = h(A,Y)\\ g : \powset(U) \rightarrow \powset(U) \\ g_B(X) = h(X,B) \end{array} \] sono continue secondo Scott. Dimostrare che \[ \begin{array}{l} d : \powset(U) \rightarrow \powset(U) \\ d(Z) = h(Z,Z)\\ \end{array} \] è continua secondo Scott.
Sia \(U\) un insieme universo,
e \(f : \powset(U) \rightarrow \powset(U) \)
una funzione continua secondo Scott.
1) Dimostrare che la funzione
\[
\begin{array}{l}
g : \powset(U) \rightarrow \powset(U) \\
g(X) = f(f(X))
\end{array}
\]
è continua.
2) Dimostrare che il minimo punto fisso di \(g\) coincide con
quello di \(f\).
Sia \(S\) l'insieme delle sequenze finite di naturali definito induttivamente da \[ \dfrac{}{\epsilon}\ [S0] \qquad \dfrac{s}{n:s}(n\in\N)\ [S1] \] Si definisca induttivamente la relazione \({\sf len}\in\powset(S\times \N)\) che associa ad ogni sequenza la sua lunghezza.
Nelle stesse ipotesi del precedente esercizio, si definisca induttivamente la relazione \({\sf app} \in \powset(S\times S\times S)\) tale per cui \({\sf app}(x,y,z)\) vale quando la sequenza \(z\) è ottenuta concatenando le sequenze \(x\) e \(y\). Per esempio, \({\sf app}(1:2:\epsilon,5:1:3:\epsilon,z)\) vale solo quando \(z=1:2:5:1:3:\epsilon\).
Nelle stesse ipotesi del precedente esercizio, dimostrate che la concatenazione ``somma le lunghezze'', ovvero che: \[ \forall x,y,z\in S, n,m\in\N.\ {\sf app}(x,y,z) \land x\ {\sf len}\ n \land y\ {\sf len}\ m \implies z\ {\sf len}\ (n+m) \] Procedete per induzione su uno tra \(x\in S,n \in \N,{\sf app}(x,y,z), x\ {\sf len}\ n\). Potete provare a fare dimostrazioni diverse usando principi di induzione diversi.
(Lungo) Nelle stesse ipotesi del precedente esercizio, dimostrate che \({\sf len}\) e \({\sf app}\) sono funzioni.
Descrivete in modo informale ma preciso la relazione seguente. (\(S\) è definito come sopra.) \[ \begin{array}{c} {\sf map}\in\powset((\N\rightarrow\N)\times S\times S) \\[3mm] \dfrac{}{{\sf map}(f,\ \epsilon, \epsilon)}[M0] \qquad \dfrac{ {\sf map}(f,\ s,\ z) }{{\sf map}(f,\ n:s,\ f(n):z)}[M1] \end{array} \]
Sia \(R \in \powset(\Z\times\Z)\) la relazione definita induttivamente da \[ \dfrac{}{10\ R\ 4} \qquad \dfrac{x\ R\ y \qquad y\ R\ 0}{3x\ R\ 2y} \qquad \dfrac{x\ R\ x^2}{x\ R\ 2} \] Dimostrare che \[ \forall x,y\in\Z.\ x\ R\ y \implies x^2 > y \]
Si considerino le definizioni di \(S\) (insieme delle sequenze di naturali) e \({\sf map} \in \powset((\N \rightarrow \N) \times S \times S)\) viste sopra. Si definisca anche \(Q \in \powset((\N \rightarrow \N) \times S \times S)\) induttivamente come segue: \[ \begin{array}{c} \dfrac{}{Q(f, \epsilon, \epsilon)}\ [Q0] \qquad \dfrac{Q(f, s, z)}{Q(f, n:s, f(f(n)):z)}\ [Q1] \end{array} \] Si dimostri la seguente proprietà: \[ R:\qquad \forall f,s_1,s_2,s_3.\ {\sf map}(f, s_1, s_2) \land {\sf map}(f, s_2, s_3) \implies Q(f, s_1, s_3) \] Provate due strade diverse: 1) procedendo per induzione su \(s_1 \in S\), 2) procedendo per induzione su \({\sf map}(f,s_1,s_2)\). In entrambi i casi, partite definendo la proprietà \(T\) che usate per l'induzione, e verificate che quello che si ottiene per induzione effettivamente implica \(R\).
Riusando le stesse definizioni dell'esercizio di sopra,
si dimostri la seguente proprietà:
\[
R:\qquad
\forall f,g,s_1,s_2,s_3.\
{\sf map}(f, s_1, s_2) \land {\sf map}(g, s_2, s_3)
\implies {\sf map}(g\circ f, s_1, s_3)
\]
dove \(g\circ f\) denota la composizione
(\((g\circ f)(x) = g(f(x))\)).
Provate due strade diverse:
1) procedendo per induzione su \(s_1 \in S\),
2) procedendo per induzione su \({\sf map}(f,s_1,s_2)\).
In entrambi i casi, partite definendo la proprietà \(T\)
che usate per l'induzione, e verificate che
quello che si ottiene per induzione effettivamente implica \(R\).
Il principio di induzione afferma che, quando
\(f \in \powset(U) \rightarrow \powset(U)\) è monotona,
\[
f(Y) \subseteq Y \implies \fix(f) \subseteq Y
\]
Di tale principio esiste anche la seguente variante ``forte'':
\[
f(\fix(f) \cap Y) \subseteq Y \implies \fix(f) \subseteq Y
\]
Questa variante, usa un'ipotesi induttiva più forte, che non
afferma più soltanto l'appartenenza a \(Y\),
ma anche a \(\fix(f)\). Per esempio, procedendo per
induzione ``debole'' sui naturali e dimostrando il caso induttivo,
si deve fare vedere che \(p(n) \implies p(n+1)\) dove \(n\)
è un valore qualunque (un arbitrario elemento dell'universo \(U\)
sul quale abbiamo dato le regole di inferenza) e non per forza
un naturale (!).
Il principio ``forte'' consente invece di assumere
anche \(n\in\N\) tra le ipotesi induttive, e quindi semplificando
la dimostrazione del caso induttivo.
Si dimostri il principio forte, sfruttando quello debole.
Si estenda IMP con il comando
\[
{\sf do}\ c\ {\sf while}\ e\neq 0
\]
dove \(c\) è un comando ed \(e\) è un'espressione intera.
La semantica intuitiva del comando aggiunto è la seguente.
All'inizio si esegue \(c\); poi si valuta \(e\). Se \(e\)
vale zero, si esce dal ciclo. Altrimenti si ripete il tutto:
si riesegue \(c\), si rivaluta \(e\), etc.
Aggiungere una o più regole alla semantica
big step per formalizzare questo comportamento.
Si estenda IMP con il comando
\[
{\sf save}\ x\ {\sf in}\ c
\]
(dove \(x\) è una variabile e \(c\) un comando)
con la seguente semantica intuitiva.
Si annota il valore di x, poi si esegue c, e dopo si ripristina il
vecchio valore di x precedentemente annotato.
Aggiungere una o più regole alla semantica big step per formalizzare
questo comportamento.
[Impegnativo]
Si estenda IMP con il comando
\[
{\sf while}\ e\neq 0\ {\sf alternate}\ c_1\ {\sf with}\ c_2
\]
(dove \(e\) è un'espressione intera e \(c_1,c_2\) sono comandi)
con la seguente semantica intuitiva.
Si verifica la condizione \(e\neq 0\). Se non vale si esce dal ciclo.
Se vale si esegue \(c_1\) e si continua come segue.
Si verifica la condizione \(e\neq 0\). Se non vale si esce dal ciclo.
Se vale si esegue \(c_2\) e si ripete il tutto da capo, alternando
\(c_1\) e \(c_2\) ad ogni iterazione.
Aggiungere una o più regole alla semantica big step per formalizzare
questo comportamento.
Dopo avere letto l'esercizio precedente, dimostrate in modo informale che il comando \[ {\sf while}\ e\neq 0\ {\sf alternate}\ c_1 \ {\sf with}\ c_2 \] è equivalente a \[ \begin{array}{l} {\sf while}\ e\neq 0\ {\sf do}\\ \qquad c_1; \\ \qquad {\sf if}\ e\neq 0 \ {\sf then}\ c_2 \ {\sf else\ skip} \end{array} \]
[Impegnativo]
Si rimuovano dalla definizione della semantica big step di IMP
le due regole relative al comando \(\sf if\), e si aggiunga alle
regole rimaste la regola seguente:
\[
\dfrac{
\tuple{e , \sigma} \rightarrow_e v \qquad
\tuple{c_1 , \sigma} \rightarrow_b \sigma_1 \qquad
\tuple{c_2 , \sigma} \rightarrow_b \sigma_2
}{
\tuple{{\sf if}\ e \neq 0\ {\sf then}\ c_1\ {\sf else}\ c_2 , \sigma}
\rightarrow_b {\bf cond}(v, \sigma_1, \sigma_2)
}[If]
\]
dove l'operatore \(\bf cond\) è definito come segue
\[
\begin{array}{l}
{\bf cond} : \Z \times Store \times Store \rightarrow Store
\\
{\bf cond}(v,\sigma_1,\sigma_2) = \begin{cases}
\sigma_1 & \mbox{se } v\neq 0 \\
\sigma_2 & \mbox{se } v = 0
\end{cases}
\end{array}
\]
Dire se dopo questa modifica alle regole, la semantica rimane
equivalente alla semantica originale di IMP. Se si, giustificarlo
in modo informale ma preciso. Se no, trovare su quale comando
la nuova semantica differisce e spiegarne il motivo.
Si estenda IMP con il comando
\[
{\sf swap}(x,y)
\]
(dove \(x,y\) sono variabili)
con la seguente semantica intuitiva.
I valori delle due variabili vengono scambiati.
Aggiungere una o più regole alla semantica big step per formalizzare
questo comportamento.
Si estenda IMP con il comando
\[
{\sf repeat}\ e\ {\sf times}\ c
\]
(dove \(e\) è un'espressione intera e \(c\) è un comando)
con la seguente semantica intuitiva.
All'inizio viene valutata \(e\): sia \(z\) il suo valore.
Se \(z \leq 0\), il comando \(\sf repeat\) non ha nessun effetto.
Altrimenti, il comando \(\sf repeat\) esegue
il comando \(c\) esattamente \(z\) volte.
Per esempio,
\[
\begin{array}{l}
x := 0; \\
y := 5; \\
{\sf repeat}\ y\ {\sf times}\\
\qquad x:=x+1; \\
\qquad y:=y+1 \\
\end{array}
\]
termina in uno stato in cui \(x\) vale \(5\) e \(y\) vale \(10\).
Aggiungere una o più regole alla semantica big step per formalizzare
questo comportamento.
Si estenda IMP con il comando
\[
{\sf loop}\ c_1\ {\sf exit\ if}\ e = 0\ {\sf otherwise}\ c_2
\]
(dove \(e\) è un'espressione intera e \(c_1,c_2\) sono comandi)
con la seguente semantica intuitiva.
All'inizio viene eseguito \(c_1\). Poi viene valutata \(e\): se il
risultato è nullo, il comando \(\sf loop\) termina qui. Altrimenti,
viene eseguito \(c_2\) e poi si ripete tutto il \(\sf loop\) da capo.
Per esempio,
\[
\begin{array}{l}
x := 0; \\
y := 5; \\
{\sf loop}\\
\qquad y:=y-1 \\
\qquad {\sf exit\ if}\ y=0 \ {\sf otherwise}\\
\qquad x:=x+1 \\
\end{array}
\]
termina in uno stato in cui \(x\) vale \(4\) e \(y\) vale \(0\).
Aggiungere una o più regole alla semantica big step per formalizzare
questo comportamento.
Si estenda IMP con il comando
\[
{\sf take}\ x \ {\sf in}\ c
\]
(dove \(x\) è una variabile e \(c\) è un comando)
con la seguente semantica intuitiva.
All'inizio viene eseguito \(c\). Poi,
il valore di tutte le variabili viene ripristinato al valore
precedente all'esecuzione di \(c\), tranne per \(x\) che invece
preserva il suo valore successivo all'esecuzione di \(c\).
Aggiungere una o più regole alla semantica big step per formalizzare
questo comportamento.
Sia \(x\) una variabile fissata di IMP.
Si consideri il seguente predicato sui comandi di IMP, definito
ricorsivamente.
\[
\begin{array}{l}
\dfrac{}{p(x:=0)}[P0]
\qquad
\dfrac{}{p(x:=2\cdot e)}[P1]
\\[5mm]
\dfrac{p(c_2)}{p(c_1;c_2)}[P2]
\qquad
\dfrac{p(c_1) \qquad p(c_2)
}{
p({\sf if}\ e\neq 0\ {\sf then}\ c_1\ {\sf else}\ c_2)
}[P3]
\end{array}
\]
(Sopra, \(x\) è fissata, mentre \(e,c_1,c_2\) sono arbitrari)
Dimostrare, sfruttando il principio di induzione associato a \(p\),
che
\[
p(c) \land \tuple{c,\sigma}\rightarrow_b \sigma'
\implies
\sigma'(x)\ \textrm{pari}
\]
Dimostrate che il comando \[ {\sf while}\ e\neq 0\ {\sf do}\ c \] è equivalente a \[ \begin{array}{l} {\sf while}\ e\neq 0\ {\sf do}\\ \qquad {\sf if}\ e\neq 0 \ {\sf then}\ c \ {\sf else\ skip} \end{array} \] Nella dimostrazione, fate riferimento alle relative derivazioni per i comandi di sopra.
Dimostrate che il comando \[ {\sf if}\ e_1\cdot e_2\neq 0\ {\sf then}\ c_1 \ {\sf else}\ c_2 \] è equivalente a \[ \begin{array}{l} {\sf if}\ e_1\neq 0\ {\sf then}\\ \qquad {\sf if}\ e_2\neq 0\ {\sf then}\ c_1 \ {\sf else}\ c_2 \\ {\sf else}\\ \qquad c_2 \end{array} \] Nella dimostrazione, fate riferimento alle relative derivazioni per i comandi e/o espressioni di sopra.
Dimostrate che il comando \[ {\sf if}\ x \neq 0\ {\sf then}\ x:=1 \ {\sf else}\ x:=x+1 \] è equivalente a \[ x := 1 \] Nella dimostrazione, fate riferimento alle relative derivazioni per i comandi e/o espressioni di sopra.
Dimostrate che il comando \[ x:=x+1 ; {\sf if}\ x \neq 0\ {\sf then}\ c_1 \ {\sf else}\ c_2 \] è equivalente a \[ {\sf if}\ x+1 \neq 0\ {\sf then}\ x:=x+1; c_1 \ {\sf else}\ x:=x+1; c_2 \] Nella dimostrazione, fate riferimento alle relative derivazioni per i comandi e/o espressioni di sopra.
Dimostrate che il comando \[ x:=5\;;\; {\sf if}\ x \neq 0\ {\sf then}\ c_1 \ {\sf else}\ c_2 \] è equivalente a \[ x:=5\;;\; c_1 \] Nella dimostrazione, fate riferimento alle relative derivazioni per i comandi e/o espressioni di sopra.
Dimostrate che il comando \[ x:=5\;;\; {\sf if}\ x \neq 0\ {\sf then}\ c_1 \ {\sf else}\ c_2 \] è equivalente a \[ x:=5\;;\; c_1 \] Nella dimostrazione, fate riferimento alle relative derivazioni per i comandi e/o espressioni di sopra.
Considerate il comando di IMP (esteso con \(\land\))
\[
{\sf if}\ \phi_1 \land \phi_2 \ {\sf then}\ c_1 \ {\sf else}\ c_2
\]
dove \(\phi_{1},\phi_{2}\) sono espressioni booleane.
Riscrivete il comando sopra in modo equivalente senza usare
l'operatore \(\land\). (Potete assumere che dentro \(\phi_1,\phi_2\)
non ci siano altri \(\land\).)
Infine, ripetete l'esercizio sopra nella sua naturale variante per
\[
{\sf if}\ \phi_1 \lor \phi_2 \ {\sf then}\ c_1 \ {\sf else}\ c_2
\]
e per
\[
{\sf if}\ \lnot\phi_1 \ {\sf then}\ c_1 \ {\sf else}\ c_2
\]
Si dimostri la seguente tripla di Hoare \[ \begin{array}{l} \hoareA{n\geq 0}\\ s := 0; \\ x := 0; \\ {\sf while}\ x \leq n \ {\sf do} \\ \qquad {\sf if}\ f(x) \neq 0 \ {\sf then} \\ \qquad\qquad s := s + f(x) \\ \qquad {\sf else} \\ \qquad\qquad {\sf skip}; \\ \qquad x:=x+1 \\ \hoareA{s = \sum_{X=0}^{n} f(X)} \end{array} \] Come si può semplificare il programma di sopra in modo equivalente?
Si dimostri la seguente tripla di Hoare \[ \begin{array}{l} \hoareA{n\geq 0}\\ s := 0; \\ x := 0; \\ {\sf while}\ x \leq n \ {\sf do} \\ \qquad {\sf if}\ f(x) \geq 0 \ {\sf then} \\ \qquad\qquad s := s + f(x) \\ \qquad {\sf else} \\ \qquad\qquad s := s - f(x); \\ \qquad x:=x+1 \\ \hoareA{s = \sum_{X=0}^{n} \mid f(X) \mid} \end{array} \]
Sotto, indichiamo con \(fib(n)\) l'ennesimo numero di Fibonacci: \(fib(0)=0, fib(1)=1, fib(n+2)=fib(n)+fib(n+1)\). Si dimostri la seguente tripla di Hoare \[ \begin{array}{l} \hoareA{n = N \geq 0}\\ a := 0; \\ b := 1; \\ {\sf while}\ n > 0 \ {\sf do} \\ \qquad b := a+b; \\ \qquad a := b-a; \\ \qquad n := n-1 \\ \hoareA{a = fib(N)} \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{n = N \geq 0 } \\ x := 0 ; \\ y := 1 ; \\ {\sf while}\ x < n\ {\sf do} \\ \qquad y := 0 - y; \\ \qquad x := x + 1 \\ \hoareA{y = (-1)^N } \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{n = N \geq 0 } \\ x := 0 ; \\ y := 1 ; \\ {\sf while}\ x < n\ {\sf do} \\ \qquad {\sf if}\ y=1\ {\sf then}\\ \qquad \qquad y := -1 \\ \qquad {\sf else}\\ \qquad \qquad y := 1; \\ \qquad x := x + 1 \\ \hoareA{y = (-1)^N } \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{n = N \geq 0 \land a = A } \\ {\sf while}\ n > 0\ {\sf do} \\ \qquad a := a * a; \\ \qquad n := n - 1 \\ \hoareA{a = A^{(2^N)} } \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{a \leq b } \\ {\sf while}\ a < b \ {\sf do} \\ \qquad {\sf if}\ b - a > 5 \ {\sf then}\\ \qquad\qquad x:=5 \\ \qquad {\sf else}\\ \qquad\qquad x:=1; \\ \qquad a := a+x \\ \hoareA{a = b } \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{ x =X \geq 0 \land y = q = 0 } \\ {\sf while}\ x > 0 \ {\sf do} \\ \qquad x:=x-1; \\ \qquad y:=y+1; \\ \qquad {\sf if}\ y = 5 \ {\sf then}\\ \qquad\qquad y:=0; \\ \qquad\qquad q := q+1 \\ \qquad {\sf else}\\ \qquad\qquad {\sf skip} \\ \hoareA{q = \lfloor X / 5 \rfloor } \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{ 0 \leq x = X \leq y = Y } \\ z := y-x ; \\ {\sf while}\ z > 0 \ {\sf do} \\ \qquad x:=x+1; \\ \qquad y:=y-1; \\ \qquad z:=z-1; \\ \hoareA{ x = Y \land y = X } \end{array} \]
Si dimostri la validità della tripla di Hoare seguente: \[ \begin{array}{l} \hoareA{ n = N \geq 0 } \\ s := 0 ; \\ x := 1 ; \\ {\sf while}\ n > 0 \ {\sf do} \\ \qquad s:=s+x; \\ \qquad x:=2*x; \\ \qquad n:=n-1; \\ \hoareA{ s = 2^N - 1 } \end{array} \]
Si aggiunga al sistema deduttivo per le triple di Hoare la regola \[ \dfrac{ \hoare{P}{c}{Q} }{ \hoare{P}{{\sf while}\ \phi\ {\sf do}\ c}{Q} } \] Stabilire se con la regola aggiunta il sistema deduttivo continua ad essere corretto. In altri termini, stabilire se continua a valere \[ \vdash \hoare{P}{c}{Q} \implies \vDash \hoare{P}{c}{Q} \] per ogni comando \(c\).
Si aggiunga al sistema deduttivo per le triple di Hoare la regola \[ \dfrac{ \hoare{P}{c}{P} }{ \hoare{P}{{\sf while}\ \phi\ {\sf do}\ c}{P} } \] Stabilire se con la regola aggiunta il sistema deduttivo continua ad essere corretto.
Si aggiunga al sistema deduttivo per le triple di Hoare la regola \[ \dfrac{ \hoare{P}{c}{Q} }{ \hoare{P}{{\sf if}\ \phi\ {\sf then}\ c\ {\sf else}\ c}{Q} } \] Stabilire se con la regola aggiunta il sistema deduttivo continua ad essere corretto.
Si aggiunga al sistema deduttivo per le triple di Hoare la regola \[ \dfrac{ \hoare{P}{x:=e_2}{Q} }{ \hoare{P}{x:=e_1;\ x:=e_2}{Q} } \] Stabilire se con la regola aggiunta il sistema deduttivo continua ad essere corretto.
[Impegnativo] Si aggiunga al sistema deduttivo per le triple di Hoare la regola \[ \dfrac{ \hoare{P\{5/x\} \land x=0 }{c_2}{Q} }{ \hoare{P\{5/x\} }{x:=0;\ {\sf if}\ x\neq 0\ {\sf then}\ c_1\ {\sf else}\ c_2}{Q} } \] Stabilire se con la regola aggiunta il sistema deduttivo continua ad essere corretto.
Si aggiunga al sistema deduttivo per le triple di Hoare la regola \[ \dfrac{ \hoare{P \land x=0 }{c_2}{Q} }{ \hoare{P}{x:=0;\ {\sf if}\ x\neq 0\ {\sf then}\ c_1\ {\sf else}\ c_2}{Q} } \] Stabilire se con la regola aggiunta il sistema deduttivo continua ad essere corretto.
Sia \(f : \Z \rightarrow \Z\) una funzione arbitraria, e aggiungete \(f(Exp)\) alle espressioni di IMP. Si scriva un programma \(c\) tale per cui \[ \begin{array}{l} \hoareA{a=A \land b=B>A}\\ c \\ \hoareA{x=f(A)+2\cdot f(A+1)+3\cdot f(A+2)+ \cdots+(B-A+1)\cdot f(B)} \end{array} \] Si giustifichi informalmente la correttezza della soluzione proposta, e se ne stimi la complessità asintotica.
Sia \(f : \Z \rightarrow \Z\) una funzione arbitraria, e aggiungete \(f(Exp)\) alle espressioni di IMP. Si scriva un programma \(c\) che, dati \(A\) e \(B\) con \(A<B\), conti quanti minimi locali di \(f\) ci sono nell'intervallo \([A,B]\). Un minimo locale è un \(f(X)\) tale per cui \(f(X) \leq f(X-1)\) e \(f(X) \leq f(X+1)\). Si stimi infine la complessità asintotica della soluzione proposta.
Si consideri il linguaggio IMP esteso con i vettori (array). Si scriva un programma in tale linguaggio tale che, dato un vettore in una variabile \(a\), lo modifichi invertendo l'ordine delle componenti. Per esempio, un vettore \(\tuple{1,2,3}\) deve trasformarsi in \(\tuple{3,2,1}\). Si usi l'espressione \(a.length\) per indicare la lunghezza del vettore. Si giustifichi informalmente la correttezza della soluzione proposta, e se ne stimi la complessità asintotica.
Si consideri il linguaggio IMP esteso con i vettori (array). Si scriva un programma in tale linguaggio tale che, dato un vettore in una variabile \(a\), lo modifichi incrementando ogni componente maggiore di \(5\). Per esempio, un vettore \(\tuple{1,20,3}\) deve trasformarsi in \(\tuple{1,21,3}\). Si usi l'espressione \(a.length\) per indicare la lunghezza del vettore. Si giustifichi informalmente la correttezza della soluzione proposta, e se ne stimi la complessità asintotica.
Si consideri il linguaggio IMP esteso con i vettori (array). Si scriva un programma in tale linguaggio tale che, dato un vettore di interi \(\tuple{a_1,a_2,a_3,\ldots,a_{n-1},a_n}\) in una variabile \(a\), lo modifichi facendolo diventare \(\tuple{0,a_1,a_2,a_3,\ldots,a_{n-1}}\). Per esempio, un vettore \(\tuple{2,3,4,5}\) deve trasformarsi in \(\tuple{0,2,3,4}\). Si usi l'espressione \(a.length\) per indicare la lunghezza del vettore. Si giustifichi informalmente la correttezza della soluzione proposta, e se ne stimi la complessità asintotica.
Si costruisca un algoritmo per calcolare \(\lfloor \sqrt{x} \rfloor\) dato un intero \(x\) positivo. Nel farlo, si usino solo le operazioni aritmetiche elementari (non la radice quadrata). Si miri a ottenere un algoritmo efficiente, considerandone la complessità asintotica.
Si considerino i seguenti due algoritmi per eliminare
i duplicati da un vettore \(\tuple{a_0,\ldots,a_{n-1}}\),
producendo un altro vettore (più corto, in generale)
\(\tuple{b_0,\ldots,b_{m-1}}\),
Algoritmo 1) Scandisco tutte le posizioni di \(a\) con \(0\leq i < n\).
Per ogni \(a_i\), controllo se esiste un \(j\in [0,i)\) tale che
\(a_j=a_i\). Se esiste, non faccio nulla, altrimenti lo aggiungo
al vettore \(b\).
Algoritmo 2) Inizio ordinando il vettore \(a\). Poi ne scandisco
le posizioni con \(0\leq i < n\). Per ogni \(a_i\), controllo se
\(i>0\) e \(a_{i-1}=a_i\). In tal caso, non faccio nulla, altrimenti
aggiungo \(a_i\) al vettore \(b\).
Sopra, ``aggiungere al vettore \(b\)'' vuole semplicemente indicare
l'operazione \(b[k]:=a[i];k:=k+1\) dove \(k\) è una variabile
inizialmente posta a \(0\).
Si stimi la complessità asintotica di entrambi gli algoritmi.
Siano dati due vettori \(\tuple{a_0,\ldots,a_{n-1}}\) e
\(\tuple{b_0,\ldots,b_{n-1}}\) contenenti i coefficienti di due polinomi
\[
\begin{array}{l}
p(x) = a_0 + a_1\cdot x + \cdots + a_{n-1} \cdot x^{n-1} \\
q(x) = b_0 + b_1\cdot x + \cdots + b_{n-1} \cdot x^{n-1}
\end{array}
\]
Scrivere un programma in IMP, esteso con i vettori (array), che
produce in un vettore \(c\) (di lunghezza \(2\cdot n-1\))
i coefficienti del polinomio \(r(x) = p(x)\cdot q(x)\).
Si giustifichi informalmente la correttezza della soluzione proposta,
e se ne stimi la complessità asintotica.
Home - Teaching - Informatica
Roberto Zunino, 2014