Premessa

Ciao! Se è la prima volta che capiti su questo sito, ti consiglio di consultare la pagina principale di questo cosiddetto Giardino Digitale per scoprire meglio cos’è e come navigarlo.

Lo stato di questa nota è al momento: 🔴 Bozza.

---

Dal momento che il $\lambda$-calcolo è computazionalmente completo, abbiamo visto come è possibile con esso creare con esso dei veri e propri programmi, semplicemente codificando in termini determinati costrutti della programmazione classica (come abbiamo fatto, per esempio, con la codifica di Church).

Tuttavia, possiamo subito notare un problemino non trascurabile: nella codifica di Church, possiamo tranquillamente scrivere $\lambda$-espressioni che da un punto di vista puramente sintattico hanno senso, ma semanticamente no.

Per esempio, possiamo fare un’addizione tra due valori booleani:

$$\text{ADD}\text{TRUE}\text{FALSE}$$

Però questa $\lambda$-espressione, da un punto di vista semantico, non ha senso: cosa dovrebbe significarci la somma di due valori booleani?

Allo stesso modo, possiamo provare a fare una disgiunzione logica tra due numerali di Church:

$$\text{OR}\underline{3}\underline{2}$$

Ma cosa vuole dire questa $\lambda$-espressione?

Proprio per questo motivo, ci serve in qualche modo discriminare sulla forma che vogliamo che abbiano i nostri termini quando andiamo a usarli: ecco che quindi importiamo direttamente dal mondo della programmazione la classica nozione di tipo per espandere il $\lambda$-calcolo e crearne sue versioni “tipizzate”, come il $\lambda$-calcolo semplicemente tipizzato.

Definizione: $\lambda$-calcolo semplicemente tipizzato

Il $\lambda$-calcolo semplicemente tipizzato (spesso indicato anche come ${\lambda }^{\to }$-calcolo o con l’acronimo STLC, dall’inglese Simply Typed Lambda Calculus), è un’espansione del $\lambda$-calcolo che include i tipi.

Questi tipi non sono altro che semplici “etichette” che decidiamo noi di assegnare ai termini per distinguere l’uso che dobbiamo farne di loro nelle nostre $\lambda$-espressioni.

Nel ${\lambda }^{\to }$-calcolo vogliamo distinguere i termini solo in due categorie: quelli che rappresentano dati atomici (come numeri, valori booleani, stringhe, ecc.) e quelli che rappresentano funzioni che, dato un termine di un certo tipo, restituiscono un altro termine di un altro tipo.

Definizione: tipo nel ${\lambda }^{\to }$-calcolo

Nel ${\lambda }^{\to }$-calcolo, un tipo $\tau$ è un’etichetta assegnata a un termine che corrisponde a una stringa ben formata a partire dalla seguente grammatica espressa in BNF:

$$\tau ::=\alpha \mid \tau \to \tau$$

dove:

• $\alpha$ è il tipo atomico, ossia un tipo non ulteriormente riducibile.
• $\tau \to \tau$ è il tipo funzione, ossia un tipo che indica che un’astrazione prende come argomento un termine di tipo $\tau$ e restituisce un termine di tipo $\tau$.
  

Esempi di tipi

Esempi di tipo atomico sono $\text{Bool}$ e $\text{Nat}$, da assegnare a termini che rappresentano rispettivamente valori booleani e numeri naturali.

Un esempio invece di tipo funzione è $\text{Nat}\to \text{Bool}$, da assegnare a un’astrazione che prende come argomento un termine di tipo atomico $\text{Nat}$ e restituisce un termine di tipo atomico $\text{Bool}$. Per esempio, nella codifica di Church c’è il test per zero che prende come argomento un numerale di Church (che rappresenta un numero naturale) e restituisce un valore booleano.

Ecco che quindi possiamo ridefinire il termine per includere al suo interno le costanti, che ci aiuteranno a rappresentare i tipi atomici.

Definizione: termine nel ${\lambda }^{\to }$-calcolo

Nel ${\lambda }^{\to }$-calcolo, un termine $T$ (anche detto ${\lambda }^{\to }$-termine o ${\lambda }^{\to }$-espressione) è una stringa ben formata a partire dalla seguente grammatica espressa in BNF:

$$T::=x\mid c\mid (\lambda x.T)\mid (TT)$$

dove:

1. $x$ è una variabile,
2. $c$ è una costante,
3. $(\lambda x.T)$ è un’astrazione con argomento $x$ e corpo $T$ e
4. $(TT)$ è un’applicazione in cui la funzione $T$ viene applicata all’argomento $T$.

