Chapter 8 Conclusioni

Il problema dello sfruttamento delle nuove tecnologie basate su XML per la memorizzazione, l'indicizzazione e la condivisione di documenti matematici è destinato a diventare sempre più rilevante nel prossimo futuro, quando, incentivata dall'introduzione di standard per la visualizzazione e lo scambio di espressioni matematiche, quali MathML ed OpenMath, la comunità scientifica inizierà a mettere in linea sul World Wide Web librerie distribuite di documenti matematici.

Il solo progresso delle tecnologie Web non sarà, però, sufficiente a soddisfare le aspettative degli utenti: al fine di poter verificare la correttezza dei documenti e per permettere di effettuare ricerche complesse all'interno delle librerie, diventa necessario considerare anche la semantica dei documenti matematici; questa è l'argomento di studio della Logica Formale e della Teoria della Dimostrazione, i cui prodotti concreti sono i proof-assistant.

I proof-assistant, utilizzati fino ad ora da gruppi estremamente ristretti di persone, non hanno subito l'evoluzione, trainata dalle nuove tecnologie Web, a cui sono stati soggetti la maggior parte degli applicativi software negli ultimi anni e che ha portato al passaggio dal modello application-centric, in cui l'enfasi è posta sull'applicazione, a quello document-centric, focalizzato sul documento; al contrario, questi strumenti sono cresciuti negli anni in modo disorganizzato, comprendendo sempre più funzionalità ed evolvendo in sistemi sempre più monolitici e refrattari alle modifiche. Un altro aspetto negativo degli attuali proof-assistant è che l'attenzione viene posta esclusivamente sugli aspetti di provabilità dei teoremi, ovvero sulla ricerca delle dimostrazioni, trascurando il prodotto di tale ricerca, che sono le prove stesse.

Lo scopo di questa tesi è quello di studiare l'integrazione di questi due mondi al fine di rendere possibile la creazione di librerie distribuite di conoscenza matematica formalizzata; come effetto collaterale, si ottiene la ristrutturazione in chiave modulare dell'architettura dei proof-assistant. Per raggiungere questo ambizioso obiettivo, è necessario affrontare numerosi problemi, sia teorici che di natura tecnologica, alcuni dei quali privi di soluzioni soddisfacenti.

Concretamente, è stata proposta un'architettura generale comprendente strumenti per la creazione, il mantenimento e lo sfruttamento di una libreria di questo tipo e sono stati progettati e realizzati alcuni di questi strumenti per dimostrare la realizzabilità del progetto e individuarne le problematiche. Fra gli strumenti sviluppati vi sono stati:

un modulo per esportare teorie matematiche dal formato interno utilizzato dal proof-assistant Coq ad un'opportuna istanza di XML;
un proof-checker per gli oggetti matematici memorizzati in formato XML;
un sistema di stylesheet per la rimatematizzazione del contenuto formale attraverso l'applicazione delle usuali notazioni matematiche bidimensionali;
tool per la gestione degli aspetti di distribuzione della libreria (accesso ai documenti remoti);
un'interfaccia Web e un'interfaccia in Gtk per il browsing della libreria.

Durante la progettazione, l'enfasi è stata posta sulla facilità di pubblicazione e accesso ai documenti della libreria e su quelle tematiche che vengono normalmente trascurate negli attuali proof-assistant, quali la visualizzazione delle prove.

Nella forma, il progetto è decisamente originale, anche se è correlato a numerosi altri progetti nei campi del web-publishing, delle digital-library e del proof-reasoning. Il lavoro più affine è il progetto MathWeb, nato contemporaneamente e indipendentemente dal progetto HELM sviluppato all'Università di Bologna e il cui nucleo iniziale è rappresentato dal prodotto di questa tesi. Il prossimo paragrafo è dedicato ad un confronto esaustivo dei due progetti; nel paragrafo 8.2, infine, vengono elencati i possibili sviluppi futuri.

8.1 Confronto fra i progetti HELM e MathWeb

