🎭 Skolem, Herbrand e Montanari in Dieci Atti

Brainfood Kolemödelöv Spice

Un piatto storico-algoritmico tra Skolem e Montanari unificato a vapore

La vita è strana, come disse Shakespeare, "All the world's a stage, and all the men and women merely players", e a volte il nostro ruolo è quello di trovarci davanti a un problema che sembra così banale da risultare quasi offensivo nella sua semplicità. Due espressioni logiche che contengono termini e quantificatori e una montagna di altri dettagli sintattici e semantici che insieme ci chiedono se possiamo rendere queste due espressioni identiche sostituendo le variabili con termini concreti, e nel caso, quali sono le sostituzioni specifiche che devi applicare per ottenere questo risultato di unificazione che, una volta raggiunto, ti permette di procedere con il resto della tua computazione logica, il tuo programma Prolog, il tuo type checker, o qualunque cosa tu stia cercando di fare con queste due formule che ti osservano con aria di sfida dalla pagina? Bene, questo è il problema dell'unificazione, ed il tipo di cosa che gli informatici degli anni '70 hanno deciso di affrontare non perché fosse particolarmente affascinante come argomento di conversazione ai cocktail party, ma perché era fondamentale per fare funzionare effettivamente la logica computazionale in modo che non richiedesse migliaia di anni per risolvere persino i problemi più banali.

In questo nostro universo a questo punto entra Ugo Montanari, un ricercatore italiano che ha avuto la genialità per descrivere un algoritmo che potremmo chiamare, senza esagerare, una delle colonne portanti della programmazione logica moderna, un algoritmo che prende due termini e determina se esiste una sostituzione (una unificazione) che li rende identici, e se tale sostituzione esiste, l'algoritmo la trova in modo relativamente poco costoso dal punto di vista computazionale. Ma eccoci qui, con questo algoritmo di Montanari tra le mani, e ci chiediamo (perché è naturale chiedersi queste cose), come è possibile che questa procedura meccanica, passo dopo passo, riesca a fare quello che fa? Come è possibile che, data la complessità ricorsiva della struttura dei termini logici, riesca comunque a dare con una risposta corretta e soprattutto computabile in tempo polinomiale? La risposta, mio caro lettore, che forse stai iniziando a sentire le prime avvisaglie di un'emicrania intellettuale, risiede in un uomo chiamato Thoralf Skolem, un logico norvegese che ha vissuto all'inizio del ventesimo secolo e che ha avuto un'idea così potente nella sua semplicità e così radicale nelle sue conseguenze, che ancora oggi, la sua idea continua a permeare ogni angolo dalla logica computazionale alla verifica formale di programmi, e di praticamente qualsiasi cosa che coinvolga il tentativo di farsi capire da una macchina utilizzando il linguaggio della logica matematica. Quindi, anzichè iniziare dal principio (cosa che faresti in un libro di testo noioso), cominciamo dal presente, dall'algoritmo di Montanari che stai già usando senza nemmeno rendertene conto, ogni volta che un type checker inferisce il tipo di una funzione che hai scritto senza annotare esplicitamente, ogni volta che una machine learning library tenta di unificare i tensori che hai passato con quelli che la funzione si aspetta, e da lì faremo un salto temporale indietro per scoprire esattamente quale genere di magia Skolem ha realizzato che rende tutto questo possibile.

Interludio segreto

Prima di addentrarci nell'algoritmo di Montanari, una curiosità storica che suona quasi paradossale ma che è vera e documentata, Georg Cantor dimostrò che esistono insiemi non numerabili, ma quando la logica del primo ordine venne studiata più a fondo, emerse un risultato che oggi chiamiamo Paradosso di Skolem. In pratica il teorema di Löwenheim–Skolem implica che, se una teoria del primo ordine è soddisfacibile, allora ha anche un modello numerabile, quindi una teoria che dimostra l’esistenza di insiemi più grandi dei naturali può comunque avere un modello che, dall’esterno, è numerabile. Questo cortocircuito è una rivelazione sulla relatività della nozione di cardinalità all’interno dei modelli. E per chiarire la struttura delle formule coinvolte in questi ragionamenti, Skolem introdusse la trasformazione che oggi porta il suo nome. Lo fece non per costruire algoritmi, i computer e i dimostratori automatici sarebbero arrivati decenni dopo, ma per rendere più trasparente la forma delle formule e per analizzare meglio i modelli che il teorema metteva in luce.

Non è una cosa nuova che un'idea nata per risolvere un problema di fondamenti della matematica finisca per essere usata altrove come qui è servita per meccanizzare l'idea di ragionamento, qualcuno la chiama serendipità, altri fortuna. Quindi se Cantor ha stabilito che esistono infiniti di diversa grandezza, fu Skolem, studiando le conseguenze modellistiche di quel quadro, a fornire lo strumento che, molti anni dopo, si sarebbe rivelato indispensabile per la logica computazionale.

Atto Primo: L'Algoritmo di Montanari

