\documentclass[a4paper, 12pt]{article}

\usepackage{amssymb}

\begin{document}


\subsection*{Computazioni, Programmazione funzionale e Preludio al $\lambda$-calcolo}
Cosa significa {\bf computare}? In generale possiamo affermare che "computare" significa 
\begin{quote}
{\em trasformare una informazione da una forma implicita ad una forma esplicita.}
\end{quote}
Per esempio, quando trasformiamo una espressione come {\tt (3+4)*2} in {\tt 14}, stiamo eseguendo un calcolo, una computazione. Entrambe le espressioni rappresentano (denotano) il numero $\mathit{14}$, ma tale informazione \`e ovviamente pi\`u esplicita in  {\tt 14} che in {\tt (3+4)*2}.

Questa definizione di computazione \`e per\`o troppo vaga. Dobbiamo renderla precisa, formalizzarla,
attraverso la definizione di uno specifico modello computazionale. Un {\em modello computazionale} \`e una specifica formalizzazione matematica del concetto di "computazione" e delle nozioni ad asso collegate: informazione, trasformazione (passo di computazione), ecc.\\
Ci sono vari modelli computazionali (e tanti altri se ne potranno sviluppare ancora), anche molto differenti tra di loro: Turing Machines, URM, Sistemi di Post, $\lambda$-calcolo, Programmazione logica, il formalismo delle Funzioni parziali ricorsive, ecc. ecc.

I linguaggi di programmazione che utilizziamo sono, direttamente o indirettamente, ispirati ognuno
ad uno o pi\`u modelli computazionali. In generale, "programmare" significa descrivere un particolare processo computazionale (un algoritmo) in un linguaggio di programmazione, che si basa su uno o pi\`u modelli computazionali\footnote{In realt\`a possiamo descrivere un algoritmo direttamente in un modello computazionale, che pu\`o venire inteso infatti come un modo di formalizzare
il concetto stesso di algoritmo.}. 

I linguaggi di programmazione si  possono classificare in base al modello computazionale su cui si basano\footnote{Molti linguaggi appartengono a pi\`u di una classe. Per esempio C++ \`e sicuramente imperativo, ma \`e anche Object-Oriented.}
\begin{description}
\item[I {\em Linguaggi di programmazione {\bf imperativi}}] (come {\sf C}, {\sf Pascal}, {\sf Fortran}, \ldots) sono quelli basati su modelli come le Turing Machines o le URM. Infatti le nozioni fondamentali di tali linguaggi (formalizzate nei modelli computazionali su cui si basano) sono:
\begin{itemize}
\item
memoria
\item
variabile - qualcosa il cui contenuto si pu\`o "leggere" e  "modificare" (cella di memoria)
\item
assegnamento
\item
istruzione
\item
iterazione
\end{itemize} 
\item[I {\em Linguaggi di programmazione {\bf funzionali}}]
\hspace{-1.5mm}\footnote{
I linguaggi funzionali sono sempre pi\`u utilizzati anche a livello industriale
(https://wiki.haskell.org/Haskell\_in\_industry
). Alcuni esempi: Facebook utilizza {\sf Haskell} per facilitare
l'esecuzione delle {\em news feeds}; WhatsApp si affida ad
{\sf Erlang} per i messaging servers, arrivando a poter gestire fino a 2 
milioni di utenti connessi per server; Twitter,
LinkedIn, Foursquare, Tumblr, and Klout utilizzano {\sf Scala}
per sviluppare le core infrastructure for i siti. 
Inoltre, anche se non utilizza direttamente linguaggi funzionali,
il popolare modello  MapReduce di Google per la computazione sul cluod
\`e stato ispirato dalle funzioni {\tt map} and {\tt reduce} che comunemente si trovano
nella programmazione funzionale.
[{\em citazione da Hu, Z., Hughes, J., Wang, M.: How functional programming mattered. Ntl. Sci.
Rev. 2(3), 349-370 (2015)}]
} (come {\sf Haskell}, {\sf Scheme}, {\sf ML}, {\sf OCaml}, {\sf Erlang}\ldots)
Tali linguaggi fanno riferimento al modello computazionale del {\em $\lambda$-calcolo} ed i concetti presenti nei linguaggi imperativi, cos\`i naturali\footnote{solo perch\'e abbiamo solo lavorato finora principalmente con linguaggi imperativi.} per molti di noi, sono {\bf completamente} assenti (o assumono un significato differente).
Troviamo invece nozioni come 
\begin{itemize}
\item
espressione
\item
variabile - da intendere nel senso matematico:
   \begin{itemize}
    \item entit\`a sconosciuta
    \item astrazione di un valore concreto
   \end{itemize}
\item
valutazione - differente dalla nozione di {\em esecuzione}:
   \begin{itemize}
    \item quando si valuta una espressione matematica non modifichiamo alcunch\'e.
   \end{itemize}
\item
ricorsione
\end{itemize}

\item[I {\em Linguaggi di programmazione {\bf logici}}]  (come {\sf Prolog} ed i suoi numerosi dialetti)
Si basano su alcune propriet\`a di sottosistemi della logica del primo ordine (che studieremo).
Il concetto di computazione coincide con il concetto di ricerca di una deduzione per una formula logica. Programmare consiste nel definire le ipotesi che ci possono permettere di dimostrare l'esistenza
del valore che intendiamo calcolare.
\end{description}
\noindent
Non elenchiamo altre classi di linguaggi di programmazione poich\'e nel nostro corso ci interessiamo 
solo ai modelli computazionali relativi alle classi sopra elencate. 

\subsubsection*{La programmazione funzionale}

\noindent
Prendiamo la definizione {\bf 1.41} del testo di Ausiello:\\
la funzione che restituisce l'{inversa} di una stringa $x\in\Sigma^*$ \`e definita come
$$
\tilde{x} = \left\{ \begin{array}{l@{\hspace{4mm}}l}
                      \varepsilon & \mbox{se $x=\varepsilon$}\\
                      \tilde{y}a & \mbox{se $x= ay$ \hspace{3mm }con $a\in\Sigma$ e $y\in\Sigma^*$}
                      \end{array}\right.
$$

Questa definizione, oltre ad identificare univocamente una funzione sulle stringhe di un alfabeto $\Sigma$, descrive implicitamente anche un metodo per calcolarla.
Infatti, usando questa definizione, possiamo facilmente calcolare, per esempio, $\widetilde{cbb}$:
$$
\begin{array}{rl}
 &\widetilde{cbd} \\
= & \widetilde{bd}c \\
= & \widetilde{d}bc \\
= & \widetilde{\varepsilon}dbc\\
= & dbc
\end{array}
$$

Nei linguaggi di programmazione funzionali, l'attivit\`a di programmazione consiste nel definire
funzioni che, come nell'esempio appena visto, descrivono implicitamente anche un 
metodo per calcolarle\footnote{Non tutte le definizioni di funzioni descrivono anche un procedimento per il loro calcolo.
Per esempio, si consideri il seguente sistema di equazioni differenziali
$$
\begin{array}{l}
f: \mathbb{R} \rightarrow \mathbb{R} ,   g: \mathbb{R} \rightarrow \mathbb{R}\\[1mm]
f '' - 6g' = 6 sen(x)\\
6g'' + a2 f ' = 6 cos(x) \\[1mm]
f(0) = 0,  f '(0) = 0,  g(0) = 1,  g'(0) = 1 
\end{array}
$$
Esistono solo una $f$ ed una $g$ che soddisfano queste equazioni, e quindi questo sistema \`e
una definizione di (cio\'e un modo di identificare univocamente) $f$ e $g$. Questa definizione per\`o non
ci dice anche come {\em calcolare} il valore di $f$ e $g$ quando gli applichiamo degli argomenti.
}.

Nel linguaggio {\sf Haskell}, per esempio, la funzione ''inversa di una stringa''\footnote{Per {\sf Haskell} le stringhe sono liste di caratteri. La stringa vuota corrisponde quindi alla lista vuota di
caratteri: {\tt []}.} si descrive,
mutando leggermente la sintassi, esattamente come fatto sopra:

\begin{verbatim}
inv []    = []
inv (a:y) = (inv y)++[a]
\end{verbatim}

Quando chiediamo ad {\sf Haskell} di calcolare l'inversa della stringa $cbd$, scriviamo 
\begin{verbatim}
> inv "cbd"
\end{verbatim}
ricevendo come risposta
\begin{verbatim}
> "dbc"
\end{verbatim}
La computazione eseguita da {\sf Haskell} \`e simile a quella che abbiamo eseguito prima per calcolare $\widetilde{cbd}$.

Per comprendere in dettaglio qual \`e il tipo di ''computazioni'' eseguite dai linguaggi di programmazione funzionali e formalizzate nel modello computazionale del $\lambda$-calcolo,
forniamo, sempre in {\sf Haskell}, una versione equivalente e pi\`u ''elementare'' di {\tt inv}:
\begin{verbatim}
inv = \y -> if (null y) then y
                        else (inv (tail y))++[head y] 
\end{verbatim}
Per capire meglio il senso di quanto scritto sopra,
{\tt null}, {\tt tail}, {\tt head} e {\tt ++} sono funzioni predefinite di {\sf Haskell}:
\begin{description}
\item
{\tt null} restituisce {\tt True} se l'argomento \`e una lista vuota, {\tt False} altrimenti;
\item
{\tt tail} prende una lista come argomento e restituisce una lista unguale, ma senza il primo elemento;
\item
{\tt head} prende una lista come argomento e restituisce il suo primo elemento;
\item {\tt ++} prende due liste come argomenti e restituisce la loro concatenazione.
\end{description}
{\tt if\ldots then\ldots else} invece permette di costruire espressioni condizionali. Il valore di una espressione
{\tt if {\em expr1} then {\em expr2} else {\em expr3}} corrisponde al valore dell'espressione
{\tt \em expr2} se il valore di {\tt \em expr1} \`e {\tt True}, e al valore di {\tt \em expr3} se il valore di {\tt \em expr1} \`e {\tt False}.


\noindent
Inoltre, possiamo interpretare il senso di {\tt inv =} come {\em {\tt inv} \`e il nome di \ldots},
mentre possiamo interpretare il senso di {\tt $\backslash$y ->} come {\em questa \`e una funzione che, se prende in input un argomento {\tt y}, restituisce \ldots}\\

Vediamo qualche altro esempio di funzioni definite in {\sf Haskell}:

\begin{verbatim}
square x = x*x
\end{verbatim}
La funzione {\tt square} calcola il quadrato di un numero. Questa definizione \`e, come nel caso della funzione  {\tt inv} una rappresentazione compatta di
\begin{verbatim}
square = \x -> x*x
\end{verbatim}

Possiamo definire in {\sf Haskell} la funzione {\em fattoriale}:
\begin{verbatim}
fact 0 = 1
fact n = n*(fact (n-1))
\end{verbatim}
che \`e una rappresentazione pi\`u comprensibile (zucchero sintattico, si usa dire) di
\begin{verbatim}
fact = \n -> if (n==0) then 1 else n*(fact (n-1))
\end{verbatim}

Da quanto visto, possiamo dire che quando si definisce una funzione in un linguaggio 
di programmazione funzionale si fanno le seguenti cose:
\begin{enumerate}
\item
\label{i}
costruire una {\em espressione matematica} partendo da {\bf variabili}, {\bf costanti}, {\bf funzioni predefinite}
e {\em nomi}\footnote{I nomi non sono altro che variabili, a cui possiamo associare una espressione attraverso l'operatore {\tt =}.} di funzioni precedentemente definite \linebreak dall'utente (quando si definiscono funzioni ricorsive
si pu\`o utilizzare il nome stesso della funzione che stiamo definendo). 
A partire dagli elementi indicati, l'espressione si costruisce utilizzando l'{\bf applicazione funzionale}.\footnote{ Per esempio, l'espressione  {\tt x*x} \`e "costruita" applicando la funzione predefinita {\tt '*'} a due argomenti, entrambi costituiti dalla variabile {\tt x}.
%\\ L'espressione {\tt if (n==0) then 1 else n*(fact (n-1))}
%e' costruita invece formando {\tt (n==0)} applicando l'operatore di uguaglianza a due argomenti: la variabile {\tt n} e la costante {\tt n}; poi formando {\tt n*(fact (n-1))} applicando {\tt '-'} agli argomenti {\tt n} ed {\tt 1}, applicando {\tt  (n-1)} al nome di funzione {\tt fact} e poi utilizzando  {\tt n} e {\tt (fact (n-1))} come argomenti argomenti da applicare a {\tt '*'}.
%Infine {\tt n}, {\tt 1} e {\tt n*(fact (n-1))} le usiamo come argomenti dell'operatore \linebreak{\tt if  then  else}  per costruire l'espressione\\
%\centerline{\tt if (n==0) then 1 else n*(fact (n-1))}.
}
\item
costruire una {\em funzione anonima} (cio\'e senza nome) a partire \linebreak dall'espressione costruita nel punto \ref{i}. Tale espressione viene chiamata {\em corpo} della funzione. Per costruire la funzione anonima identifichiamo una variabile (che chiamiamo {\em parametro formale della funzione}) nel corpo della funzione e
utilizziamo l'operatore di {\bf astrazione funzionale}, che in {\sf Haskell} \`e\\
\vspace{-8mm}
\begin{verbatim}  
                         \ ->
\end{verbatim}
Nell'esempio del fattoriale, dopo aver costruito l'espressione (il corpo delle funzione)
{\tt  if (n==0) then 1 else n*(fact (n-1))} identifichiamo {\tt n} come parametro formale e
applichiamo l'operatore di astrazione funzionale, ottenendo:
\vspace{-4mm}
\begin{verbatim}
          \n -> if (n==0) then 1 else n*(fact (n-1))
\end{verbatim}
E' importante notare che nella programmazione funzionale una funzione anonima cos\`i definita \`e anch'essa una espressione. Questo permette di poter definire funzioni che prendono altre funzioni
come argomento, o che restituiscono funzioni come risultato.
\item
{\bf associare} l'espressione che rappresenta la funzione anonima {\bf ad un nome}, utilizzando l'operatore {\tt =}. Nel caso del fattoriale:
\vspace{0mm}
\begin{verbatim}
     fact = \n -> if (n==0) then 1 else n*(fact (n-1))
\end{verbatim}
Da notare che non dobbiamo necessariamente associare ad un nome una espressione che rappresenta una funzione anonima. Possiamo associare ad un nome una qualsiari espressione,
per esempio
%\vspace{-4mm}
\begin{verbatim}
     pippo = (2+3)*7
\end{verbatim}
Poich\'e un nome (una variabile) \`e un'espressione, se chiediamo ad {\sf Haskell} di valutare
l'espressione {\tt pippo}, verr\`a valutata l'espressione associata a {\tt pippo}, restituendo {\tt 35}
\end{enumerate}

Dalla breve discussione fatta possiamo capire perch\'e i seguenti elementi sono utilizzati in tutti i linguaggi funzionali per costruire espressioni e definire funzioni:
\begin{itemize}
\item
variabili
\item
costanti
\item
funzioni base
\item
applicazione funzionale
\item
astrazione funzionale
\item
associazione di espressioni a nomi\footnote{In realt\`a alcuni linguaggi associano ad un nome un'espressione, per esempio {\sf Haskell}, mentre altri, come {\sf Scheme}, associano ad un nome un {\em valore}. Noi non stiamo facendo un corso di Programmazione Funzionale e quindi
ci interessa solo avere una idea, seppur abbastanza precisa, di cosa significa programmare in un linguaggio funzionale.}
\end{itemize}
\noindent
E' importante notare come, ogni volta che si utilizza un nome in un'espressione, per esempio
in {\tt (square 7)+5}, si potrebbe evitare di usarlo, sostituendo ad esso l'espressione
ad esso associata:
\vspace{-2mm}
\begin{verbatim}
     ((\x -> x*x) 7) +5)
\end{verbatim}
 Sembrerebbe quindi che, anche se \`e qualcosa che aiuta a
migliorare la leggibilit\`a del nostro codice, associare espressioni a nomi non sia strettamente
indispensabile. Questo per\`o (almeno in apparenza) non \`e vero se consideriamo
definizioni di funzioni ricorsive. Infatti, se \`e possibile utilizzare 
\vspace{-2mm}
\begin{verbatim}
     (\x -> x*x)
\end{verbatim}
in una espressione dove si utilizzi {\tt square}, non possiamo certo utilizzare
\begin{verbatim}
     \n -> if (n==0) the 1 else n*(fact (n-1))
\end{verbatim}
in un punto dove debba essere utilizzata la funzione fattoriale. Questa funzione anonima contiene
{\tt fact}, e quindi dovremmo andare a sostituire la funzione anonima al posto del nome {\tt fact},
ottenendo per\`o un'espressione che ancora contiene {\tt fact} e cos\`i via ... ma non possiamo certo andare avanti 
all'infinito. Associare espressioni a nomi sembra quindi indispensabile per definire funzioni ricorsive.\\

 
\subsubsection*{Computazioni nei linguaggi funzionali}


Ora, per capire meglio come avviene una computazione nei linguaggi funzionali, e poter
quindi capire come questo tipo di computazione \`e formalizzata nel $\lambda$-calcolo, entriamo nel dettaglio della computazione\footnote{ovviamente quella presentata \`e una semplificazione a scopo didattico.} dell'espressione 
\begin{verbatim}
> inv "cbd"
\end{verbatim}

Indichiamo con $\leadsto_A$,  $\leadsto_B$ e $\leadsto_C$ differenti tipi di {\em passi di computazione}. La computazione corrispondente alla valutazione dell'espressione {\tt  inv "cbd"}
\`e descritta in Figura \ref{fig:comp}.

\begin{figure}
\hrule\hfill\\[-4.5mm]
\hrule
$$
\begin{array}{@{\hspace{-10mm}}rl}
              & \underline{{\tt inv}}\  \mbox{\tt "cbd"} \\[2mm]
& \mbox{- \em al posto di {\tt inv} mettiamo la funzione associata al nome {\tt inv} -}\\
\leadsto_A  & \underline{(\backslash \mbox {\tt y -> if (null y) then y
                        else (inv (tail y))++[head y])  "cbd"}}\\[2mm]
&  \mbox{- \em mettiamo il parametro attuale {\tt "cbd"} al posto del parametro formale {\tt y}}\\
 & \mbox{\ \ \em nel corpo della funzione -} \\
\leadsto_B  & \mbox {\tt  if \underline{(null "cbd")} then "cbd"
                        else (inv (tail "cbd"))++[head "cbd"]})\\[2mm]
 & \mbox{\em - calcolo della funzione predefinita {\tt null} -}\\
\leadsto_C  & \mbox {\tt \underline{if False then "cbd"
                        else (inv (tail "cbd"))++[head "cbd"]}})\\[2mm]
& \mbox{\em - valutazione dell'espressione {\tt if\ldots then\ldots else} -}\\
\leadsto_C  & \mbox {\tt (inv \underline{(tail "cbd")})++[head "cbd"]})\\[2mm]
& \mbox{\em - calcolo della funzione predefinita {\tt tail} -}\\

\leadsto_C  & \mbox {\tt (\underline{inv} "bd")++[head "cbd"]})\\[2mm]
& \mbox{- \em al posto di {\tt inv} mettiamo la funzione associata al nome {\tt inv} -}\\

\leadsto_A  & \mbox {\tt \underline{(($\backslash$y -> if (null y) then y
                        else (inv (tail y))++[head y])  "bd")}++[head "cbd"]})\\[3mm]
&  \mbox{- \em mettiamo il parametro attuale {\tt "bd"} al posto del parametro formale {\tt y}-}\\
\leadsto_B  & \mbox {\tt (if \underline{(null "bd")} then "bd"
                        else (inv (tail "bd"))++[head "bd"])++[head "cbd"])}\\[2mm]
\vdots\hspace{2mm} & \hspace{42mm}\vdots \\
\leadsto_C  & \mbox {\tt (if \underline{(null [])} then []
                        else (inv []) )++[head "d"]++[head "bd"]++[head "cbd"]}\\[2mm]
\leadsto_C  & \mbox {\tt \underline{(if True then []
                        else (inv []))}++[head "d"]++[head "bd"]++[head "cbd"]}\\[2mm]
\leadsto_C  & \mbox {\tt []++\underline{[head "d"]}++[head "bd"]++[head "cbd"]}\\[2mm]

&  \mbox{- \em valutazione della funzione predefinita {\tt head}-}\\
\leadsto_C  & \mbox {\tt \underline{[]++[d]}++[head "bd"]++[head "cbd"]}\\[2mm]

&  \mbox{- \em valutazione della funzione predefinita {\tt ++}-}\\
\leadsto_C  & \mbox {\tt [d]++\underline{[head "bd"]}++[head "cbd"]}\\[2mm]

\leadsto_C  & \mbox {\tt \underline{[d]++[b]}++[head "cbd"]}\\[2mm]

\leadsto_C  & \mbox {\tt [db]++\underline{[head "cbd"]}}\\[2mm]

\leadsto_C  & \mbox {\tt \underline{[db]++[c]}}\\[2mm]

\leadsto_C  & \mbox {\tt "bdc"}\\[2mm]
\end{array}
$$
\hrule\hfill\\[-4.5mm]
\hrule
\caption{Valutazione di {\tt  inv "bdc"}}
\label{fig:comp}

\end{figure}
\mbox{\em }
\begin{itemize}
\item
Il passo computazionale $\leadsto_A$ corrisponde a sostituire un nome con l'espressione associata ad esso.
\item
Il passo computazionale $\leadsto_B$ corrisponde a sostituire il parametro attuale\footnote{In una applicazione $(f\,  e)$, l'argomento $e$ viene chiamato {\em parametro attuale} della funzione $f$; mentre in una definizione di funzione, per esempio $f x = x+3$, il nome dell'argomento ($x$ nel nostro esempio), viene chiamato {\em parametro formale}.} di una funzione anonima al posto del parametro formale della funzione
all'interno del corpo della funzione stessa.
\item
Il passo computazionale $\leadsto_C$ corrisponde al calcolo di una funzione predefinita a cui abbiamo applicato un valore esplicito. 
\end{itemize}
\noindent
Notiamo come ogni passo computazionale nella Figura \ref{fig:comp} {\em trasformi} una sottoespressione. In Figura \ref{fig:comp} abbiamo infatti sottolineato le sottoespressioni trasformate dai vari passi di computazione.\\
In alcuni punti si potrebbe in realt\`a trasformare pi\`u di una sottoespressione. Per esempio
quando si arriva a\\ 
\centerline{\tt  if (null "cbd") then "cbd" else (inv (tail "cbd"))++[head "cbd"]}
potremmo trasformare non solo {\tt  (null "cbd")}, ma una qualsiasi delle seguenti sottoespressioni
sottolineate\\
\centerline{{\tt  if \underline{(null "cbd")} then "cbd" else (\underline{inv} \underline{(tail "cbd")})++[\underline{head "cbd"}]}}
Una {\em strategia di valutazione} \`e un algoritmo, una politica, che, quando in una espressione sono presenti
pi\`u sottoespressioni "tasformabili" (riducibili), sceglie quella da trasformare (ridurre).
Quello che distingue un linguaggio funzionale da un'altro sono soprattutto le loro strategie di valutazione. {\sf Haskell} utilizza una strategia chiamata {\em lazy}\footnote{questa strategia appartiene alla classe di strategie {\em call-by-name}.}, che riduce il sottotermine
la cui valutazione \`e indispensabile per arrivare al risultato.

Nella valutazione di una espressione, potremmo in realt\`a anche trasformare tutte le sottoespressioni riducibili, in parallelo. Questo \`e possibile nei linguaggi funzionali grazie alla mancanza di {\em side effects}, che sono invece presenti nei linguaggi di programmazione
imperativa, dove il risultato di una computazione pu\`o dipendere da effetti dovuti ad altre computazioni.
Per comprendere quanto affermato, prendiamo ad esempio il seguente schema di programma imperativo
\begin{verbatim}
BOOLEAN even := TRUE;   // variabile globale
:
PROCEDURE calculate (INTEGER value) : INTEGER;
BEGIN
 even := NOT even;
 IF even
  THEN   RETURN (value + 1)
  ELSE    RETURN (value + 2)
 ENDIF
END;
:
print(calculate (6));
:
print(calculate (6));
:
\end{verbatim}

Le due istruzioni di stampa sono identiche. Ma possono produrre risultati differenti. Pu\`o venire stampato il valore $7$, oppure $8$, e questo non dipende solo dall'argomento di {\tt calculate}, che \`e $6$ in entrambi i casi, o dal codice della procedura {\tt calculate}, che viene eseguito 
in entrambi i casi. Dipende dal valore della variabile globale {\tt even}, la cui modifica \`e un {\em side effect} della esecuzione di {\tt calculate}. Il valore restituito da {\tt calculate} dipende quindi anche dal numero di volte
che viene eseguito il suo codice.
Nella programmazione funzionale, invece, poich\'e le funzioni che definiamo sono vere funzioni
matematiche, il valore di una sottoespressione \`e sempre lo stesso, indipendentemente da dove si trova e da quante volte viene valutata. Questa propriet\`a dei linguaggi funzionali si chiama {\em referential transparency}. La presenza di side effects fa intuire perch\'e non \`e semplice comprendere cosa fa un programma imperativo o dimostrarne qualche propriet\`a. 
\bigskip

Tornando alle strategie di valutazione dei linguaggi funzionali, ci sono strategie che producono computazioni che non terminano quando si valutano espressioni che sembrano avere un valore.
Per esempio, consideriamo una strategia che in una applicazione di una funzione {\tt f} ad un argomento {\tt arg} valuta {\tt arg} (se questo non \`e un valore esplicito) prima di valutare {\tt (f arg)}\footnote{Strategie di questo tipo appartengono alla classe di strategie {\em call-by-value}.}. Seguendo tale strategia, valutiamo ora \\
\centerline{\tt (alwayseven (inf 3))}
dove le funzioni {\tt alwayseven} e {\tt inf} sono definite nel seguente modo:
\vspace{-1mm}
\begin{verbatim}
    alwayseven n = 7

    inf n = inf n 
\end{verbatim}
Se nella valutazione di {\tt (alwayseven (inf 3))} valutiamo prima {\tt (inf 3)}, otteniamo
ancora {\tt (alwayseven (inf 3))}, e cos\`i all'infinito.
Se invece valutiamo prima l'applicazione di  {\tt (inf 3)} ad {\tt alwayseven}, otteniamo subito il valore {\tt 7}.\\
 Quindi ci sono strategie che restituiscono il valore di espressioni che, se valutate con altre strategie, produrrebbero computazioni infinite. E' quindi naturale porsi la seguente domanda:
Se una strategia di valutazione produce il valore $v$ di un'espressione $e$, tutte le strategie che non comportano computazioni infinite restituiscono tutte $v$ come valore di $e$? Questa propriet\`a
\`e garantita dal Teorema di Confluenza del $\lambda$-calcolo, che studieremo.



\subsubsection*{Funzioni di ordine superiore}

Rispetto ai  linguaggi imperativi, i linguaggi funzionali trattano le funzioni come un qualsiasi valore manipolabile dal linguaggio. 
Come conseguenza, \`e  possibile definire funzioni che prendono altre funzioni come argomento o che restituiscono funzioni
come risultato. 
Questo genere di funzioni vengono chiamate solitamente ``funzioni di ordine superiore'' per distinguerle da
quelle che si utilizzano nei linguaggi non funzionali e che prendono come argomento - e restituiscono 
come risultato - solo elementi di tipi di dato che non sono funzioni.\\

Un banale esempio in Haskell di funzione che prende un altra funzione come argomento e' il seguente:

\begin{quote}
{\tt
atzero f = f 0
}
\end{quote}

{\tt atzero} prende come argomento una funzione e restituisce il valore di quest'ultima sul numero $0$.\\
Vediamo come Haskell valuta l'espressione {\tt (atzero square)}:\\

\noindent
\hspace{26pt}{\tt (atzero square)\\
$\leadsto_A$ (($\backslash$f -> (f 0)) square)\\
$\leadsto_B$ (square 0)\\
$\leadsto_A$ (($\backslash$n -> (n*n)) 0)\\
$\leadsto_B$ (0*0)\\
$\leadsto_C$ 0\\
}\\

\`E possibile definire funzioni in cui sia gli argomenti che i risultati sono funzioni.
Un semplicissimo esempio \`e la funzione {\tt compose}, che prende due funzioni (unarie) come argomenti 
e restituisce la loro composizione.

\begin{quote}
{\tt
compose f g = $\backslash$x -> (f (g x))
}
\end{quote}


Potremmo ora definire
\begin{quote}
{\tt
inc n = n+1
}
\end{quote}
e poi far valutare {\tt ((compose square inc) 3)}, ottenendo  {\tt 16}.\\
Oppure definire 
\begin{quote}
{\tt
squareinc = (compose square inc)
}
\end{quote}
ed utilizzare la funzione {\tt squareinc} tutte le volte che abbiamo bisogno di fare il quadrato dell'incremento di uno.\\

La possibilit\`a di definire funzioni di ordine superiore fornisce una grande flessibilit\`a ed espressivit\`a ai linguaggi funzionali.

\subsubsection*{Curryficazione}

La nozione di funzione di ordine superiore ci permette di introdurre quella di ``curryficazione'', utilizzata in molti linguaggi funzionali.
Curryficare  significa trasformare una funzione $$f : (A_1\times\ldots\times A_n) \rightarrow B$$

in una funzione di ordine superiore  
$$f_{C}: A_1\rightarrow (A_2 \rightarrow (\ldots \rightarrow (A_n\rightarrow B)..))$$

tale che 
$$ f(a_1,\ldots, a_n) = f_C(a_1)(a_2)\ldots(a_n)$$


In Haskell le funzioni che definiamo vengono considerate implicitamente curryficate.
Questo significa che potremmo definire {\tt compose} semplicemente nel seguente modo
\begin{quote}
{\tt
compose f g x = (f (g x))
}
\end{quote}
e comunque poter far valutare {\tt ((compose square inc) 3)} e  definire
\begin{quote}
{\tt
squareinc = (compose square inc)
}
\end{quote}

\`E importante notare che utilizzare le versioni currificate delle funzioni al posto delle funzioni stesse
non \`e limitativo, poich\`e ogni volta che ci servisse il valore di $ f(a_1,\ldots, a_n)$ potremmo utilizzare
$ f_C(a_1)(a_2)\ldots(a_n)$. 
Al contrario, avere le versioni curryficate delle funzioni fornisce maggiore flessibilit\`a
ad un linguaggio di programmazione. \\
Questo \`e il motivo per cui nel modello computazionale del $\lambda$-calcolo
le funzioni che si introducono hanno solo un argomento.Al posto di definire funzioni
a pi\`u argomenti, si possono definire, in modo equivalente, le loro versioni curryficate.


\subsubsection*{Uso dell'induzione per dimostrare propriet\`a di programmi
}
Abbiamo accennato prima alla propriet\`a di referencial transparency propria dei linguaggi
(puramente) funzionali.
Questa permette l'uso di tecniche matematiche per manipolare programmi (per esempio per ottimizzarli rispetto a particolari parametri) oppure per dimostrarne propriet\`a, come ad esempio la correttezza.\\

La ricorsione \`e alla base della potenza computazionale dei linguaggi di programmazione funzionali.
Si pu\`o notare come lo schema di una definizione ricorsiva di una funzione sia analogo a quello utilizzato nelle dimostrazioni
matematiche per induzione. 
Infatti in un programma ricorsivo l'output e' definito per gli elementi di base e
poi \`e definito per un input generico
assumendo che il programma funzioni correttamente su elementi pi\`u ``piccoli'' (``semplici'') dell'input generico.\\
Similmente, in una dimostrazione matematica per induzione, la propriet\`a in oggetto  \`e dimostrata per
il caso base (solitamente $0$) e poi  per il caso generale assumendo che valga per numeri pi\`u piccoli.

Il principio di induzione \`e una regola logica che per\`o, implicitamente, ``rappresenta'' anche un metodo di calcolo,
e nella programmazione funzionale corrisponde alla definizione di funzioni numeriche per ricorsione,
come il programma Haskell per il fattoriale visto in precedenza.\\

La stretta corrispondenza tra programmi ricorsivi e principio di induzione rende possibile
l'uso di quest'ultimo per dimostrare propriet\`a di programmi ricorsivi.
Possiamo usare l'induzione per esempio per dimostrare la seguente affermazione relativa alla funzione Haskell {\tt fact}:
\begin{quote} 
{\em Per ogni input {\tt n} il calcolo (la valutazione) di {\tt (fact n)} termina.}
\end{quote}
Basta infatti mostrare che 
\begin{enumerate}
\item
la valutazione di {\tt (fact 0)} termina;
\item
per un generico {\tt k} $> 0$, la valutazione di {\tt (fact k)} termina, utilizzando l'ipotesi induttiva
che {\tt (fact (k-1))} termini.
\end{enumerate}

\noindent
Prendiamo quindi il programma che calcola il fattoriale e vediamo che
\begin{enumerate}
\item
la valutazione di {\tt (fact 0)} termina, poiche' corrisponde immediatamente a restituire $0$;
\item
se  {\tt k} $> 0$, la valutazione di {\tt (fact k)} corrisponde a valutare il ramo {\tt else } e quindi a valutare
l'espressione {\tt (k*(fact (k-1)))}. 
Poich\`e per ipotesi induttiva la valutazione di {\tt(fact (k-1))}
termina, e poich\`e il calcolo della sottrazione e della moltiplicazione su due numeri banalmente termina, 
l'intera valutazione dell'espressione {\tt (fact k)} termina.\\
\end{enumerate}

\noindent
Per poter dimostrare propriet\`a di programmi che lavorano su strutture dati complesse
avremo ovviamente necessit\`a di utilizzare strumenti matematici pi\`u sofisticati, come ad esempio
il principio di {\bf induzione ben-fondata} (vedi {\bf [VS]}).


\subsubsection*{Preludio al $\lambda$-calcolo}

Se il modello computazionale del $\lambda$-calcolo \`e il fondamento teorico dei linguaggi
di programmazione funzionale esso dovr\`a formalizzare gli elementi che
costituiscono il minimo indispensabile per definire funzioni.\\


Gli elementi costitutivi della programmazione funzionale che abbiamo visto sono:
variabili, costanti, funzioni base, applicazione funzionale, astrazione funzionale, definizione di funzioni ricorsive (associando nomi ad espressioni) ed i passi computazionali $\leadsto_A$, $\leadsto_B$ e $\leadsto_C$. Tali elementi sembrano tutti indispensabili. In realt\`a non lo sono!
 Alcuni sono rappresentabili utilizzando gli altri e quindi possiamo 
evitare di prenderli in considerazione in un modello computazionale, che deve formalizzare solo l'{\em essenza}
del significato di {\em computazione}.

In particolare, {\em costanti}, {\em funzioni base}, {\em definizioni ricorsive} e i passi computazionali  $\leadsto_A$ e $\leadsto_C$, si possono tutti definire in termini esclusivamente di
{\em variabili}, {\em applicazione}, {\em astrazione funzionale} e passo computazionale $\leadsto_B$\footnote{La cosa che sembra impossibile \`e definire funzioni ricorsive senza
poter dare nomi ad espressioni. Eppure si pu\`o. Con i pochi elementi indicati si pu\`o, in un certo senso, rappresentare in concetto stesso di {\em ricorsione}.}. Il modello computazionale del $\lambda$-calcolo \`e un formalismo
estremamente semplice. E questa semplicit\`a si riflette sul fatto che programmare nei linguaggi
funzionali \`e relativamente semplice, cos\`i come dimostrare propriet\`a di programmi scritti in tali linguaggi.\\



Nel $\lambda$-calcolo le variabili sono rappresentate da un insieme infinito di elementi $x$, $y$, $z,\ldots$. Le variabili sono $\lambda$-termini. L'applicazione \`e rappresentata con 
l'operatore $'\cdot'$. L'applicazione di due $\lambda$-termini $M$ e $N$ \`e anch'essa un $\lambda$-termine, $(M\cdot N)$ (di solito si scrive semplicemente $(MN)$. L'astrazione funzionale di un $\lambda$-termine $M$ rispetto ad una variabile $x$ \`e anch'essa un $\lambda$-termine, $\lambda x.M$. I $\lambda$-termini formalizzano il concetto di espressione della 
programmazione funzionale (sappiamo che le funzioni anonime sono anch'esse espressioni e che
possono essere argomenti di funzioni o possono venir restituite come output di funzioni).\\
Il passo di computazione $\leadsto_B$ \`e formalizzato dalla relazione di $\beta$-riduzione 
$$(\lambda x.M)N \rightarrow_\beta M[N/x]$$
dove $M$, ed $N$ possono essere $\lambda$-termini qualsiasi e dove $[N/x]$ indica la
sostituzione del parametro attuale $N$ al posto del parametro formale $x$ nel corpo $M$
della funzione anonima.


Un passo di computazione nel $\lambda$-calcolo corrisponde a trasformare un $\lambda$-termine
contenente un sottotermine della forma $(\lambda x.M)N$ nello stesso $\lambda$-termine, ma in cui 
al posto di $(\lambda x.M)N$  c'\`e $M[N/x]$.

Dopo questo breve preludio, si pu\`o iniziare a studiare il $\lambda$-calcolo.












\end{document}