Il progetto MathWeb, coordinato dal Prof. Michael Kohlhase, è nato recentemente come evoluzione del progetto Omega, di cui ha allargato gli obiettivi e le finalità. Omega è un progetto a lungo termine sviluppato presso Universität des Saarlandes (città di Saarbrücken, Germania) dal gruppo del Prof. Jörg Siekmann, attualmente composto da quattordici fra ricercatori e professori, coadiuvati da una decina di studenti. Lo scopo del progetto è lo sviluppo di un sistema in grado di incentivare l'utilizzo dei theorem-prover nello sviluppo e nell'insegnamento della matematica. L'architettura, pesantemente distribuita, prevede numerosi sottosistemi, fra i quali un proof planner (pianificatore della prova), tool per la formulazione di problemi, theorem-prover general-purpose o specializzati in vari domini matematici, interfacce per l'utilizzo di sistemi per la computer-algebra, generatori pseudo-automatici di dimostrazioni per analogia e sofisticati meccanismi di intelligenza artificiale per la presentazione delle prove in linguaggio naturale. Le nuove tematiche affrontate da MathWeb rispetto al progetto Omega sono quelle della memorizzazione delle teorie in linguaggio XML, della pubblicazione on-line di librerie distribuite di documenti matematici e della loro resa in formati standard di presentazione¹.

Sebbene gli obiettivi di MathWeb siano molto più ambiziosi di quelli di Helm, diversi aspetti possono essere proficuamente confrontati:

L'individuazione del contenuto informativo delle prove
La presentazione delle prove
Il formato di codifica dei documenti matematici
Il modello di distribuzione
I meccanismi di indicizzazione e ricerca

8.1.1 Il contenuto informativo delle prove

Mentre noi abbiamo individuato nei l-termini il vero contenuto informativo delle dimostrazioni, in Omega non solo la prova, ma anche l'intero processo con la quale è stata ottenuta è rilevante. Pertanto, quello che in Omega viene salvato su disco è l'intero proof-plan, ovvero la storia della dimostrazione, comprendente la sequenza di tattiche applicate e tutte le informazioni rese disponibili dai tool invocati. Poiché Omega, per la risoluzione di alcuni goal o la riduzione di espressioni matematiche, si interfaccia con sistemi esterni, per esempio Maple, non sarebbe possibile per il sistema la costruzione sistematica di un l-termine che abiti la tesi. Pertanto, la scelta di considerare l'intero proof-plan come contenuto informativo è pienamente giustificabile. D'altro canto, i l-termini di CIC, unico sistema logico attualmente supportato da HELM, contengono indubbiamente tutta l'informazione richiesta e questo giustifica la loro identificazione con il contenuto informativo delle prove. La maggiore concisione e pulizia di HELM viene, però, penalizzata durante la fase di presentazione delle prove.

8.1.2 La presentazione delle prove

In Omega, avendo a disposizione l'intero proof-plan, la generazione automatica della descrizione in linguaggio naturale di una prova è sicuramente facilitata rispetto a sistemi in cui il formato delle prove è meno informativo. Indubbiamente, grazie all'utilizzo di tecniche evolute di intelligenza artificiale, i risultati ottenuti in questo campo sono notevoli, specie se confrontati con sistemi analoghi, come il modulo Natural di Coq [CKT95]. In generale, comunque, la tecnologia attuale non sembra, e forse non sarà mai, in grado di generare descrizioni che sembrino veramente naturali per prove di notevole complessità. In HELM il problema viene evitato ricorrendo alle annotazioni informali, grazie alle quali l'utente ha la possibilità di descrivere liberamente le prove formali. Questo approccio è suscettibile di due critiche: la prima è che, in questo modo, non è garantita alcuna corrispondenza fra la prova formale e la sua annotazione informale; la seconda riguarda l'onere per l'utente di annotare ogni prova, compito estremamente complesso se effettuato successivamente alla ricerca della dimostrazione formale. Per quanto riguarda la prima critica, la possibilità di richiamare il proof-checker sulla prova formale ne garantisce la correttezza, mentre la possibilità di deannotare progressivamente il l-termine permette di individuare le discrepanze fra le due descrizioni. In presenza di dimostrazioni complesse, inoltre, la dimostrazione ottenuta automaticamente potrebbe essere cosí difficile da comprendere da diventare inutile, mentre la leggibilità di quella annotata è sotto il diretto controllo dell'utente. A parte questi casi estremi, comunque, la critica rimane fondata, anche se il feeling dell'autore è che i matematici possano sempre preferire una dimostrazione informale, eventualmente inesatta, ma scritta con l'acume e la sensibilità dell'umano rispetto a quella, sicuramente corretta ma artificiosa, generata automaticamente. Inoltre, un importante punto a favore della scelta di HELM è la possibilità, da parte dei singoli utenti, di riannotare a piacimento le dimostrazioni. Per esempio, ciò che può essere ovvio per l'autore può non esserlo per chi legge la dimostrazione, che può scegliere di deannotare la parte di dimostrazione che non capisce e riannotarla in maniera differente. Questa possibilità, indubbiamente auspicabile, è ovviamente interdetta nei sistemi che generano automaticamente la dimostrazione in linguaggio naturale.