Ognuna di queste 4 forme che può assumere un termine è detta forma sintattica.

Nel $\lambda$-calcolo semplicemente tipizzato, l’avverbio semplicemente indica che, a differenza di altri varianti tipizzate del $\lambda$-calcolo, in questa decidiamo di adottare solamente il tipo atomico e il tipo funzione e nient’altro.

1 - Giudizi sui tipi

Il motivo per cui abbiamo introdotto questa nozione di tipi è per determinare se un termine, oltre a essere sintatticamente corretto, lo è anche dal punto di vista semantico.

Questo lo controlleremo attraverso dei giudizi, ossia proposizioni logiche in cui affermiamo che un termine $M$ ha tipo $t$ e le esprimeremo nella seguente notazione:

$$⊢M:t$$

C’è solo un problemino: questo termine $M$ potrebbe contenere al proprio interno delle variabili libere e, di conseguenza, per capire qual è il tipo da assegnare a queste variabili non ci basta più il solo termine $M$ ma ci serve un contesto che ci aiuti a capirlo, sotto forma di una funzione parziale che associa a ogni variabile che usiamo nel termine un tipo.

Definizione: contesto

Nel ${\lambda }^{\to }$-calcolo, un contesto $\Gamma$ è una funzione parziale da variabili a tipi:

$$\Gamma :\{x,y,z,\dots \}\rightharpoonup \{\alpha ,\tau \to \sigma \}$$

Ora abbiamo tutti gli strumenti per definire formalmente un giudizio.

Definizione: giudizio

Nel ${\lambda }^{\to }$-calcolo, un giudizio è una proposizione logica che asserisce che, dati dei contesti ${\Gamma }_1,{\Gamma }_2,\dots ,{\Gamma }_n$, un termine $M$ ha tipo $t$:

$${\Gamma }_1,{\Gamma }_2,\dots ,{\Gamma }_n⊢M:t$$

dove ${\Gamma }_1,{\Gamma }_2,\dots ,{\Gamma }_n$ indica l’unione dei contesti ${\Gamma }_1,{\Gamma }_2,\dots ,{\Gamma }_n$:

$$\bigcup _{i=1}^n{\Gamma }_i$$

Il giudizio può anche non avere contesti se $M$ è un combinatore:

$$⊢M:\tau$$

Esempio di giudizio

Il giudizio

$$\Gamma ⊢x:\text{Bool}$$

indica che la variabile $x$, nel contesto $\Gamma$, ha tipo atomico $\text{Bool}$:

$$\Gamma (x)=\text{Bool}$$

Grazie ai giudizi possiamo determinare se un termine è ben tipato o meno, ossia se le sue componenti rispettano i loro tipi.

Definizione: termine ben tipato

Un termine $T$ si dice ben tipato se e solo se esiste un contesto $\Gamma$ e un tipo $\tau$ tali che:

$$\Gamma ⊢T:\tau$$

1.1 - Regole di tipo

Avendo definito questi giudizi come proposizioni logiche, possiamo usare le regole di inferenza per dedurre nuovi giudizi a partire da quelli che sappiamo già per certo, in modo da poter stabilire se un termine è ben tipato o meno. Queste regole di inferenza le chiameremo regole di tipo.

Definizione: regola di tipo

Una regola di tipo è una regola di inferenza che stabilisce, in base alla forma sintattica di un termine $T$ e al tipo dei suoi costituenti, quale tipo può essere assegnato all’intero termine $T$.

Una regola di tipo è generalmente espressa come:

$$\frac{P_1{P}_2\dots P_n}{C}$$

dove:

• $P_1,P_2,\dots ,P_n$ sono le premesse, espresse sotto forma di giudizi, che indicano i tipi dei costituenti del termine $T$ e
• $C$ è la conclusione, espressa anch’essa sotto forma di giudizio, che stabilisce il tipo del termine $T$.
  

Definizione: regola di tipo assiomatica

Una regola di tipo si dice assiomatica se non ha premesse ma solo la conclusione:

$$\frac{}{C}$$

Ogni regola di tipo, a partire da un gruppo di giudizi (ossia le premesse) è in grado di generare un nuovo giudizio (la conclusione). Tuttavia, a loro volta le premesse possono essere conclusioni di altre regole di tipo precedenti, come nel caso

$$\frac{\frac{A_1{A}_2}{P_1}\frac{}{P_2}\dots \frac{B_1{B}_2\dots B_n}{P_n}}{C}$$

dove le premesse $P_1$ e $P_n$ sono a loro volta conclusioni di regole di tipo che hanno come premesse, rispettivamente, i giudizi $A_1,A_2$ e $B_1,B_2,\dots ,B_n$, mentre la premessa $P_2$ è conclusione di una regola di tipo assiomatica, non avendo premesse.

