Algoritmo di inferenza

Per determinare se un termine è ben tipato o meno si procede cercando di costruire un albero di derivazione ma, nel farlo, non ci è sempre chiaro come procedere in maniera sistematica, come abbiamo visto nell’esempio di prima. Ecco che quindi vogliamo costruire un algoritmo che ci permetta di farlo sistematicamente: l’algoritmo di inferenza.

L’idea generale dell’algoritmo di inferenza è la seguente: innanzitutto ci dotiamo di un sistema grafico che ci permetta di operare facilmente sulle ${\lambda }_{\text{Bool}}^{\to }$-espressioni, quindi proviamo a “intuire” quali tipi potremmo assegnare ai sotto-termini della ${\lambda }_{\text{Bool}}^{\to }$-espressione, creando dei collegamenti che ci permettano di porli in relazione tra di loro, e infine proviamo a trovare una soluzione.

Fase 1 dell’algoritmo

Come già detto, per il primo passo di questo algoritmo di inferenza ci serve un modo “visivamente comodo” per rappresentare le ${\lambda }^{\to }$-espressioni. Per farlo, scegliamo una struttura ad albero esattamente come abbiamo fatto per l’albero di derivazione, infatti questa nuova struttura sarà facilmente “traducibile” poi in un albero di derivazione proprio perché sono entrambi della forma ad albero.

Questa struttura verrà chiamata albero sintattico.

Definizione: albero sintattico

Data una ${\lambda }_{\text{Bool}}^{\to }$-espressione $T$, l’albero sintattico $\text{Tree}[T]$ è una struttura ad albero definita induttivamente sulla forma sintattica del termine $T$:

1. Se $T$ è un termine della forma di una variabile $x$, allora $\text{Tree}[T]=\text{Tree}[x]$ sarà:
2. Se $T$ è un termine della forma di una costante $c$, allora $\text{Tree}[T]=\text{Tree}[c]$ sarà:
3. Se $T$ è un termine della forma di un’astrazione $\lambda x.M$, allora $\text{Tree}[T]=\text{Tree}[\lambda x.M]$ sarà:
4. Se $T$ è un termine della forma di un’applicazione $MN$, allora $\text{Tree}[T]=\text{Tree}[MN]$ sarà:
5. Se $T$ è un termine della forma di una struttura di controllo $\text{if}cMN$, allora $\text{Tree}[T]=\text{Tree}[\text{if}cMN]$ sarà:

Esempio di albero sintattico

Ecco un esempio di albero sintattico della ${\lambda }_{\text{Bool}}^{\to }$-espressione $(\lambda x.x)\text{True}$:

Esercizio 1 di costruzione di un albero sintattico

Costruisci l’albero sintattico della ${\lambda }_{\text{Bool}}^{\to }$-espressione $\lambda x.\lambda y.\lambda z.\text{False}z(xy)$.

Esercizio 2 di costruzione di un albero sintattico

Costruisci l’albero sintattico della ${\lambda }_{\text{Bool}}^{\to }$-espressione $\text{if}\text{True}(\lambda x.x)(\lambda x.\lambda y.y)$.

Fase 2 dell’algoritmo

Dopo aver costruito l’albero sintattico, si fa una visita dell’albero usando la strategia bottom-up (quindi partendo dalle foglie e arrivando alla radice): ogni nodo viene “annotato” con un’espressione di tipo, ossia delle “etichette” che ci aiutano a intuire quale tipo potrebbe assumere quel nodo.

Definizione: espressione di tipo

Sia $\text{TVar}=\{\alpha ,\beta ,\gamma ,\dots \}$ l’insieme infinito di variabili di tipo.

Un’espressione di tipo $\tau$ è un’etichetta assegnata a un nodo dell’albero sintattico che corrisponde a una stringa ben formata a partire dalla seguente grammatica espressa in BNF:

$$\tau ::=\alpha \mid \text{Bool}\mid \tau \to \tau$$

dove:

• $\alpha$ è una variabile di tipo per un tipo ancora sconosciuto.
• $\text{Bool}$ è il tipo booleano.
• $\tau \to \tau$ è il tipo funzione.