La seconda critica, quella sulla difficoltà di annotare le prove, è invece largamente infondata per due motivi. Il primo è che l'uso delle annotazioni non impedisce la loro generazione tramite strumenti automatici, che possono eventualmente sfruttare anche informazione non contenuta nel l-termine, come la sequenza delle tattiche. In questo senso, possiamo dire che la generazione automatica della presentazione di una prova in linguaggio naturale è solo un caso particolare della scrittura di una annotazione. Inoltre, le annotazioni potrebbero essere generate, automaticamente o manualmente, durante la scrittura delle prove, permettendo una descrizione massimamente fedele al ragionamento effettuato. Il secondo motivo riguarda la possibilità di semplificare la procedura ricorrendo a tool dotati di elaborate interfacce grafiche e in grado di prevenire l'utente suggerendogli la giusta sequenza di annotazione.

8.1.3 Il formato dei documenti matematici

Mentre HELM si affida ad un generico formato XML per i documenti formali ed a MathML per la loro rappresentazione semi-formale, per Omega² si è scelto un formato proprietario delle prove, che vengono scritte in Allegro Lisp; MathWeb, invece, adotta un'estensione non standard di OpenMath per la rappresentazione dei documenti matematici, chiamata OmDoc. La scelta del formato proprietario per le prove è coerente con la visione distribuita, ma essenzialmente application-centric, di Omega: il gestore del proof-plan, il vero cuore di Omega, può connettersi a diversi tool esterni per la ricerca delle prove; per poter lavorare sulle prove, però, è necessario ricorrere a questo strumento. Pertanto, Omega è suscettibile alle critiche al software application-centric (vedi paragrafo 1.2.2), mentre HELM, che aderisce al paradigma content-centric, ne è immune.

Per quanto riguarda il formato di rappresentazione dei documenti matematici, necessariamente contenenti descrizioni delle prove, la scelta di MathWeb è caduta su OpenMath. Poiché in Omega non vi è una rappresentazione XML delle prove, era necessario per loro trovare un formato che potesse codificare sia la presentazione, che la semantica semi-formale delle espressioni matematiche: l'unico standard che soddisfa queste richieste è OpenMath. Per quanto riguarda HELM, invece, la presenza dei file XML che mantengono il l-termine formale permette di utilizzare MathML content come rappresentazione semi-formale, con in più la possibilità di seguire gli XLink per risalire alla semantica formale. Entrambe le scelte hanno dovuto affrontare problemi analoghi, ovvero la trasformazione dei documenti semi-formali in un opportuno formato di presentazione e il problema della rappresentazione del livello degli oggetti. Per le trasformazioni, entrambi i gruppi di sviluppo hanno optato per la scelta standard di stylesheet XSLT, utilizzando HTML o MathML presentation come formati di output³.