Possiamo quindi costruire dei grafici a forma di albero che ci permettono di risalire da un determinato giudizio alle regole di tipo assiomatiche che ci permettono di dedurlo: l’albero di derivazione.

Definizione: albero di derivazione

Nel ${\lambda }^{\to }$-calcolo, un albero di derivazione è una struttura ad albero che mostra passo per passo come un certo giudizio $G$ è ottenuto applicando le regole di tipo a partire da quelle assiomatiche. In particolare:

• la radice dell’albero è rappresentata dal giudizio $G$,
• ogni nodo interno è rappresentato da un giudizio ottenuto applicando una specifica regola di tipo, in modo che i figli del nodo siano esattamente i giudizi presenti nelle premesse della regola di tipo applicata e
• le foglie sono rappresentate da regole di tipo assiomatiche.
  

2 - STLC con booleani (STLCB)

Ora , seguendo quanto ho studiato nel corso di Linguaggi e Paradigmi di Programmazione che ho seguito all’Università, proviamo a espandere ulteriormente il ${\lambda }^{\to }$-calcolo accettando come unico tipo atomico quello booleano.

Definizione: ${\lambda }^{\to }$-calcolo con booleani

Il ${\lambda }^{\to }$-calcolo con booleani (spesso indicato anche come ${\lambda }_{\text{Bool}}^{\to }$-calcolo o con l’acronimo STLCB, dall’inglese Simply Typed Lambda Calculus with Booleans), è un’espansione del ${\lambda }^{\to }$-calcolo che ammette tra i tipi atomici unicamente il tipo booleano.

Ridefiniamo quindi il concetto di tipo.

Definizione: tipo nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo

Nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo, un tipo $\tau$ è un’etichetta assegnata a un termine che corrisponde a una stringa ben formata a partire dalla seguente grammatica espressa in BNF:

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

dove:

• $\text{Bool}$ è il tipo booleano, ossia il tipo che possono assumere le costanti booleane.
• $\tau \to \tau$ è il tipo funzione, ossia un tipo che indica che un’astrazione prende come argomento un termine di tipo $\tau$ e restituisce un termine di tipo $\tau$.
  

Nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo, avendo sovrascritto la definizione di tipo, dobbiamo ridefinire anche il termine, in cui però specifichiamo che gli unici valori che possono assumere le costanti sono solo quelli booleani ($\text{True}$ e $\text{False}$) e aggiungiamo una nuova forma sintattica: quella della struttura di controllo.

Definizione: termine nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo

Nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo, un termine $T$ (anche detto ${\lambda }_{\text{Bool}}^{\to }$-termine o ${\lambda }_{\text{Bool}}^{\to }$-espressione) è una stringa ben formata a partire dalla seguente grammatica espressa in BNF:

$$T::=x\mid c\mid (\lambda x.T)\mid (TT)\mid (\text{if}cTT)$$

dove:

1. $x$ è una variabile,
2. $c$ è una costante che può assumere come valori soltanto $\text{True}$ e $\text{False}$ ($c\in \{\text{True},\text{False}\}$),
3. $(\lambda x.T)$ è un’astrazione con argomento $x$ e corpo $T$,
4. $(TT)$ è un’applicazione in cui la funzione $T$ viene applicata all’argomento $T$,
5. $(\text{if}cTT)$ è una struttura di controllo in cui, se la condizione $c$ risulta vera ($c=\text{True}$), allora è uguale a $T$, altrimenti è uguale a $T$:

$$\begin{array}{r}\text{if}\text{True}TT=T\\ \text{if}\text{False}TT=T\end{array}$$

Ognuna di queste 5 forme che può assumere un termine è detta forma sintattica.

2.1 - Regole di tipo nell’STLCB

Prima di tutto, dichiariamo 5 regole di tipo per le 5 forme sintattiche che può assumere un termine nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo.

Definizione: regola di tipo $\text{(var)}$

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.

La regola di tipo $\text{(var)}$ dice che, se in un contesto un termine della forma di una variabile $x\in {\Lambda }^{\to }$ ha tipo $\tau$, allora $x$ ha tipo $\tau$:

$$\frac{}{\Gamma ,x:\tau ⊢x:\tau }$$

Definizione: regola di tipo $\text{(bool)}$

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.

La regola di tipo $\text{(bool)}$ dice che, se in un contesto un termine della forma di una costante $c$ è di tipo booleano $\text{Bool}$, allora ha tipo booleano $\text{Bool}$:

$$\frac{}{\Gamma ⊢c:\text{Bool}}$$

Definizione: regola di tipo $\text{(astr)}$

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.

La regola di tipo $\text{(astr)}$ dice che, se in un contesto un termine della forma di un’astrazione $\lambda x.M$ avente l’argomento $x$ con tipo $\sigma$ abbiamo $M$ con tipo $\tau$, allora l’intera astrazione $\lambda x.M$ ha tipo funzione $\sigma \to \tau$:

$$\frac{\Gamma ,x:\sigma ⊢M:\tau }{\Gamma ⊢\lambda x.M:\sigma \to \tau }$$

Definizione: regola di tipo $\text{(app)}$

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.

La regola di tipo $\text{(app)}$ dice che, se in un contesto un termine della forma di un’applicazione $MN$ abbiamo la funzione $M$ con tipo funzione $\sigma \to \tau$ e l’argomento $N$ con tipo $\sigma$ , allora l’intera applicazione $MN$ ha tipo $\tau$:

$$\frac{\Gamma ⊢M:\sigma \to \tau \Gamma ⊢N:\sigma }{\Gamma ⊢MN:\tau }$$

Definizione: regola di tipo $\text{(if)}$

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.

La regola di tipo $\text{(if)}$ dice che, se in un contesto un termine della forma di una struttura di controllo $\text{if}cMN$ ha $c$ di tipo booleano $\text{Bool}$ ed $M$ ed $N$ entrambi di tipo $\tau$, allora l’intera struttura di controllo $\text{if}cMN$ ha tipo $\tau$:

$$\frac{\Gamma ⊢c:\text{Bool}\Gamma ⊢M:\tau \Gamma ⊢N:\tau }{\Gamma ⊢\text{if}cMN:\tau }$$

Nonostante non abbiamo ancora tutti gli strumenti corretti per farlo, proviamo a vedere come andrebbero usate queste regole di tipo per verificare se un termine è ben tipato provando a costruire un albero di derivazione (spoiler: più avanti introdurremo un algoritmo per farlo correttamente, l’algoritmo di inferenza).

Esempio di uso delle regole di tipo in un albero di derivazione

Prendiamo come esempio il seguente termine:

$$(\lambda x.x)\text{True}$$

Assumiamo che sia ben tipato: che tipo avrà?

Possiamo barare un po’ e notare che è un’applicazione del combinatore identità alla costante booleana $\text{True}$, quindi il risultato sarà proprio la costante booleana $\text{True}$ e avrà lo stesso tipo di $\text{True}$, ossia il tipo booleano $\text{Bool}$.

Avremo quindi il seguente giudizio:

$$⊢(\lambda x.x)\text{True}:\text{Bool}$$

Per procedere da questo giudizio, basta guardare la forma sintattica del termine: essendo un’applicazione, useremo la regola di tipo $\text{(app)}$ che dice che, affinché l’applicazione $(\lambda x.x)\text{True}$ sia ben tipata, la funzione $(\lambda x.x)$ deve essere di un tipo funzione $\alpha \to ?$ dove $\alpha$ deve coincidere con il tipo dell’argomento $\text{True}$ (che ha tipo booleano $\text{Bool}$), mentre usiamo momentaneamente $?$ come segnaposto per decidere più tardi cosa metterci lì. Avremo quindi:

$$\frac{⊢\lambda x.x:\text{Bool}\to ?⊢\text{True}:\text{Bool}}{⊢(\lambda x.x)\text{True}:\text{Bool}}\text{(app)}$$

Il ramo della costante $c$ possiamo subito chiuderlo usando la regola di tipo $\text{(bool)}$ che è assiomatica, quindi siamo arrivati al capolinea da questo lato:

$$\frac{⊢\lambda x.x:\text{Bool}\to ?\frac{}{⊢\text{True}:\text{Bool}}\text{(bool)}}{⊢(\lambda x.x)\text{True}:\text{Bool}}\text{(app)}$$

Dall’altro lato, quel $?$ come segnaposto possiamo sostituirlo barando un altro po’ e vedendo che, dato che l’astrazione $\lambda x.x$ è il combinatore identità, se gli passiamo un argomento di tipo booleano $\text{Bool}$ ci restituirà un risultato sempre di tipo booleano $\text{Bool}$:

$$\frac{⊢\lambda x.x:\text{Bool}\to \text{Bool}\frac{}{⊢\text{True}:\text{Bool}}\text{(bool)}}{⊢(\lambda x.x)\text{True}:\text{Bool}}\text{(app)}$$

