Correttezza di un programma funzionale

Formalmente, verificare la correttezza di un programma funzionale significa dimostrare che esso calcola una certa funzione matematica, la quale corrisponde alla specifica del programma. Per semplicità, tale problema verrà qui ridotto al problema di dimostrare che le definizioni delle funzioni soddisfano determinate proprietà. Adesso verranno presentate delle tecniche che permettono dieffettuare tali dimostrazioni.

Principio di induzione sui numeri naturali

La tecnica principale (ma non l’unica) usata per le dimostrazioni di proprietà dei programmi funzionali è il principio di induzione, la cui forma di base è quella sui numeri naturali: per dimostrare che una certa proprietà $P$ vale per tutti i numeri naturali $n\geq b$ (dove $b$ è spesso $0$) si dimostra che

• caso base: vale $P(b)$
• passo induttivo: per ogni $n \geq b, \ P(n)$ implica $P(n+1)$

Esempio: funzione fattoriale

Trasparenza referenziale

Siccome i programmi funzionali non hanno effetti collaterali, se un termine $t$ si riduce a un altro termine $t', t \twoheadrightarrow t'$, allora si possono considerare i due termini uguali, $t = t'$, cioè indistinguibili dal punto di vista del processo di valutazione: sostituire $t$ con $t'$ o viceversa nel contesto di una qualsiasi espressione si riduce. Infatti, si può dimostrare formalmente che, dati $t$ e $t'$ tali che $t \twoheadrightarrow t'$, una qualunque espressione $E(... t...)$ si riduce a un valore $V$ (non ulteriormente riducibile) se e solo se anche l’espressione $E(...t'...)$ ottenuta sostituendo $t$ con $t'$ si riduce allo stesso valore $V$,

$$ E(\dots t \dots) \twoheadrightarrow V \Longleftrightarrow E(\dots t'\dots) \twoheadrightarrow V $$

cioè le due espressioni sono in un certo senso rappresentazioni diverse dello stesso valore.

Questo principio prende il nome di trasparenza referenziale (referential transparency), ed è importante perchè permette di applicare il ragionamento equazionale, il modo di operare sulle equazioni/uguaglianze usato tipicamente in matematica. In particolare, la possibilità di applicare un’uguaglianza in entrambi i versi, sostituendo uno qualsiasi dei due lati con l’altro, dà una maggiore “agilità” nelle dimostrazioni rispetto a quella che si otterrebbe lavorando direttamente con la relazione di riduzione, la quale consente la sostituzione solo nel verso da sinistra a destra.

Data un’uguaglianza $t = t'$ ricavata da una relazione di riscrittura $t \twoheadrightarrow t'$, si chiamano:

• unfold l’operazione di sostituzione del lato sinistro $t$ con il lato destro $t'$ (cioè la sostituzione nel verso della riduzione $t \twoheadrightarrow t'$) in una qualche espressione
• fold l’operazione di sostituzione del ato destro $t'$ con il lato sinistro $t$ (cioè la sostituzione nel verso opporto alla riduzione $t \twoheadrightarrow t'$) in una qualche espressione.

Esempio: associativtà di ++

Esempio: reverse