L'algoritmo di Montanari è fondamentalmente una procedura che risolve un insieme di equazioni fra termini, dove ogni termine è costruito ricorsivamente e l'obiettivo è determinare se esiste un'assegnazione di valori alle variabili (una sostituzione) che rende tutte le equazioni simultaneamente vere. Questo che significa che se hai un'equazione come f(X, g(Y)) = f(a, g(b)), tu stai cercando una sostituzione che, quando applicata a entrambi i lati dell'equazione, li rende identici carattere per carattere. Montanari ha descritto questo algoritmo come una sequenza di trasformazioni su un insieme di equazioni non risolte, dove ogni trasformazione elimina progressivamente la complessità delle equazioni stesse, fino a quando non rimangono che due casi possibili, l'insieme di equazioni è stato trasformato in una forma risolta (che rappresenta una sostituzione valida), oppure ad un certo punto durante il processo di trasformazione si incontra una contraddizione. Ecco come funziona, grosso modo, in pseudocodice che non è veramente pseudocodice ma che si fa capire più o meno:

UNIFY(equazioni, sostituzione_attuale):
  se equazioni è vuoto:
    ritorna sostituzione_attuale

  seleziona un'equazione E dalle equazioni
  rimuovi E da equazioni

  applica decomposizione a E:
    se E è della forma costante = costante e sono uguali:
      continua con il resto

    se E è della forma f(t1, ..., tn) = f(s1, ..., sn):
      sostituisci E con le equazioni t1=s1, ..., tn=sn
      ricorsione su equazioni aggiornate

    se E è della forma X = t dove X è una variabile e t è un termine:
      applica il "occur check" (controlla che X non compaia in t):
        se X non compare in t:
          aggiungi X->t alla sostituzione
          applica questa sostituzione a tutte le altre equazioni
          ricorsione su equazioni aggiornate
        se X compare in t:
          fallisci (unificazione impossibile)

    se E è una contraddizione (costanti diverse, simboli diversi, etc):
      fallisci

Questo algoritmo funziona riducendo la complessità del problema e infatti quando elimini un'equazione, il numero di variabili libere e non risolte diminuisce (o rimane stabile), e il numero di funzioni e costanti "dirette" in quelle equazioni tende a diminuire verso il punto in cui non rimane niente di interessante da fare se non dichiarare vittoria.

Ma qui è le cose diventano strane, perché prima che Montanari descrivesse questo algoritmo doveva esserci un'idea di base che rendesse anche soltanto possibile pensare in questi termini, doveva esserci il concetto che, in qualche modo, fosse lecito e corretto (non solo computazionalmente ma logicamente) ridurre il numero di quantificatori esistenziali nel nostro problema di unificazione, doveva esserci il riconoscimento che le variabili universali "da fuori" (come X e Y nell'equazione f(X, g(Y)) = f(a, g(b))) potessero essere eliminate e sostituite da termini costruiti a partire dalle costanti e funzioni che sono già presenti nel problema, senza perdere la capacità di trovare tutte le possibili soluzioni.

E quell'idea sarebbe? Quella è stata l'idea di Skolem.

Intermmezzo Narrativo

Prima di tuffarci nei profondità algebriche e semantiche di ciò che Skolem ha realizzato, permettetemi di offrire una metafora, una che, spero, non sia troppo fantasiosa per far infuriare i veri logici della sala, ma nemmeno eccessivamente semplice da risultare insulsa per coloro che stanno cercando di capire davvero cosa stia accadendo in questa storia.

Immaginiamo uno chef, ma uno che ha studiato matematica da giovane prima di dedicarsi alla cucina, uno di quelli che ha una strana ossessione per la struttura e per il principio sottostante le cose, che presenta un piatto a un critico gastronomico estremamente esigente.

Il critico guarda il piatto e chiede: "E questo cos'è?"

Lo chef risponde: "È Skolemödelöv al sugo di Unificazione con riduzione di Complessità mediante Eliminazione Sistematica di Variabili Universali Attraverso Istanziazione con Funzioni Sintatticamente Costruite Dall'Ambiente Circostante."

Il critico fa una smorfia stranito dal nome lunghissimo e incomprensibile.

Lo chef continua: "Vede, il piatto è costruito usando solo gli ingredienti che che avevo già pronti sul banco in cucina, tutto a Km 0, ho preso quello che c'era, l'ho reinterpretato, questa è la magia del piatto, non aggiungere ingredienti nuovi, ma nel capire che gli ingredienti che hai già a disposizione possono essere usati in modi così intelligenti da creare qualcosa che sembra completamente nuovo.

Il critico, ancora confuso, ordina un'altra birra.

Lo chef, indeterrito, continua: "Quello che ho fatto è preso un problema che sembrava richiedere di considerare tutti i possibili infiniti mondi in cui le variabili universali potessero essere istanziate, e l'ho ridotto a considerare soltanto un singolo mondo costruito usando appena gli ingredienti che avevo già, un mondo di Herbrand, lo chiamiamo, in onore di Jacques Herbrand, che è quello che ha scoperto questo trucco decenni dopo Skolem ma non sapeva che Skolem l'aveva già fatto, e in questo mondo minuscolo, ma sufficientemente ricco, è garantito che se una soluzione esista in qualunque altro mondo possibile, allora una soluzione esiste anche qui."

Il critico incomincia a capire (o almeno, finge di capire abbastanza bene da non fare altre domande imbarazzanti).

Lo chef sorride e sparisce in cucina.

Atto Secondo: La Logica si Trasforma

Ma ora dobbiamo capire il contesto logico/filosofico in cui si trovava, e il modo in cui la comunità matematica dell'epoca stava cercando di capire il significato di quella strana creatura che era la logica dei predicati, quella che oggi chiamiamo logica del primo ordine e che è, praticamente, il linguaggio in cui si esprimono i computer quando cercano di ragionare su concetti astratti.