Per la [regola di tipo $\text{(astr)}$], il corpo $x$ è ben tipato in un contesto in cui l’argomento $x$ ha tipo $\text{Bool}$ e ottiene tipo $\text{Bool}$:

$$\frac{\frac{x:\text{Bool}⊢x:\text{Bool}}{⊢\lambda x.x:\text{Bool}\to \text{Bool}}\text{(astr)}\frac{}{⊢\text{True}:\text{Bool}}\text{(bool)}}{⊢(\lambda x.x)\text{True}:\text{Bool}}\text{(app)}$$

Infine, il giudizio $x:\text{Bool}⊢x:\text{Bool}$ è frutto dell’uso della regola di tipo $\text{(var)}$:

$$\frac{\frac{\frac{}{x:\text{Bool}⊢x:\text{Bool}}\text{(var)}}{⊢\lambda x.x:\text{Bool}\to \text{Bool}}\text{(astr)}\frac{}{⊢\text{True}:\text{Bool}}\text{(bool)}}{⊢(\lambda x.x)\text{True}:\text{Bool}}\text{(app)}$$

Dato che anche qui siamo arrivati a usare una regola di tipo assiomatica, abbiamo concluso qua e abbiamo dimostrato che il termine $(\lambda x.x)c$ è ben tipato e ha tipo booleano $\text{Bool}$, costruendo così correttamente un albero di derivazione.

2.2 - Proprietà dei termini ben tipati

Se un termine $M$ è ben tipato e si riduce a un altro termine $N$, allora $M$ ed $N$ avranno lo stesso tipo. Ciò significa quindi che la riduzione singola preserva il tipo.

Lemma di subject reduction

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.
Dati due termini $M,N\in {\Lambda }_{\text{Bool}}^{\to }$, se in un contesto $\Gamma$ $M$ ha tipo $\tau$ e si riduce a $N$, allora anche $N$ avrà tipo $\tau$ nel contesto $\Gamma$:

$$\forall M,N\in {\Lambda }_{\text{Bool}}^{\to }((\Gamma ⊢M:\tau \wedge M\to N)⟹(\Gamma ⊢N:\tau ))$$

Definizione: valore

Nel ${\lambda }_{\text{Bool}}^{\to }$-calcolo, un valore è un termine $T$ che è della forma semantica di una costante booleana o di un’astrazione.

Esempi di valori

Ecco una lista di termini e per ognuno dei quali vediamo se sono valori o meno:

• $(\lambda x.x)\text{True}$: non è un valore perché è un’applicazione con funzione $\lambda x.x$ e argomento $\text{True}$. Tuttavia, con un passaggio di $\beta$-riduzione, otteniamo $\text{True}$ che è una costante booleana e diventa un valore.
• $\text{True}(\lambda x.x)$: non è un valore perché è un’applicazione con funzione $\text{True}$ e argomento $\lambda x.x$. È in forma normale, quindi non è riducibile e non potrà mai diventare un valore.
• $\lambda x.x(\lambda y.y)$: è un valore perché è un’astrazione con argomento $x$ e corpo $x(\lambda y.y)$.

Possiamo dimostrare che, per ogni termine $M$ riducibile in zero o più passi in un altro termine $N$ in forma normale, quest’ultimo è un valore.

Teorema del progresso

Sia ${\Lambda }_{\text{Bool}}^{\to }$ l’insieme di termini del ${\lambda }_{\text{Bool}}^{\to }$-calcolo.
Dati due termini $M,N\in {\Lambda }_{\text{Bool}}^{\to }$ con $M$ combinatore e $N$ in forma normale, se $M$ ha tipo $\tau$ ed è riducibile in zero o più passi in $N$, allora $N$ è un valore:

$$\forall M,N\in {\Lambda }_{\text{Bool}}^{\to }\left(\right((⊢M:\tau )\wedge (M\Rightarrow N\nrightarrow ))⟹(N\text{ eˋ un valore}))$$

---

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:
      • Lambda calcolo con tipi.
    • Prof. Luca Padovani, videoregistrazioni del corso:
      • Lambda calcolo con tipi.
  • Corso di Linguaggi e Paradigmi di Programmazione, A.A. 2025-26 (pagina Moodle):
    • Prof. Viviana Bono, lezioni del corso.
• 📹 Eyesomorphic, Programming with Math | The Lambda Calculus su YouTube.
• 🌐 Lambda-calcolo su Wikipedia in lingua italiana, archiviato sulla Wayback Machine in data 25 novembre 2025.
• 🌐 Simply typed lambda calculus su Wikipedia in lingua inglese, archiviato sulla Wayback Machine in data 25 novembre 2025.