Per determinare delle “relazioni” tra le varie espressioni di tipo usiamo dei vincoli che devono essere rispettati affinché la ${\lambda }_{\text{Bool}}^{\to }$-espressione sia ben tipata.

Definizione: vincolo

Un vincolo è una relazione di uguaglianza tra due espressioni di tipo $\tau$ e $\sigma$:

$$\tau =\sigma$$

Proviamo quindi a capire come annotare le espressioni di tipo sull’albero sintattico distinguendo tra i vari casi.

Nel caso di un termine della forma di una variabile $x$, nel nodo $x$ ci annotiamo un segnaposto $\alpha$, avendo cura di usare lo stesso segnaposto $\alpha$ per tutte le occorrenze di $x$ e solo per quelle:

Nel caso di un termine della forma di una costante $c$, nel nodo $c$ ci annotiamo il tipo booleano $\text{Bool}$:

Nel caso di un termine della forma di un’astrazione $\lambda x.M$, partendo dal basso (perché stiamo usando la strategia bottom-up):

• Dal sotto-albero $\text{Tree}[M]$ avremo ottenuto un’espressione di tipo $\tau$.
• Nel nodo $\lambda x$ ci annotiamo un tipo funzione $\alpha \to \tau$, dove $\alpha$ è un segnaposto (e, per ogni occorrenza di $x$ in $M$, dovremo usare sempre lo stesso segnaposto $\alpha$) e $\tau$ è l’espressione di tipo del sotto-albero $\text{Tree}[M]$.

Il risultato è il seguente:

Nel caso di un termine della forma di un’applicazione $MN$, partendo sempre dal basso (perché stiamo usando la strategia bottom-up):

• Dal sotto-albero $\text{Tree}[M]$ avremo ottenuto un’espressione di tipo $\tau$ (dove $\tau$ è diverso dal $\tau$ usato nell’astrazione $\lambda x.M$, perché questi due sotto-termini $M$ non sono la stessa cosa).
• Dal sotto-albero $\text{Tree}[N]$ avremo ottenuto un’espressione di tipo $\sigma$.
• Nel nodo $@$ ci annotiamo un nuovo segnaposto $\alpha$.
• Generiamo un nuovo vincolo $\tau =\sigma \to \alpha$.

Il risultato è il seguente:

In particolare, se $\text{Tree}[M]$ è di un certo tipo funzione ${\tau }_1\to {\tau }_2$, allora il nodo $@$ ha tipo ${\tau }_2$ e il vincolo generato è ${\tau }_1=\sigma$:

Nel caso di un termine della forma di una struttura di controllo $\text{if}cMN$:

• Dal sotto-albero $\text{Tree}[c]$ avremo ottenuto un’espressione di tipo ${\tau }_1$.
• Dal sotto-albero $\text{Tree}[M]$ avremo ottenuto un’espressione di tipo ${\tau }_2$.
• Dal sotto-albero $\text{Tree}[N]$ avremo ottenuto un’espressione di tipo ${\tau }_3$.
• Generiamo il vincolo che richiede che il tipo di $c$ sia booleano: ${\tau }_1=\text{Bool}$.
• Generiamo il vincolo che richiede che il tipo di ${\tau }_2$ e di ${\tau }_3$ coincida: ${\tau }_2={\tau }_3$.
• Nel nodo $\text{if}$ ci annotiamo il tipo ${\tau }_2$ ($={\tau }_3$), che sarà proprio il tipo che restituisce la struttura di controllo.

Il risultato è il seguente:

Fase 3 dell’algoritmo

Nella terza fase dell’algoritmo di inferenza, una volta che l’albero sintattico è stato annotato, si cerca di capire se questo insieme di vincoli ammette una soluzione e si cerca di trovare quella generale da cui derivare tutte le altre.

All’inizio della terza fase ci ritroviamo con un sistema di $n$ vincoli:

$$\text{Sys}=\{{\tau }_i={\sigma }_i{\}}_{1\le i\le n}$$