Nei primi anni del ventesimo secolo, la logica matematica era ancora una cosa piuttosto nuova e piuttosto controversa, Frege aveva creato il suo sistema di notazione che nessuno riusciva a leggere, Russell e Whitehead stavano cercando di fondare la matematica su principi logici e stavano scoprendo paradossi terribili (come il famoso paradosso di Russell, che distrugge il concetto ingenuo di "insieme di tutti gli insiemi"), e in generale c'era una sensazione di essere su un terreno non ancora completamente mappato, dove ogni passo poteva portare a una rivelazione profonda o a un baratro logico. Skolem, che era una figura tranquilla e poco incline alla pubblicità (al contrario di certi suoi colleghi più rumorosi), stava riflettendo su una questione che potremmo esprimere così:

supponiamo di avere una affermazione logica che contiene sia variabili universali (il quantificatore per-ogni, ∀) che variabili esistenziali (il quantificatore esiste, ∃), come ad esempio "per ogni X, esiste un Y tale che P(X, Y)" (∀X ∃Y P(X, Y)), quando io cerco di dimostrare questa affermazione o di determinare se è vera in un particolare modello matematico, cosa stai effettivamente facendo?

Stai dicendo, pre ogni possibile valore che X potrebbe assumere, io devo trovare almeno un valore per Y che rende vera P(X, Y), ma qui c'è una cosa importantissima, il valore di Y che funziona per un particolare X potrebbe essere completamente diverso dal valore di Y che funziona per un altro X, Y è dipendente da X, Y è una funzione di X. Skolem ha realizzato che potevamo riformulare questa affermazione (sotto determinate condizioni) e al posto di dire "per ogni X, esiste un Y tale che P(X, Y)", si poteva dire "esiste una funzione f tale che per ogni X, P(X, f(X))", dove f è una funzione di Skolem (che in onore di Skolem è chiamata così) che cattura precisamente questa dipendenza. Quello che Skolem aveva realizzato era che era possibile eliminare i quantificatori esistenziali dalla sua formula (o almeno, poteva eliminarli dai quantificatori più interni, quelli che dipendono dai quantificatori universali) sostituendoli con funzioni che non erano date in precedenza nel problema, ma che potevi assumere di esistere senza cambiare il significato logico di quello che stavi cercando di provare. Questo significava che era posibile trasformare un problema logico complesso con molti quantificatori intrecciati in un problema più semplice con solo quantificatori universali (o addirittura nessun quantificatore se avevi già eliminato tutti gli esistenziali), e poi, avendo solo quantificatori universali, si potevano ignorare del tutto e semplicemente considerare tutti i possibili istanziamenti delle tue variabili usando le costanti e funzioni che apparivano già nel problema. Questa è l'essenza di quello che è diventato noto come il Principio di Skolem o Skolemizzazione.

Atto Terzo: Entra in scena Herbrand

E in che modo si realizz nella pratica il collegamento tra Skolem e Montanari, come cioè lo strumento concettuale che Skolem ha creato nel 1920 si traduca nell'algoritmo meccanico e pratico che Montanari ha descritto negli anni '70 per risolvere effettivamente i problemi di unificazione che si incontrano quando si scrive un type checker per un linguaggio di programmazione funzionale? Per capirlo dobbiamo introdurre il concetto di forma normale di Skolem, il formato canonico in cui si esprime una formula logica dopo aver applicato sistematicamente la trasformazione di Skolem, quindi dopo aver eliminato i quantificatori esistenziali e rimpiazzati con funzioni di Skolem, e dopo aver riorganizzato il tutto in modo che rimangano solo quantificatori universali all'esterno (se rimangono quantificatori del tutto). Supponiamo di avere una cosa come ∀X ∃Y ∀Z ∃W P(X, Y, Z, W), che èpiuttosto complicata perché ha quantificatori che si alternano, il che rende il problema di determinare la sua soddisfacibilità (cioè, se esiste un'interpretazione del mondo che rende vera questa formula) estremamente difficile perché devi considerare la dipendenza di Y da X e la dipendenza di W sia da X che da Z. Bene, ora applichiamo la trasformazione di Skolem, il primo ∃Y dipende da ∀X, quindi lo rimpiazzi con una funzione f(X), ottenendo ∀X ∀Z ∃W P(X, f(X), Z, W), poi il ∃W dipende sia da ∀X che da ∀Z (perché questi sono i quantificatori universali che rimangono all'esterno), quindi lo rimpiazzi con una funzione g(X, Z), ottenendo infine ∀X ∀Z P(X, f(X), Z, g(X, Z)).

Ora una volta eliminati tutti i quantificatori esistenziali, la formula contiene solo variabili universali, il che significa che puoi ignorare i quantificatori universali e pensare solo al nucleo della formula (quella che viene chiamata la clausola di Skolem, nel nostro caso P(X, f(X), Z, g(X, Z))) come a una serie di vincoli che devono essere soddisfatti da qualunque istanziamento tu faccia delle variabili X e Z. E entra Montanari, infatti supponiamo di avere un'altra formula trasformata in forma normale di Skolem, diciamo ∀X' ∀Z' Q(X', f'(X'), Z', g'(X', Z')), e tu voglia determinare se queste due formule possono essere unificate, cioè se esiste un'assegnazione di valori alle variabili (e alle funzioni di Skolem, se necessario) che rende le due formule identiche o almeno coerenti fra loro, allora quello che stiamo effettivamente facendo è quello che Montanari ha descritto infatti stiamo prendendo le due formule, le stiamo trattando come termini (perché, nel linguaggio della logica, una formula è solo un termine costruito ricorsivamente usando simboli predicativi invece di simboli funzionali), e stiamo applicando la procedura di unificazione per determinare se esiste una sostituzione che le rende identiche. Ma c'è un pezzo mancante che completa il puzzle e che rende tutto questo computazionalmente pratico, il concetto di universo di Herbrand, che è una scoperta di Jacques Herbrand che ha costruito (involontariamente, potremmo dire, perché Herbrand non conosceva il lavoro di Skolem al momento) sopra le fondamenta che Skolem aveva gettato. L'universo di Herbrand di un insieme di formule è l'insieme di tutti i termini che puoi costruire usando le costanti e i simboli funzionali che appaiono già nelle formule stesse, senza introdurre niente di nuovo dal di fuori, è il mondo minimo in cui puoi interpretare le tue formule, il mondo in cui gli unici oggetti che esistono sono quelli che puoi nommare usando la sintassi del tuo problema. E se una formula logica è soddisfacibile (cioè, esiste almeno un mondo, una interpretazione, in cui è vera), allora è soddisfacibile anche nel suo universo di Herbrand, cioè, è soddisfacibile nel mondo minimo costruito usando solo gli ingredienti sintattici che aveva già a disposizione, non hai mai bisogno di comprare ingredienti nuovi dal mercato, quello che hai in cucina è sempre abbastanza...