Più interessante è il confronto fra le soluzioni adottate per affrontare il problema che sia MathML che OpenMath sono nati per codificare espressioni e non interi documenti matematici contenenti, per esempio, definizioni e teoremi. La scelta di MathWeb è stata la definizione di un'opportuna estensione di OpenMath, chiamata OMDoc: i documenti OMDoc comprendono non solo oggetti matematici, ma anche i corrispondenti metadati e frammenti di stylesheet XSLT utilizzati per fini presentazionali. I principali elementi XML di OMDoc per descrivere oggetti matematici sono annotazioni informali, definizioni, teoremi, esempi ed esercizi. Attributi vengono utilizzati, per esempio, per classificare ulteriormente teoremi in lemmi, corollari, etc. Per quanto riguarda i metadati, fra i quali sono presenti quelli Dublin Core, è impossibile non criticare la scelta di codificarli non utilizzando lo standard RDF. Complessivamente, è criticabile la scelta di affiancare nello stesso documento dati, metadati e presentazione: poiché, tipicamente, le applicazioni sono interessate esclusivamente ad uno di questi aspetti alla volta, questo le costringe ad un inutile parsing di informazione inutilizzata. Inoltre, in questo modo si rinuncia all'importante separazione del contenuto dalla presentazione, che rappresenta uno degli obiettivi principali dell'introduzione degli standard XML e XSL. Sotto questo aspetto, l'architettura di HELM, che prevede la separazione in file distinti di metadati, notazioni e oggetti, con l'aggiunta di teorie per assemblare e strutturare questi ultimi, risulta essere molto più pulita. Inoltre, in questo modo, è possibile definire teorie distinte basate sugli stessi oggetti senza doverli replicare. Il prezzo da pagare è la perdita dell'unità del documento, che costringe sovente al downloading di numerosi file e all'utilizzo massiccio di XLink. Mentre il secondo punto non rappresenta un vero problema, il primo può essere risolto implementando getter più elaborati, in grado di richiedere il download contemporaneo di diversi file, che possono essere compressi durante la trasmissione (vedi 4.1). Questa soluzione, però, richiede un'attiva collaborazione da parte dei server di distribuzione, contravvenendo al terzo requisito di HELM (vedi paragrafo 1.3.1).

8.1.4 Il modello di distribuzione

Gli obiettivi dei modelli di distribuzione di HELM (vedi capitolo 4) e MathWeb sono profondamente diversi. Brevemente, MathWeb si propone di affrontare il problema dei diritti d'autore sui documenti scientifici presenti in rete. Per questo motivo, viene richiesta l'esistenza in rete di una e una sola copia per ogni documento. È possibile la migrazione della copia: per esempio, quando l'autore pubblica l'articolo, la copia deve migrare dal suo server a quello dell'editore. Per evitare la rottura di collegamenti fra documenti a causa della migrazione delle copie, sono previsti appositi puntatori dalle precedenti locazioni all'attuale. Poiché l'esistenza di una sola copia crea inevitabili colli di bottiglia, vengono proposti meccanismi di caching per aumentare le prestazioni. Infine, è prevista la possibilità di rendere obsoleto un documento (per esempio, a causa di definizioni errate).

Le critiche al modello di MathWeb sono innumerevoli. In primo luogo, l'esistenza di un'unica copia che viene fatta migrare è soggetta a tipiche problematiche di fault-tolerance: la migrazione è rischiosa e il server che mantiene l'unica copia è un ``single point of failure''. Il sistema di puntatori richiede meccanismi di path compression per evitare la creazione di lunghe catene per giungere alla copia cercata e, poiché i documenti possono essere modificati (rendendoli obsoleti), opportune politiche debbono essere implementate per sincronizzare i cache. Durante partizionamenti della rete, la sincronizzazione può essere perduta o, peggio, l'informazione sulla locazione dell'unica copia potrebbe diventare obsoleta, con conseguente impatto, per esempio, sui diritti economici di accesso al documento. Infine, chiunque voglia pubblicare o accedere ad un articolo deve avere a disposizione un host su cui sia installato un server MathWeb. Si confronti quest'ultima osservazione con gli antitetici requisiti di HELM (paragrafo 1.3.1).