Per risolvere questo sistema usiamo un algoritmo di risoluzione.

Algoritmo di risoluzione

Dato un sistema di $n$ vincoli $\text{Sys}=\{{\tau }_i={\sigma }_i{\}}_{1\le i\le n}$, l’algoritmo di risoluzione permette di risolvere $\text{Sys}$, ottenendo un successo o un fallimento.

I passi da seguire sono i seguenti:

1. Per ogni vincolo ${\tau }_i={\sigma }_i\in \text{Sys}$, verificare se nella seguente tabella il vincolo rispetta una delle seguenti forme e condizioni e, eventualmente, eseguire la trasformazione indicata:

Forma del vincolo	Condizione	Cosa fare
$\tau =\tau$	$\tau$ è un’espressione di tipo qualsiasi	Eliminare il vincolo
$\tau =\alpha$	$\tau$ è un’espressione di tipo qualsiasi e $\alpha$ è un segnaposto	Rimpiazzare il vincolo con $\alpha =\tau$
$\tau \to {\tau }^{\prime }=\sigma \to {\sigma }^{\prime }$	$\tau$ e $\sigma$ sono due espressioni di tipo qualsiasi	Rimpiazzare il vincolo con $\tau =\sigma$ e ${\tau }^{\prime }={\sigma }^{\prime }$
$\tau \to \sigma =\text{Bool}$	$\tau$ e $\sigma$ sono due espressioni di tipo qualsiasi, $\text{Bool}$ è il tipo booleano	L’algoritmo fallisce per errore di tipo
$\text{Bool}=\tau \to \sigma$	$\tau$ e $\sigma$ sono due espressioni di tipo qualsiasi, $\text{Bool}$ è il tipo booleano	L’algoritmo fallisce per errore di tipo
$\alpha =\tau$	$\tau$ è un’espressione di tipo qualsiasi, $\alpha$ è un segnaposto e $\alpha$ compare in $\tau$	L’algoritmo fallisce per errore di occorrenza
$\alpha =\tau$	$\tau$ è un’espressione di tipo qualsiasi, $\alpha$ è un segnaposto e $\alpha$ non compare in $\tau$	Rimpiazzare le occorrenze di $\alpha$ con $\tau$ in tutti gli altri vincoli e lasciando questo invariato

2. Ripetere il passo 1 finché non si ottiene un fallimento dell’algoritmo o finché non è più possibile applicare le trasformazioni indicate.
3. Se non è avvenuto un fallimento dell’algoritmo, allora ha avuto successo e si è risolto il sistema $\text{Sys}$.

Osservazione: invarianza dell'ordine delle trasformazioni

L’ordine in cui si applicano le trasformazioni del passo 1 dell’algoritmo di risoluzione non influisce sul risultato.

Con il successo dell’algoritmo di risoluzione, avremo ottenuto un nuovo sistema di $n^{\prime }$ vincoli

$${\text{Sys}}^{\prime }=\{{\alpha }_i={\rho }_i{\}}_{1\le i\le n^{\prime }}$$

dove ogni ${\alpha }_i$ è un segnaposto (che compare una sola volta nel sistema) corrispondente esattamente a un tipo che sarà uguale a un’espressione di tipo ${\rho }_i$.

A questo punto non ci rimane altro che fare una sostituzione di ogni ${\alpha }_i$ con il rispettivo ${\rho }_i$.

Definizione: sostituzione

Nell’algoritmo di inferenza, una sostituzione $\theta$ è una funzione da variabili di tipo a espressioni di tipo in cui, dato un tipo $\tau$, sostituiamo in $\tau$ ogni occorrenza di ogni sotto-tipo $\alpha$ con la sostituzione $\theta (\alpha )$.

Da questa sostituzione otteniamo una possibile soluzione dell’algoritmo di inferenza.

Definizione: soluzione

Nell’algoritmo di inferenza, dato un sistema di $n$ vincoli $\{{\tau }_i={\sigma }_i{\}}_{1\le i\le n}$ e una sostituzione $\theta$, diciamo che $\theta$ è una soluzione (o unificatore) del sistema se, per ogni $1\le i\le n$:

$$\theta ({\tau }_i)=\theta ({\sigma }_i)$$

Attenzione: differenza tra gli $=$ nella definizione di soluzione

Nella definizione di soluzione, i due $=$ che compaiono rispettivamente nel sistema di $n$ vincoli $\{{\tau }_i={\sigma }_i{\}}_{1\le i\le n}$ e nella relazione di uguaglianza $\theta ({\tau }_i)=\theta ({\sigma }_i)$ non significano la stessa cosa: mentre nel primo caso serve solo come “promemoria” per ricordarsi di come sono “collegate” tra di loro le espressioni di tipo, nel secondo indica una vera e propria uguaglianza tra i risultati delle sostituzioni.

In particolare, usando l’algoritmo di risoluzione per “ridurre al minimo” il sistema di vincoli, otterremo non una soluzione qualsiasi ma la soluzione più generale, che ci permette di ricavare a partire da essa tutte le altre possibili soluzioni.

Definizione: soluzione più generale

Nell’algoritmo di inferenza, dato un sistema di $n$ vincoli $\{{\tau }_i={\sigma }_i{\}}_{1\le i\le n}$ e una soluzione $\theta$, diciamo che $\theta$ è la soluzione più generale (o unificatore più generale) del sistema se ogni soluzione del sistema è ottenibile componendo $\theta$ con un’altra sostituzione.

Definizione dell’algoritmo

Dopo aver esplicitato il funzionamento dell’algoritmo di inferenza attraverso le 3 fasi di cui si compone, possiamo finalmente dichiararlo formalmente.

Algoritmo di inferenza

Data una ${\lambda }_{\text{Bool}}^{\to }$-espressione $T$, l’algoritmo di inferenza permette di inferire il tipo di $T$.

I passi da seguire sono i seguenti:

1. Costruire l’albero sintattico $\text{Tree}[T]$.
2. Su ogni nodo dell’albero sintattico $\text{Tree}[T]$ annotare delle espressioni di tipo e generare i rispettivi vincoli seguendo questa tabella:

Contenuto del nodo	Cosa annotare	Vincoli da generare	Risultato sull’albero sintattico
Termine della forma di una variabile $x$	Nel nodo $x$: un segnaposto $\alpha$, avendo cura di usare lo stesso segnaposto $\alpha$ per tutte le occorrenze di $x$ e solo per quelle
Termine della forma di una costante $c$	Nel nodo $c$: il tipo booleano $\text{Bool}$
Termine della forma di un’astrazione $\lambda x.M$	Nel nodo $\lambda x$: un tipo funzione $\alpha \to \tau$, dove $\alpha$ è un segnaposto (e, per ogni occorrenza di $x$ in $M$, dovremo usare sempre lo stesso segnaposto $\alpha$) e $\tau$ è l’espressione di tipo del sotto-albero $\text{Tree}[M]$
Termine della forma di un’applicazione $MN$ con $\text{Tree}[M]$ con espressione di tipo $\tau$ qualsiasi	Nel nodo $@$: un segnaposto $\alpha$	$\tau =\sigma \to \alpha$, dove $\tau$ è l’espressione di tipo del sotto-albero $\text{Tree}[M]$ e $\sigma$ è l’espressione di tipo del sotto-albero $\text{Tree}[N]$
Termine della forma di un’applicazione $MN$ con $\text{Tree}[M]$ con espressione di tipo ${\tau }_1\to {\tau }_2$	Nel nodo $@$: il tipo ${\tau }_2$	${\tau }_1=\sigma$, dove $\sigma$ è l’espressione di tipo del sotto-albero $\text{Tree}[N]$
Termine della forma di una struttura di controllo $\text{if}cMN$	Nel nodo $\text{if}$: il tipo ${\tau }_2$, dove ${\tau }_2$ è l’espressione di tipo del sotto-albero $\text{Tree}[M]$	${\tau }_1=\text{Bool}$, dove ${\tau }_1$ è l’espressione di tipo del sotto-albero $\text{Tree}[c]$ ${\tau }_2={\tau }_3$, dove ${\tau }_2$ è l’espressione di tipo del sotto-albero $\text{Tree}[M]$ e ${\tau }_4$ è l’espressione di tipo del sotto-albero $\text{Tree}[N]$