Questo è ciò che collega Skolem e Herbrand a Montanari, quando Montanari descrive il suo algoritmo di unificazione, sta implicitamente dicendo che la ricerca di una unificazione tra due termini può essere confinata al universo di Herbrand dei termini stessi, che le unificazioni che trovi usando il suo algoritmo sono le unicamente rilevanti, perché se una unificazione fosse possibile "nel grande mondo là fuori", allora una unificazione sarebbe possibile anche nel piccolo mondo costruito sintatticamente dal tuo problema.

Atto Quarto: Il Teorema di Completezza

A questo punto, se sei ancora qui e stai cercando di seguire questo abisso di complessità letteraria e concettuale che ti ho teso davanti, probabilmente ti stai anche chiedendo come cavolo fai a sapere che tutto questo è corretto e che l'algoritmo di Montanari sia effettivamente in grado di trovare tutte le unificazioni che esistono. La risposta la troviamo codificata in una serie di teoremi che sono stati dimostrati nel corso degli ultimi cent'anni della logica matematica, che tutti insieme, formano una struttura teorica così robusta che potremmo quasi dire che abbiamo raggiunto un livello di certezza che raramente si incontra al di fuori della matematica pura, parlo del Teorema di Completezza di Gödel, della Correttezza e Completezza dell'Unificazione, e di una serie di altri risultati che insieme garantiscono che la strategia di Skolem, implementata tramite Montanari è fondamentalmente corretta dal punto di vista logico. Gödel, nel 1929, ha dimostrato che il sistema della logica del primo ordine è completo, nel senso che ogni formula che è logicamente valida (vera in tutti i modelli possibili) è provabile usando le regole di inferenza della logica stessa, oltre a essere il teorema più frainteso della storia implica che la logica del primo ordine non è troppo debole (lasciando sfuggire verità che non riesce a provare) e neanche troppo potente (provando cose che in realtà non sono vere).

Collegato a questo c'è il fatto che se tu applicassi la trasformazione di Skolem a una formula logica, la formula risultante sarebbe equisoddisfacibile con l'originale, il che significa che la formula originale è soddisfacibile se e solo se la formula trasformata è soddisfacibile, e ciò significa che trasformare il problema iniziale non lo cambia dal punto di vista della sua risolvibilià.