Ferme restando le differenze fra gli obiettivi dei due modelli di distribuzione, quello di MathWeb mette in luce due mancanze di HELM. La prima è l'impossibilità di rendere obsoleto un documento. La soluzione più semplice, ma anche scarsamente soddisfacente, sarebbe allestire uno o più server che mantengano la lista dei documenti obsoleti. Il secondo è la mancanza di garanzie sull'esistenza di un documento referenziato da un secondo; in particolare, se costruisco una teoria A basandomi su definizioni e teoremi date in una teoria B, quando l'ultima copia di B viene cancellata tutte le copie di A perdono di significato. Supporre che esista per sempre almeno una copia di ogni documento è quantomeno utopistico. Pertanto, è ragionevole supporre che, se sono interessato ad un documento A di cui esistono poche copie, me ne memorizzi una su disco per evitarne la perdita, mettendola, poi, a diposizione di tutti. Quindi, il requisito di HELM che prevede l'esistenza di più copie di uno stesso documento, tutte identificate dallo stesso nome logico, risolve concretamente il problema. Per inciso, in questo modo avviene una naturale selezione dei documenti sulla base della loro rilevanza: quelli scarsamente referenziati verranno prima o poi cancellati, mentre quelli interessanti aumenteranno la loro diffusione.

8.1.5 I meccanismi di indicizzazione e ricerca

I due progetti differiscono notevolmente anche per quanto riguarda i meccanismi di indicizzazione e ricerca. HELM adotta il tradizionale approccio dei motori di ricerca, che visitano i siti di distribuzione indicizzandone efficacemente i documenti grazie all'utilizzo di metadati descritti nello standard RDF. Comuni browser possono quindi essere utilizzati per contattare i motori di ricerca. MathWeb, al contrario, non prevede motori di ricerca, ma affida l'indicizzazione dei documenti ai server già introdotti dal modello di distribuzione. In questo modo, le query non vengono effettuate ad un singolo server, ma, attraverso un programma apposito, devono essere contattati tutti quelli esistenti. La risoluzione della query diventa quindi un problema distribuito, reso mediamente complesso dalle richieste prestazionali in presenza di un gran numero di server. Questa architettura, abbastanza complessa, non è sicuramente giustificata da problemi di fault tolerance, risolvibili attraverso l'utilizzo di un numero sufficiente di (istanze di) motori di ricerca. Anzi, la caduta di un server impedisce perfino la ricerca sui documenti ivi conservati. In compenso, l'elevata complessità computazionale della risoluzione di query per niente banali, come quelle presentate a pagina 1, necessita di sistemi distribuiti con bilanciamento del carico e ricerche in parallelo, simili a quelli di MathWeb. Nel modello di HELM, questo problema non viene trascurato, ma semplicemente scaricato sull'architettura del motore di ricerca, per la quale si possono adottare soluzioni analoghe a quelle di sistemi come Yahoo o Altavista, che sono in grado di soddisfare migliaia di richieste contemporaneamente.

8.2 Lavori Futuri

Grazie agli ambiziosi obiettivi del progetto, sono possibili numerosi sviluppi del lavoro svolto finora; alcuni sono mirati al miglioramento e al consolidamento di quanto già realizzato e richiedono collaborazione da parte di altri gruppi di ricerca, come il team responsabile dello sviluppo di Coq; altri sono estensioni del sistema al fine di considerare le problematiche che non sono ancora state affrontate, quali l'indicizzazione tramite metadati dei documenti della libreria e i meccanismi di ricerca. Infine, affinché l'intero progetto possa considerarsi avviato con successo, è necessario che si formi una comunità di utenti e che nuovi gruppi di sviluppo integrino nell'architettura generale gli strumenti per la gestione di formalismi logici diversi da CIC. Segue una rassegna dei principali sviluppi possibili:

Architettura generale: Per verificare la validità dell'architettura generale di HELM, è necessario considerare almeno un altro sistema logico, diverso da CIC, e sviluppare per esso i moduli corrispondenti a quelli già implementati per CIC.
Modulo di esportazione da Coq: Al fine di esportare in modo corretto tutta l'informazione necessaria, eliminando la necessità di ricorrere alla successiva fase di riparazione dei file, è necessaria una stretta collaborazione con il team di sviluppo di Coq, già prevista per l'autunno 2000. In tale occasione, si provvederà anche all'adozione di alcune nuove estensioni a CIC, previste per la nuova versione di Coq, fra le quali l'introduzione di un costrutto di naming, che risulterà utile anche per la resa delle prove, e la sostituzione del meccanismo di cottura con un altro più semplice, ma ad esso equivalente.
Getter: Nei due getter già sviluppati potranno essere integrate le rimanenti funzionalità opzionali descritte nel paragrafo 4.1. Inoltre, potrà essere necessario rivedere il meccanismo di sintesi dei documenti a mano a mano che aumenta il numero degli eventuali file sorgenti (oggetto, dei tipi sintetizzati, contenenti annotazioni, etc.).
CIC Proof-checker: Per completare l'implementazione del proof-checker, è necessario considerare la gestione del livello degli universi. Inoltre, una volta aggiornato il meccanismo di esportazione da Coq alla versione 7.0, sarà necessario modificare l'intero proof-checker per utilizzare le nuove estensioni a CIC.
Stylesheet notazionali: Oltre all'aggiornamento degli stylesheet di default dovuto alle nuove estensioni di CIC, rimane da valutare la realizzabilità di un meccanismo per la generazione semi-automatica degli stylesheet forniti dagli utenti.
Meccanismi di annotazione: È necessario superare i problemi tecnologici che rendono quasi inutilizzabile l'attuale prototipo per l'annotazione, al fine di poter intraprendere un periodo di sperimentazione per individuare le problematiche legate all'annotazione e la sua effettiva importanza per la rappresentazione delle prove in linguaggio naturale.
Sviluppo di proof-assistant: Un interessante sviluppo, inizialmente non previsto, consiste nell'implementazione di un proof-assistant modulare basato sul formato XML di rappresentazione dei dati. L'enfasi verrebbe posta sulla naturalezza dei l-termini generati dalle tattiche, al fine di produrre prove facilmente annotabili e simili alle corrispondenti prove cartacee non formalizzate. Inoltre, potrebbe essere investigata la possibilità di annotare il termine durante la ricerca della prova.
Meccanismi di indicizzazione e ricerca: Debbono ancora essere completamente sviluppati, anche se sono già chiare le linee guida da seguire.
Comunicazione dell'informazione fra differenti sistemi logici: Una volta che il progetto sia ben avviato e siano stati sviluppati gli strumenti affinché più sistemi logici possano contribuire alla libreria, si potrà affrontare il problema più profondo sollevato dalla creazione di librerie di documenti matematici codificati in formalismi eterogenei, ovvero quello dell'uso nelle dimostrazioni di definizioni e teoremi dati in un diverso formalismo.

1: Al momento della pubblicazione di questa tesi, la ristrutturazione del progetto Omega in due progetti distinti, Omega e MathWeb, non è ancora terminata e non è del tutto chiaro quale progetto affronterà alcune problematiche. Nel resto del capitolo, la cui prima stesura risale a prima dell'inizio della scissione, i due progetti vengono talvolta identificati.
2: Le caratteristiche di Omega descritte in questo paragrafo sono prese da una serie di documenti trovati sul sito del progetto e ora non più on-line a causa della sua ristrutturazione. Pertanto, le informazioni date potrebbero essere obsolete.
3: MathWeb fornisce anche uno stylesheet verso L^AT_EX. Tale trasformazione può essere ottenuta facilmente applicando in cascata lo stylesheet per ottenere MathML presentation e uno di quelli, disponibili in rete, per passare da questo formato a L^AT_EX; lo stylesheet verso MathML, previsto in MathWeb, non è però ancora stato scritto.