3. Sul sistema di $n$ vincoli $\text{Sys}=\{{\tau }_i={\sigma }_i{\}}_{1\le i\le n}$ usare l’algoritmo di risoluzione.
4. Se l’algoritmo di risoluzione ha fallito, allora la ${\lambda }_{\text{Bool}}^{\to }$-espressione non è ben tipata.
5. Se l’algoritmo di risoluzione ha avuto successo, effettuare su ogni vincolo del nuovo sistema ${\text{Sys}}^{\prime }=\{{\alpha }_i={\rho }_i{\}}_{1\le i\le n^{\prime }}$ la sostituzione.
6. Il risultato del passo 5 è la soluzione più generale del sistema.

Estensioni dell’algoritmo

L’algoritmo di inferenza può essere esteso a versioni del ${\lambda }_{\text{Bool}}^{\to }$-calcolo con ulteriori tipi.

Estensione con i numeri interi

Possiamo, per esempio, aggiungere tra i tipi anche i numeri interi $\mathbb{Z}$, sotto forma del tipo $\text{Int}$:

$$\tau ::=\text{Bool}\mid \text{Int}\mid \tau \to \tau$$

Di conseguenza, nella definizione del termine basterà specificare che le costanti $c$ potranno assumere come valori anche i numeri interi $\mathbb{Z}$:

$$c\in \{\text{True},\text{False},0,1,-1,2,-2,\dots \}$$

e, nella forma sintattica della struttura di controllo $\text{if}cMN$, $c$ potrà assumere solo i valori $\text{True}$ e $\text{False}$.

Nell’algoritmo di inferenza non si notano particolari differenze, ma:

• Tra le espressioni di tipo, annoverare tra le possibili forme anche $\text{Int}$.
• Nella tabella di generazione dei vincoli, specificare che ai termine della forma di una costante $c$ va assegnato il tipo giusto a seconda del valore che assume, quindi: $$c:\{\begin{array}{ll}\text{Bool}& \text{se }c\in \{\text{True},\text{False}\}\\ \text{Int}& \text{se }c\in \{0,1,-1,2,-2,\dots \}\end{array}$$
• Nell’algoritmo di risoluzione, aggiungere che, se c’è un vincolo della forma $$\tau \to \sigma =\text{Int}$$ o $$\text{Int}=\tau \to \sigma$$ o $$\text{Int}=\text{Bool}$$ o $$\text{Bool}=\text{Int}$$ allora l’algoritmo fallisce per errore di tipo.

Estensione con le liste

Questa volta, tra i tipi annoveriamo anche le liste, costituite da elementi di tipo $\tau$:

$$\tau ::=\text{Bool}\mid \text{Int}\mid \tau \to \tau \mid [\tau ]$$

Ovviamente, ciò implica che anche tra le espressioni di tipo dobbiamo annoverare tra le possibili forme anche $[\tau ]$.

Nei valori possibili che può assumere un termine-costante, ci includiamo i due costruttori canonici delle liste, la lista vuota $[]$ e il cons $(:)$:

$$c\in \{\text{True},\text{False},0,1,-1,2,-2,\dots ,[],(:)\}$$

In particolare, in Haskell il costruttore lista vuota $[]$ ha tipo $[\alpha ]$ e il costruttore cons $(:)$ ha tipo $\alpha \to [\alpha ]\to [\alpha ]$:

$$\begin{array}{c}[]::[\alpha ]\\ (:)::\alpha \to [\alpha ]\to [\alpha ]\end{array}$$

Tenendo conto che nella stessa ${\lambda }_{\text{Bool}}^{\to }$-espressione possiamo costruire liste di elementi di tipo diverso (per esempio, possono coesistere in una ${\lambda }_{\text{Bool}}^{\to }$-espressione una lista di tipo $[\text{Int}]$ e una lista di tipo $[\text{Bool}]$), abbiamo che le costanti dei costruttori canonici delle liste (cioè $[]$ e $(:)$) devono essere interpretate come costanti polimorfe, cioè in ogni loro occorrenza possono assumere tipo diverso.

Per questo motivo, nella fase di generazione dei vincoli dell’algoritmo di inferenza, per ogni occorrenza di uno di questi due costruttori dobbiamo stare attenti ad annotare nel nodo tipi che usano segnaposti freschi: se, per esempio, in un nodo trovo $[]$, lo annoto come una lista di elementi che hanno come tipo un segnaposto $\alpha$; se lo troverò una seconda volta, lo annoterò come una lista di elementi che hanno come tipo un segnaposto $\beta$ e così via:

$$\begin{array}{c}[]:[\alpha ]\\ \lambda x:\tau \to \sigma \\ \dots \\ []:[\beta ]\end{array}$$

Per quanto riguarda la fase di risoluzione dei vincoli, se abbiamo vincoli che impongono l’uguaglianza di tipi che hanno forme palesemente diverse (per esempio $[\tau ]=\text{Bool}$, $\text{Bool}=[\tau ]$ o $[\tau ]={\sigma }_1\to {\sigma }_2$) allora l’algoritmo fallisce per errore di tipo.

Abbiamo anche un caso analogo a quello dei tipi funzioni in cui possiamo semplificare l’uguaglianza di due funzioni ($\tau \to {\tau }^{\prime }=\sigma \to {\sigma }^{\prime }$) imponendo l’uguaglianza dei domini e dei codomini ($\tau =\sigma$ e ${\tau }^{\prime }={\sigma }^{\prime }$): se c’è un vincolo $[\tau ]=[\sigma ]$ allora possiamo rimpiazzarlo con $\tau =\sigma$.

Estensione con funzioni di libreria

In generale, possiamo estendere l’algoritmo di inferenza assumendo che nelle espressioni da tipare compaiano le funzioni della libreria standard di Haskell (es. id, head, tail, …), che potranno essere funzioni polimorfe (ossia il loro tipo non è un tipo specifico ma è una variabile di tipo) e per trattarle in questo modo va fatto come abbiamo appena fatto per le liste: ogni occorrenza deve usare nuove variabili di tipo (segnaposti) per ogni occorrenza.

Estensione con definizioni ricorsive

Potremmo volere stabilire il tipo di una definizione ricorsiva della forma

$$f=M$$

dove $f$ può comparire in $M$.

Quel che dobbiamo fare è aggiungere il vincolo $\alpha =\tau$ dove $\alpha$ è la variabile di tipo associata a $f$ e $\tau$ è l’annotazione di $M$.

---

Fonti

• 🏫 Corso di Laurea in Informatica (L-31 R) presso l’Università di Torino:
  • Corso di Linguaggi e Paradigmi di Programmazione, A.A. 2020-21 (pagina Moodle):
    • Prof. Luca Padovani, slide del corso:
      • Algoritmo di inferenza (fase 1).
      • Algoritmo di inferenza (fase 2).
      • Algoritmo di inferenza (fase 3).
      • Algoritmo di inferenza (estensioni).
    • Prof. Luca Padovani, videoregistrazioni del corso:
      • Algoritmo di inferenza (fase 1).
      • Algoritmo di inferenza (fase 2).
      • Algoritmo di inferenza (fase 3).
      • Algoritmo di inferenza (estensioni).
  • Corso di Linguaggi e Paradigmi di Programmazione, A.A. 2025-26 (pagina Moodle):
    • Prof. Viviana Bono, lezioni del corso.
• 🌐 Lambda-calcolo su Wikipedia in lingua italiana, URL consultato l’ultima volta e archiviato il 25 novembre 2025.
• 🌐 Simply typed lambda calculus su Wikipedia in lingua inglese, URL consultato l’ultima volta e archiviato il 25 novembre 2025.
• 🧠 Consultazione di ChatGPT.