E poi, specificamente per l'unificazione, Martelli e Montanari hanno dimostrato (ed è qui che il nostro Montanari entra in scena come protagonista matematico e non solo come nome in un algoritmo) che l'algoritmo che porta il suo nome è corretto (ogni sostituzione che trova effettivamente unifica i termini) e completo (trova tutti i possibili unificatori, o più precisamente, trova l'unificatore più generale, dal quale tutti gli altri unificatori possono essere ottenuti per istanziazione), e che lo fa in tempo che è lineare rispetto alla dimensione dell'input se implementato correttamente (con qualche accorgimento sulla rappresentazione dei termini, come l'uso di directed acyclic graphs per evitare di copiare letteralmente interi sottoalberi di termini).

Atto Quinto: Dal Astratto al Concreto (Finalmente)

Con alle spalle questo castello teorico bellissimo e complicato proviamo a scendere un pochino dal cielo della metafisica logica e a mostrare come tutto questo appare effettivamente quando stiamo scrivendo codice e quando stiamo costruendo problemi che devono essere risolti da macchine che seguono algoritmi come quelli di Montanari.

Supponiamo che tu abbia un semplice programma Prolog (il linguaggio di programmazione logica più famoso, praticamente una incarnazione diretta di questi concetti):

padre(giovanni, marco).
padre(marco, luca).

nonno(X, Z) :- padre(X, Y), padre(Y, Z).

?- nonno(giovanni, luca).

Quando tu poni questa query (domanda) a Prolog, il sistema traduce la query e le clausole in una forma logica, e poi applica la risoluzione, che è un metodo di provabilità che utilizza l'unificazione come suo passo centrale e fondamentale. Per provare nonno(giovanni, luca), il sistema cerca una clausola che abbia nonno nella sua testa, trova la clausola nonno(X, Z) :- padre(X, Y), padre(Y, Z), e poi deve unificare la query nonno(giovanni, luca) con la testa della clausola nonno(X, Z).

Applica l'algoritmo di unificazione:

Adesso, il sistema applica questa sostituzione al corpo della clausola (il :- padre(X, Y), padre(Y, Z) diventa :- padre(giovanni, Y), padre(Y, luca)), ed ora deve provare due goal nuovi, padre(giovanni, Y) e padre(Y, luca). Per il primo goal, unifica padre(giovanni, Y) con padre(giovanni, marco) ottenendo {Y -> marco}, e applicando questa sostituzione al secondo goal, ottiene padre(marco, luca), che unifica direttamente quibdi la query è vera.

Skolem entra in scena quando il sistema Prolog si converte in forma normale clausale (clause normal form), che è una applicazione sistematica di trasformazione di Skolem, ogni quantificatore esistenziale che appare nel corpo di una clausola (cioè, ogni variabile che appare solo nel corpo e non nella testa) è implicitamente trasformato in una funzione di Skolem, il che permette al sistema di cercare unificazioni in modo completamente meccanico e senza dover esplicitamente ragionare su "quali valori potrebbe assumere questa variabile nel mondo pieno di possibilità".

Atto Sesto: Rose, Fiori e occur check

Sperando che il piatto non vi abbia sconvolto troppo le papille gustative e vogliate finire il piatto vi anticipo che siamo a metà dell'opera, se arriverete alla fine ci sarà una gradita sorpresa. Ora torniamo a noi, dobbiamo dire che (e questo non dovrebbe sorprenderti dopo tutto quello che abbiamo già attraversato insieme), non tutto quello che abbiamo visto sia rose e fiori. Infatti nel mondo della unificazione e della Skolemizzazione, ci sono dettagli complicati e casi limite che richiedono attenzione per evitare di cadere in trappole logiche che possono portare a comportamenti inaspettati. Uno di questi dettagli è il cosiddetto occur check (controllo di occorrenza), che è una parte della procedura di unificazione di Montanari, ma che è anche una parte notoriamente problematica dal punto di vista della efficienza computazionale, il controllo di occorrenza serve a garantire che quando unifichiamo una variabile X con un termine t, assicuri che X non appaia dentro t, altrimenti finisci con strutture dati infinitamente ricorsive che non puoi nemmeno rappresentare in memoria e che rendono il tuo unificatore un oggetto logico non ben definito. Supponiamo, ad esempio, di cercare di unificare X con f(X), senza il controllo di occorrenza, il sistema potrebbe assegnare X -> f(X), il che significherebbe che X è uguale a una funzione applicata a se stessa, X = f(f(f(...))) all'infinito, una struttura impossibile da rappresentare finita­mente, il controllo di occorrenza lo previene verificando che X non appaia nel lato destro dell'assegnazione prima di procedere. Tuttavia il controllo di occorrenza richiede di scandire l'intero termine per verificare se una variabile appaia da qualche parte, introducendo così un overhead al processo di unificazione, specialmente quando i termini sono grandi e complessi, per questo motivo, molti sistemi Prolog omettono il controllo di occorrenza per motivi di efficienza, accettando il rischio di generare strutture dati infinite scommettendo sul fatto che nella pratica questi casi non occorrono frequentemente (o che il programmatore è abbastanza intelligente da non generarli intenzionalmente).

Inoltre l'algoritmo di Montanari, almeno classicamente, trova un unificatore (l'unificatore più generale, il MGU "most general unifier"), ma quando stai risolvendo un problema logico, spesso ti servono tutti i possibili unificatori, tutti i diversi modi in cui la unificazione potrebbe avvenire, questo è particolarmente critico in Prolog, dove il backtracking (cioè, il meccanismo di tornare indietro e provare alternative diverse quando una scelta non funziona) è fondamentale per l'esplorazione dello spazio di ricerca. Questo dettagli è il problema della ricerca di unificatori multipli. E poi c'è il problema della unificazione con vincoli (constraint unification), che è una estensione dell'unificazione classica dove al posto di semplici equazioni fra termini abbiamo vincoli più complessi e la ricerca di assegnazioni che soddisfano simultaneamente tutti questi vincoli diventa un problema molto più difficile che richiede algoritmi specializzati come la programmazione con vincoli (constraint programming).

Ma forse il dettaglio che li batte tutti è il problema della unificazione di ordine superiore che fa capolino quando i termini non sono costruiti solo usando variabili e simboli funzionali di primo ordine, ma possono contenere anche variabili che rappresentano funzioni stesse. Questo è il territorio della logica di ordine superiore, dove la complessità computazionale sale drammaticamente (il problema dell'unificazione di ordine superiore è indecidibile in generale e quindi non esiste un algoritmo generale che può determinare se due termini di ordine superiore sono unificabili per tutti i possibili input, anche se per certi sottoinsiemi il problema diventa decidibile con opportuni vincoli).

Atto Settimo: Un atto pratico

Abbiamo esplorato le complicazioni teoriche, permettimi di tornare a Montanari e di descrivere come il suo algoritmo è effettivamente implementato in un sistema pratico, quali sono le ottimizzazioni che rendono possibile fare unificazione velocemente anche su termini enormi, e come le intuizioni di Skolem si manifestano nel codice che gira su macchine moderni che probabilmente non sanno nemmeno chi è Skolem ma che lo usano comunque ogni giorno.

Una implementazione consapevole dell'algoritmo di Montanari in uno pseudocodice leggermente più realistico (ma ancora fortemente semplificato per ragioni di leggibilità) potrebbe apparire così:

def unify(term1, term 2, substitution=None):
  """
  Implementazione dell'algoritmo di unificazione di Montanari.
  Ritorna una sostituzione (dizionario) che unifica i due termini,
  o None se l'unificazione è impossibile.
  """
  if substitution is None:
    substitution = {}

  # Applica la sostituzione attuale a entrambi i termini
  term1 = apply_substitution(term1, substitution)
  term2 = apply_substitution(term2, substitution)

  # Base case: i termini sono già identici
  if term1 == term2:
    return substitution

  # Se term1 è una variabile
  if isinstance(term1, Variable):
    if occurs_check(term1, term2):
      return None  # Fallimento: X non può unificarsi con f(X)
    substitution[term1] = term2
    return substitution

  # Se term2 è una variabile
  if isinstance(term2, Variable):
    if occurs_check(term2, term1):
      return None
    substitution[term2] = term1
    return substitution

  # Se entrambi sono termini composti
  if isinstance(term1, Compound) and isinstance(term2, Compound):
    # Devono avere lo stesso funtore e la stessa arità
    if term1.functor != term2.functor or len(term1.args) != len(term2.args):
      return None  # Fallimento: f(...) non unifica con g(...)

    # Unifica ricorsivamente gli argomenti
    for arg1, arg2 in zip(term1.args, term2.args):
      substitution = unify(arg1, arg2, substitution)
      if substitution is None:
        return None

    return substitution

  # Se uno è una costante e l'altro no, fallimento
  return None

Naturalmente una implementazione reale in un sistema Prolog professionale è molto più sofisticata, ad esempio, invece di rappresentare i termini come strutture dati ricorsive che richiedono allocazione dinamica di memoria per ogni sottotermine, molti sistemi utilizzano una rappresentazione con indici o una rappresentazione con DAG (directed acyclic graphs) dove i sottoalberi comuni sono condivisi, riducendo così la memoria necessaria e accelerando le operazioni di copia e di applicazione di sostituzioni. Un'altra ottimizzazione è il cosiddetto structure sharing dove due termini che condividono sottoalberi comuni (cosa che è frequente quando stai facendo unificazione ripetuta), invece di copiare e duplicare questi sottoalberi, il sistema mantiene semplicemente puntatori a una rappresentazione condivisa riducendo l'uso della memoria e accelerando anche il processo di unificazione perché non devi copiare sottoalberi che rimangono invariati. E poi c'è il fast occur check, che è una versione ottimizzata del controllo di occorrenza che utilizza tecniche di graph traversal intelligenti e caching per evitare di scandore ripetutamente gli stessi sottoalberi, in molti casi, il controllo di occorrenza può essere eliminato completamente o differito fino a un momento successivo quando il costo di verificarlo è ammortizzato su più operazioni. Ma quella che rende possibile usare l'unificazione in applicazioni pratiche ad alta prestazione, p l'indexing del primo argomento che è una tecnica dove il sistema Prolog, quando deve trovare clausole che potrebbero unificarsi con una query, non scandisce linearmente tutte le clausole, ma invece mantiene una tabella di hash (o una struttura simile) che organizza le clausole in base al funtore del primo argomento del predicato così se cerchi unificazioni con il predicato padre(giovanni, X), il sistema non deve nemmeno guardare alle clausole che iniziano con padre(marco, ...), perché il primo argomento è diverso e non potrebbe unificarsi, quindi salta direttamente alle clausole rilevanti passando da una ricerca di candidati da O(n) (dove n è il numero totale di clausole) a O(1) in media (dove il tempo dipende dalla distribuzione del hash), il che rende possibile avere basi di dati logiche con milioni di fatti e ancora ottenere prestazioni di query ragionevoli.

Atto Ottavo: Oltre la storia

E a questo punto ci tocca fare un salto verso qualcosa che probabilmente è più familiare ai programmatori moderni, un campo dove la Skolemizzazione e l'unificazione giocano un ruolo altrettanto centrale ma molto meno visibile, nascosto dietro il sipario dell'inference del tipo (type inference). Questo è un territorio affascinante e complesso della programmazione con sistemi di tipo sofisticati, come quelli che si possono trovare in Haskell, OCaml e nei moderni type checker di TypeScript e Scala.

Supponiamo, in Haskell, di scrivere qualcosa come questo:

map f [] = []
map f (x:xs) = f x : map f xs

Quando il compilatore Haskell vede questa funzione, non ha informazioni di tipo esplicite (tu non hai scritto il tipo di map, il tipo di f, il tipo di x, niente, il compilatore deve dedurlo da solo), ma il compilatore Haskell è intelligente e risce a dedurre automaticamente il tipo di questa funzione, determinando che map ha tipo (a -> b) -> [a] -> [b], così "una funzione che prende una funzione da a a b e una lista di a, e ritorna una lista di b". MA come fa il compilatore a dedurre tutto questo? Lo fa attraverso un processo che è fondamentalmente una unificazione di tipo, che è una applicazione diretta dell'algoritmo di Montanari applicato ai tipi invece che ai termini logici generici. Il compilatore, quando vede la prima clausola map f [] = [], deduce che il risultato quando la lista è vuota deve essere una lista (perché ritorna [], che è una lista vuota di qualche tipo), quindi il tipo di ritorno deve essere una lista di qualche tipo, diciamo [b] (dove b è una variabile di tipo sconosciuta).

All'arrivo della seconda clausola map f (x:xs) = f x : map f xs, il compilatore nota che il pattern matching richiede che il secondo argomento sia una lista non vuota (è della forma (x:xs), un costruttore di lista con testa e coda), il che significa che il secondo argomento ha tipo [a] per qualche tipo a, la testa x ha tipo a, e la coda xs ha tipo [a]. Poi arriva il risultato è f x : map f xs, e quindi il risultato è una lista costruita applicando f a x (quindi f x deve avere tipo b, il tipo degli elementi della lista risultato) e prepending questo a map f xs (il ricorsivo del risultato), di conseguenza map f xs deve avere tipo [b]. Ora il compilatore deve unificare queste informazioni e cosa fa? Il primo parametro f è una funzione che viene applicata a x (di tipo a), producendo qualcosa di tipo b, quindi f deve avere tipo a -> b, e il tipo complessivo di map deve quindi essere (a -> b) -> [a] -> [b].

Tutto questo processo è interamente baaato sull'algoritmo di unificazione, quello che Montanari ha descritto, con Skolem implicitamente dietro le quinte ogni volta che il compilatore decide di introdurre una variabile di tipo fresca per rappresentare un tipo sconosciuto che sarà determinato successivamente attraverso il processo di unificazione. E il compilatore non ha bisogno di esplorare "tutti i mondi possibili dei tipi", ma grazie al principio di Skolem e al fatto che si sta lavorando nell'universo di Herbrand dei tipi (l'insieme di tutti i tipi che possono essere costruiti usando i costruttori di tipo e le variabili di tipo che appaiono nel programma), il compilatore sa che se un'unificazione di tipo è possibile in generale, allora è possibile all'interno di questo universo limitato, il che rende il processo calcolabile in tempo ragionevole (almeno per linguaggi senza universi polimorfici di ordine infinito). Sistemi di type inference moderni come quello di Hindley-Milner (su cui si basa Haskell) e le sue estensioni (come il sistema di tipi di Scala con i suoi bounded quantifiers e i suoi variance annotations) sono tutti stati costruiti su questi principi.

Atto Nono: PRoblemi e Regessioni infinite

Uno degli aspetti problematici riguarda il problema della unificazione con disequazioni dove invece di avere solo equazioni che devono essere soddisfatte (X = Y), abbiamo anche disequazioni e questa combinazione crea problemi che non sono completamente risolti nemmeno oggi poiché mentre l'unificazione con sole equazioni è un problema risolvibile meccanicamente, l'aggiungere disequazioni trasforma il problema in qualcosa dove le soluzioni non possono più essere rappresentate come semplici sostituzioni, ma devono essere rappresentate come insiemi (potenzialmente infiniti) di sostituzioni che soddisfano taluni vincoli di disequazione. Un altro aspetto patologico è il problema della unificazione modulo teorie equazionali, in questo caso le nostre equazioni devono essere considerate modulo una teoria equazionale, ad esempio, se abbiamo che f(X, Y) = f(Y, X) (l'operazione f è commutativa), allora f(a, b) e f(b, a) dovrebbero essere considerate uguali (unificabili), anche se sintatticamente sono diverse, determinare se due termini sono unificabili modulo una teoria equazionale diventa un problema che è dipendente dalla specifica teoria in modo forte, e per molte teorie il problema è prorpio indecidibile. E poi c'è il territorio completamente folle e affascinante della unificazione in frammenti di ordine superiore, qui tu, si proprio tu, hai la logica di ordine superiore che è espressiva quanto il calcolo lambda, ma con certe restrizioni che rendono l'unificazione decidibile. Il sistema di tipi di Scala con i suoi type parameters varianti e controvarianti, per esempio, sta implicitamente facendo una forma di unificazione di ordine superiore quando risolve i vincoli di tipo, e il fatto che il type checker di Scala talvolta abbia performance terribili su certi input dipende dalla complessità intrinseca di questi problemi di unificazione di ordine superiore che sta tentando di risolvere.

E poi c'è il più frustrante di tutti la non terminazione della unificazione che appare quando l'algoritmo di unificazione, nel tentare di risolvere un certo insieme di equazioni, entra in un ciclo infinito e non ritorna mai con una risposta. Questo non succede nel classico algoritmo di Montanari per la unificazione di primo ordine (perché il processo di riduzione delle equazioni termina sempre in un numero finito di passi), ma succede nelle estensioni dell'algoritmo che abbiamo appena visto. Un esempio classico di non-terminazione è il cosiddetto infinite regress in constraint solving, dove tu hai un insieme di vincoli che, ogni volta che tenti di risolverli, generano nuovi vincoli che, quando tenti di risolverli a loro volta, generano altri nuovi vincoli, e così via all'infinito. E il povero type checker di Haskell può a volte soffrire di questo problema se scrivi programmi sufficientemente complicati con istanze di typeclass che si rinforzano ricorsivamente (le cosiddette "overlapping instances").

Atto Decimo: Il tendone sta chiudendo

Credo che il significato più profondo di tutto questo viaggio sia che Skolem ha mostrato che è possibile confinare la tua ricerca a un universo minuscolo, costruito interamente dalla sintassi del problema stesso, e essere ancora sicuro che se una soluzione esiste nell'universo grande infinito là fuori, allora una soluzione esiste anche in questo piccolo universo finito che abbiamo creato da zero partendo dai nostri ingredienti. Una lezione profonda sull'economia del pensiero e sulla parsimonia della ricerca, sulla possibilità che gli umani (e, per estensione, le macchine) abbiano di risolvere problemi complessi non attraverso l'esplorazione esaustiva di tutte le possibilità (cosa che sarebbe computazionalmente impossibile per qualunque problema interessante), ma attraverso la scoperta di principi strutturali che permettono di confinare la ricerca a uno spazio più piccolo dove comunque tutte le soluzioni rilevanti possono essere trovate. Montanari, poi, ha preso questa interpretazione filosofica di Skolem e l'ha trasformata in un algoritmo pratico, che era il passo necessario per rendere la logica computazionale una realtà invece di una astrazione filosofica.

E infine, le generazioni successive di ricercatori che hanno esteso l'unificazione in mille direzioni diverse, che hanno preso queste fondamenta e le hanno trasformate in strumenti che usiamo tutti i giorni senza renderci conto che stiamo siamo sulle spalle di giganti che hanno riflettuto su questi problemi decenni prima che i computer moderni anche esistessero. Questo è un pezzatto dell'univero nascosto che c'è dietro l'uso quotidiano del computer e tu che stai leggendo, implicitamente, stai usando, beneficiando di intuizioni che risalgono a centocinquanta anni di riflessione sulla natura della logica e della computazione.

Conclusione Aperta

E adesso? Ci sarebbe moltissimo da dire, ma tanto, ma è ora che il nostro cuoco vada in pausa pranzo dopo aver spiegato al critico gastronomico (che ha perso conoscenza circa tre atti fa, ma che supponiamo continui a leggere nel suo stato di incoscienza) come l'arte di cucinare e l'arte della logica computazionale siano in realtà molto simili e in entrambi i casi, quello che si fa quando si prepara questo piatto è prendere ingredienti semplici, applicare principi sofisticati, e produrre qualcosa che è maggiore della somma delle sue parti, un piatto bello e costruito con la massima economia di mezzi, utilizzando quello che serve e nulla di più.

Skolem era il cuoco che ha capito che non hai bisogno di importare ingredienti esotici da lontano, quello che abbiamo sul tavolo in cucina è abbastanza, se lo sai usare correttamente mentre la ricetta per il nostro piatto l'ha scritta Montanari, passo dopo passo, in modo che chiunque (o qualunque macchina) potesse seguirla e ottenere sempre il medesimo risultato meraviglioso. E tu, lettore che sei arrivato fino a qui, sei il critico che spero abbia apprezzato il piatto e che ha compreso che il nome strano e lunghissimo che aveva era una parte essenziale della sua presentazione e speriamo che tu possa andare via con la consapevolezza che a volte le cose più importanti sono anche le cose più nascoste, quelle che lavorano dietro le quinte senza ricevere alcun riconoscimento e che nonostante tutto questo rendono possibile tutto il resto. Adesso, vi accompagno alla porta, il pasto lo offro io come vi avevo anticipato parlando di gradita sorpresa, non per niente il testo è in Creative Common. E' stato un pasto complicato ma Skolem e Montanari hanno molti altri piatti da servire quindi continua a cercare nuove ricette, ti assicuro che scoprirai un universo meraviglioso dove il pensier si perde. E icorda che molto di quello che fai quotidinamente con il tuo computer o smartphone è possibile grazie a un uomo tranquillo di nome Thoralf Skolem che, quasi centocinquanta anni fa ha avuto un'idea che ha permesso al suo nome di continuare a vivere negli algoritmi che girano su miliardi di macchine in tutto il mondo, anche se la maggior parte delle persone non ha la più pallida idea di chi sia stato. E con lui ci sono Montanari, Herbrand, Martelli e tanti altri.

E con questo, il sipario cala.

**Fine del Documento.. Almeno della parte che riesce a stare entro limiti ragionevoli per un readme GitHub iniziato ieri notte e finito di scrivere in pausa pranzo. Tra l'altro manca un po' di bibliografia lo so, ma non mi andava di farmela generare dalla AI quindi la scrivo quando ho tempo.

📜 Licenza (IT + EN)

🇮🇹 Italiano

Questo documento è rilasciato sotto licenza Creative Commons CC BY‑NC‑ND 4.0.
È consentita la condivisione del testo, a condizione che:

Eccezione per la traduzione: In deroga alla clausola ND (NoDerivatives), è espressamente consentita la traduzione integrale del documento, purché:

Qualsiasi altra forma di modifica o opera derivata non è permessa.

🇬🇧 English

This document is licensed under the Creative Commons CC BY‑NC‑ND 4.0 license.
You may share the text provided that:

Translation Exception: As an explicit exception to the ND (NoDerivatives) clause, full and faithful translations of this document are permitted, provided that:

Any other form of modification or derivative work is not allowed.