MaudeTypedLog: A Typed Interpreter for Prolog in Maude

Immagina di stare costruendo una casa di carte. Nel mondo dell'informatica, esiste un linguaggio molto popolare chiamato Prolog che agisce come un maestro costruttore, ma ha un libro delle regole molto rilassato: non gli importa se provi a bilanciare un mattone pesante sopra una delicata tenda di carta. Si limita a cercare di farli incastrare. Se il mattone è troppo pesante, l'intera struttura potrebbe crollare in seguito, oppure il costruttore potrebbe semplicemente dire: "Beh, questo non ha funzionato", senza però spiegarti il perché del fallimento. Questo accade perché Prolog è tradizionalmente "non tipizzato", il che significa che non controlla se i pezzi che stai cercando di connettere abbiano la forma o il materiale corretti prima di iniziare a costruire.

Tuttavia, a volte il costruttore sa che qualcosa non va. Se provi a mescolare una lista di numeri con un singolo numero in un modo specifico, potrebbe alzare le mani e dire: "Errore!". Ma questo accade solo dopo che la costruzione è già iniziata a traballare. Per anni, gli scienziati dell'informatica hanno cercato di dare a Prolog un libro delle regole migliore — un "sistema di tipi" — che controlli i materiali prima che la costruzione abbia inizio. Il problema è che la maggior parte di questi tentativi è o troppo complicata per essere usata dalle persone, o è così vaga da perdere gli errori più ovvi. È come avere un ispettore della sicurezza che controlla il tetto solo se glielo si chiede espressamente, o uno che dice "forse i mattoni vanno bene" quando sono chiaramente fatti di gelatina.

È qui che entra in gioco un nuovo strumento, creato dai ricercatori Enrique Gallifa-Tronch, João Barbosa e Santiago Escobar. Hanno deciso di smetere di provare a riparare direttamente Prolog e hanno invece costruito un interprete completamente nuovo e super rigoroso chiamato MaudeTypedLog. Immagina di prendere i progetti di Prolog e di farli passare attraverso un motore di simulazione magico ad alta velocità chiamato Maude. Questo motore non si limita a cercare di incastrare i pezzi; controlla se i pezzi sono addirittura autorizzati a toccarsi in primo luogo. Se provi a incollare un "numero" a una "parola", la macchina si ferma immediatamente e grida: "Errore di tipo!" prima che venga fatto qualsiasi danno.

Il documento presenta questo nuovo interprete, che è il primo del suo genere a utilizzare un sistema logico specifico a tre vie. Invece di dire solo "Sì" (funziona) o "No" (non funziona), questo sistema può dire "Sbagliato" (è un errore di tipo). Gli autori non si sono limitati a ipotizzare che questo potesse funzionare; hanno scritto il codice, costruito l'interprete e lo hanno testato con diversi programmi logici. Hanno dimostrato che il loro strumento è in grado di individuare con successo gli errori sia nelle istruzioni (il programma) che nelle domande (le query) che altri strumenti potrebbero mancare. Hanno anche dimostrato di poter indicare esattamente la riga di codice specifica che causa il problema, agendo come un detective che non si limita a dire "è avvenuto un crimine", ma indica esattamente il sospetto. Sebbene ammettano che il loro strumento non sia ancora perfetto e necessiti di ulteriori test, le loro simulazioni dimostrano che questo nuovo modo rigoroso di controllare i programmi Prolog è un modo praticabile e potente per catturare gli errori precocemente.

La storia di MaudeTypedLog

Il Problema: La "Colla" che non controlla
Prolog è un linguaggio usato per risolvere enigmi e problemi di logica. Funziona prendendo una lista di fatti e regole e cercando di incollarli insieme per rispondere a una domanda. Tradizionalmente, Prolog è "non tipizzato". Immagina di giocare a un gioco in cui devi abbinare i calzini. In Prolog, puoi provare ad abbinare un calzino rosso con una scarpa blu, e il gioco continua a provare finché non si arrende. Non urla: "Ehi, questi non sono nemmeno dello stesso tipo di oggetto!", finché non arriva alla fine, e anche allora, potrebbe semplicemente dire "Nessuna corrispondenza" senza spiegare che il problema era la scarpa.

Gli autori sostengono che questo sia pericoloso. A volte, un programma potrebbe dire "No" perché la risposta è realmente "No" (come il numero 2 che non è nella lista [1, 3]), ma altre volte dice "No" perché hai tentato di fare qualcosa di impossibile (come mettere un numero dentro una lista di parole). Prolog tratta entrambi i casi come un "No" identico, il che è confusionario.

La Soluzione: Un semaforo a tre vie
I ricercatori hanno costruito MaudeTypedLog, un interpreto che esegue i programmi Prolog ma aggiunge un rigoroso "Controllo di Tipo" ad ogni singolo passaggio. Invece di un semplice semaforo con solo Verde (Vai) e Rosso (Stop), questo sistema ha una terza luce: Giallo (Sbagliato).

• Verde (Vero): I pezzi si incastrano, i tipi corrispondono e la logica funziona.
• Rosso (Falso): I pezzi rispettano i tipi, ma la logica non funziona (ad esempio, 2 non è nella lista).
• Giallo (Sbagliato): I pezzi non possono incastrarsi perché sono del tipo sbagliato (ad esempio, cercare di sommare una parola a un numero).

Questa luce "Gialla" è l'innovazione chiave. Permette al sistema di fermarsi immediatamente quando rileva un errore di tipo, invece di lasciare che il programma vada in crash in seguito o fornisca una risposta confusionaria.

Come l'hanno costruito
Per far sì che ciò accadesse, gli autori hanno utilizzato uno strumento potente chiamato Maude. Maude è come un motore di simulazione super-potenziato capace di riscrivere le regole molto velocemente. Gli autori hanno preso le regole di Prolog e le hanno riscritte all'interno di Maude.

1. L'Algoritmo di Unificazione Tipizzata: Questo è il motore centrale. In un normale Prolog, l'unificazione è il processo di rendere due cose uguali. In MaudeTypedLog, hanno creato un algoritmo di "Unificazione Tipizzata". Prima di tentare di incollare due cose insieme, controllano i loro "tipi". Se i tipi non corrispondono, non si limitano a fallire; restituiscono un segnale specifico di "Sbagliato".
2. Risoluzione TSLD: Questo è il nome altisonante per il metodo che usano per risolvere gli enigmi. È una versione aggiornata del metodo standard di risoluzione SLD di Prolog. Il "T" sta per "Typed" (Tipizzato). Costruisce un albero di tutti i modi possibili per risolvere un problema. Se un ramo dell'albero incontra un segnale di "Sbagliato", quel ramo viene tagliato immediatamente e il sistema sa esattamente quale regola ha causato l'errore.

Cosa hanno scoperto
Gli autori hanno testato il loro nuovo interprete con diversi esempi.

• Esempio 1: Hanno creato un programma in cui una regola chiamata r cerca di trovare un numero che sia sia in una lista di numeri che in una lista di lettere. Il sistema ha identificato correttamente che, mentre alcuni percorsi funzionavano (trovando il numero 1), altri incontravano un segnale di "Sbagliato" perché cercavano di mescolare numeri e lettere.
• Esempio 2: Hanno creato un programma con un errore di tipo nascosto. Una regola cercava di inserire una lettera in uno spazio destinato a un numero. Quando hanno eseguito il comando "check", MaudeTypedLog non ha solo detto che il programma era fallito; ha indicato direttamente la regola specifica (clausola 3) che era la colpevole.

I risultati hanno mostrato che lo strumento funziona esattamente come previsto dalla teoria. Può rilevare errori di tipo sia nei programmi stessi che nelle domande poste al programma.

Cosa non può ancora fare
Gli autori sono onesti riguardo ai limiti del loro attuale lavoro. Il loro strumento è un prototipo. Non gestisce ancora tutte le funzioni matematiche complesse che Prolog solitamente possiede (come calcolare radici quadrate o sommare numeri dinamicamente). Non hanno ancora testato lo strumento su le enormi librerie di regole che i programmi Prolog professionali utilizzano. Suggeriscono che, in futuro, dovranno insegnare allo strumento come gestire queste funzioni matematiche avanzate e strutture dati più complesse come gli alberi.

Perché è importante
Questo articolo non sostiene di aver risolto ogni problema dell'informatica. Inveve, offre un modo più chiaro di guardare alla programmazione logica. Usando Maude per creare un interprete tipizzato e rigoroso, gli autori hanno dimostrato che è possibile catturare gli errori precocemente e localizzarli esattamente dove avvengono. È come dare a un costruttore un livello laser che non solo ti dice che una parete è storta, ma ti dice anche esattamente quale mattone ha la forma sbagliata, così puoi sistemarlo prima che la casa cada.