Chapter 3 Esportazione in XML da Coq di oggetti CIC

La prima fase dello sviluppo di HELM è stata la progettazione e l'implementazione di un meccanismo di esportazione delle teorie scritte in CIC da Coq in XML. La prima decisione importante è stata la scelta di quale informazione dovesse essere esportata. In particolare, è risultato subito evidente che non tutta l'informazione è significativa. Il principale criterio utilizzato per determinare la rilevanza dell'informazione è stato porre l'enfasi sul framework logico e non sul proof-assistant. In particolare, dovrebbe essere esportata tutta e sola l'informazione necessaria ad un qualsiasi sistema che lavori sulla stessa versione di CIC. Pertanto, si è scelto di non esportare:

Regole di parsing Queste sono chiaramente dipendenti dal sistema utilizzato. In particolare, dipendono dalla scelta di Coq di utilizzare una notazione testuale e uno degli obiettivi di HELM è proprio il superamento delle notazioni testuali per i proof-assistant in favore del recupero dell'usuale notazione matematica bidimensionale.
Regole di pretty-printing Queste regole vengono utilizzate in Coq per determinare la presentazione delle prove. In un sistema aperto come HELM, la loro resa deve poter essere influenzata da diversi parametri, fra i quali le scelte notazionali effettuate dall'autore del documento, le preferenze degli utenti e le capacità del browser che l'utente ha a disposizione. Per esempio, l'autore del documento potrebbe aver indicato la rappresentazione dei vettori per colonna, mentre l'utente deve essere libero, se preferisce, di cambiare la notazione in quella per righe. Inoltre, la notazione utilizzata in una resa HTML o testuale di un documento deve necessariamente essere più grezza di quella MathML e sicuramente è diversa da quella che deve richiedere un utente non vedente.
Tattiche utilizzate nelle prove e termini impliciti Innanzi tutto, anche le tattiche sono tipicamente dipendenti dal proof-assistant utilizzato; inoltre, come già spiegato a pagina 8, HELM si basa sulla convinzione che non rappresentino il reale contenuto informativo delle prove e non siano in corrispondenza con il livello al quale si vorrebbe leggerle. Pertanto, si è scelto di esportare esclusivamente i l-termini. Inoltre, adeguandosi alla politica di Coq che inferisce i termini impliciti senza introdurli a livello CIC (vedi paragrafo 2.2.1), i l-termini esportati apparterranno, almeno in questa prima implementazione, al sistema logico non esteso con tipi impliciti.
Informazione ridondante aggiunta per velocizzare l'elaborazione Coq aggiunge diverse informazioni ai termini di CIC per velocizzare le elaborazioni. Per esempio, durante il type-checking di una definizione induttiva, Coq individua quali sono i parametri ricorsivi dei costruttori e aggiunge l'informazione nelle loro definizioni per utilizzarla poi durante la verifica della condizione GD per le definizioni per punto fisso. Se questa informazione fosse esportata, diverrebbe un esempio di informazione ridondante, sicuramente inutile per il browsing ed eventualmente inutile per gli altri proof-checker, che dovrebbero comunque verificarne la veridicità. Abbiamo, quindi, deciso di non esportarla in accordo ad un principio di minimalismo: nessuna informazione ridondante deve essere esportata. Quando il principio non viene seguito, ogni volta che un file XML viene utilizzato si deve controllare la consistenza dell'informazione ridondante, talvolta allo stesso costo computazionale del calcolarla¹. Purtroppo, l'indistinguibilità dei cast ridondanti da quelli necessari (vedi paragrafo 2.2.1) ci ha obbligato ad esportarli ugualmente.

L'informazione da esportare si riduce quindi ai l-termini, agli oggetti e alla loro strutturazione. La prossima decisione, quindi, diventa la scelta di come mappare queste entità su file XML e directory che li contengano.

Mentre gli oggetti esistono in tutti i proof-assistant, i termini sono tipici di quelli basati sull'isomorfismo di Curry-Howard. Inoltre, i termini non compaiono mai isolati, ma solo all'interno degli oggetti. Per questi motivi, l'unità atomica di informazione è rappresentata da questi ultimi e abbiamo scelto di associare un file XML ad ogni oggetto, ad eccezione dei blocchi di tipi (co)induttivi definiti in maniera mutuamente ricorsiva, ai quali viene assegnato un unico file XML il cui nome è quello del primo tipo induttivo ivi definito. Questa scelta è stata motivata anche dalla volontà di identificare gli oggetti tramite section path (vedi paragrafo 2.2.5) e non tramite il loro nome. Conseguentemente, si è scelto di esportare tutti i termini nella loro forma non cucinata, che è quella in cui vengono definiti dagli autori.

Una volta deciso che ogni oggetto diventa un file XML, ad ogni sezione, e conseguentemente ad ogni file ``.v'', si può far corrispondere un directory. Come è naturale in Coq strutturare ulteriormente i file ``.v'' in directory (che non hanno un corrispondente nella rappresentazione interna di Coq), cosí abbiamo deciso di utilizzare altri directory per rappresentare le sezioni e di far tenere conto ai section path anche delle prime. Come conseguenza, possiamo organizzare l'intera libreria di HELM in un unico albero invece di avere una foresta. Si noti che non esiste nessun modo per discriminare i directory corrispondenti alle sezioni dagli altri: in effetti, possiamo tranquillamente pensare ai nuovi directory come a sezioni prive di variabili contenenti esclusivamente altre sezioni. Per esempio, la definizione della somma fra numeri naturali (plus), che è una costante definita in Coq nella sezione Peano del file INIT.v, è stata esportata con il path relativo alla radice della libreria di HELM ``coq/INIT/Peano/plus.con.xml''. Si noti che, per mantenere separati gli spazi dei nomi, è stato scelto di utilizzare suffissi diversi per specificare le classi degli oggetti: ``.con'' per le costanti (definizioni e assiomi), ``.ind'' per i tipi induttivi e ``.var'' per le variabili.

In accordo con il modello di distribuzione, che verrà descritto nel prossimo capitolo, è stato poi associato ad ogni file XML un nome logico, sotto forma di URI ottenuto anteponendo al pathname relativo del file il prefisso ``cic:/'' ed eliminando il suffisso costante ``.xml''. Per esempio, l'URI della somma fra numeri naturali diventa ``cic:/coq/INIT/Peano/plus.con''

Fino ad ora abbiamo affrontato il problema di preservare l'organizzazione in sezioni degli oggetti, che è solo una parte dell'informazione di strutturazione di Coq. Infatti, nella libreria del sistema esiste un ordinamento totale fra le definizioni degli oggetti all'interno di uno stesso file ``.v'' e un ordinamento parziale fra questi, dovuto alle dipendenze di almeno un oggetto di un file da un altro file ``.v''. Esiste, poi, un secondo ordinamento parziale, coerente con il primo², dovuto alle dipendenze fra gli oggetti CIC³. Confrontando i due ordinamenti, si nota che il primo può essere considerato semplicemente una linearizzazione accidentale del secondo, dovuta all'ordine con il quale sono state date definizioni indipendenti. Un secondo punto di vista, invece, è interpretare l'ordinamento come quello voluto dall'autore per presentare la teoria matematica. In effetti, quando in Coq si scrive una teoria (un file ``.v''), si compiono contemporaneamente due operazioni: la prima è la scrittura di definizioni e teoremi su queste; la seconda è la scelta dell'ordine in cui presentarle. Nell'usuale pratica matematica, invece, le due operazioni sono usualmente distinte e sequenziali: spesso, per esempio, vengono scritti articoli componendo in maniera differente definizioni e teoremi sviluppati in precedenza, magari presi da fonti diverse. In Coq, come spiegheremo fra poco (paragrafo 3.3), abbiamo voluto distinguere chiaramente l'output delle due fasi, individuando, oltre ai due livelli dei termini e degli oggetti, un terzo livello, formato da teorie. Come conseguenza, l'ordine totale di introduzione degli oggetti viene dimenticato durante l'esportazione da Coq, a favore di quello parziale, lasciato implicito, delle dipendenze logiche. Purtroppo, però, l'ordine implicito non è sufficiente per la cottura: la scelta di esportare gli oggetti nella loro forma non cucinata comporta la necessità di esportare tutte le informazioni necessarie alla loro successiva cottura, ovvero la lista, che deve essere ordinata, delle variabili dalle quali il termine dipende, chiamate ingredienti; l'ordinamento della lista, che deve essere coerente con quello parziale, è reso necessario per determinare la sequenza con la quale gli ingredienti devono essere astratti durante la cottura. Il dover fissare, in maniera largamente arbitraria, un ordinamento totale per la cottura, suggerisce fortemente che questa operazione possa essere rimpiazzata con un meccanismo più generale. In effetti, nella prossima versione di Coq, l'intera gestione delle variabili e delle sezioni dovrebbe cambiare, eliminando completamente la necessità di cucinare gli oggetti. Nel frattempo, si è resa necessaria, durante la fase di esportazione, l'aggiunta ad ogni oggetto cucinabile, ovvero tipi mutuamente (co)induttivi e costanti, della lista ordinata degli ingredienti da cui dipende.

L'ultima decisione da prendere prima di passare alla definizione del DTD per i file XML è la scelta di come discriminare oggetti fra loro sintatticamente indistinguibili, quali teoremi, lemmi, corollari e definizioni. Queste, infatti, sono tutte costanti cucinabili con un corpo e un tipo e la classificazione precedente non ha nessun valore a livello logico, ma solo a quello presentazionale⁴: per esempio, la scelta se considerare una data costante un teorema o un lemma è largamente arbitraria e può dipendere dal contesto in cui viene inserita; inoltre, è probabilmente del tutto indipendente dal sistema logico adottato. Pertanto, questa informazione non verrà inserita nei file XML corrispondenti agli oggetti, ma in quelli, descritti più avanti nel paragrafo 3.3, che li utilizzano per descrivere teorie matematiche.

3.1 Una critica all'approccio ``un oggetto, un file''

Proseguendo nell'implementazione di HELM, ci siamo resi conto che l'uso di un file XML per ogni teorema potrebbe essere proficuamente abbandonato in favore dell'uso di due file XML, uno per l'enunciato e uno per la dimostrazione. Esistono almeno due ragioni significative:

Spesso, sia durante il proof-checking che durante la sola visualizzazione, è necessario richiedere solamente il tipo, ovvero l'enunciato, di un teorema, che è diversi ordini di grandezza più piccolo della prova. Per ottenere questa informazione, però, è comunque necessario processare l'intero documento XML, con conseguente grossa inefficienza nel caso della soluzione ora adottata.
È possibile e talvolta usuale dare più di una dimostrazione per lo stesso teorema. Con la soluzione ora adottata, questo significa replicarne anche l'enunciato, con conseguente spreco di spazio disco.

Pertanto, nella prossima versione si adotterà la soluzione alternativa.

3.2 Il DTD per il livello dei termini e degli oggetti

Il DTD per i file XML degli oggetti CIC, al quale si farà riferimento in questo paragrafo, si trova in appendice A. I criteri che hanno guidato la sua definizione sono stati:

Separazione del livello dei termini da quello degli oggetti Gli elementi di markup del livello dei termini devono essere chiaramente distinti da quelli del livello degli oggetti. Il DTD deve essere il più possibile modulare per permettere la modifica di un livello con impatti minimi sull'altro.
Unicità del namespace I file devono utilizzare un solo namespace, per due motivi. Il primo è che le dimensioni dei file XML risultanti sono notevoli, con conseguenti alti tempi di parsing e trasmissione dei file via rete: l'utilizzo di un solo namespace riduce notevolmente le dimensioni dei file, permettendo di evitare tutti i prefissi. Il secondo motivo è che, in futuro, si preferisce avere un solo namespace per ogni sistema logico, al fine di evitarne la proliferazione.
Aderenza alla sintassi astratta di CIC Il DTD deve seguire il più possibile la sintassi astratta di CIC, evitando ogni forma di ridondanza, in accordo con il già citato principio di minimalismo.
Utilizzo degli URI per riferirsi ad altri oggetti
Leggibilità Per semplificare lo sviluppo e il debugging, si deve utilizzare un formato XML che agevoli la comprensione diretta del contenuto, anche a scapito della concisione. In particolare, chiunque conosca a fondo CIC dovrebbe essere in grado, con moderato sforzo, di interpretare un file XML.

Il quinto criterio ha suggerito l'adozione di opportuni tag di ``zucchero sintattico''. Seguendo i primi due criteri, si è scelto di utilizzare la capitalizzazione dei nomi dei tag XML per distinguere il livello dei termini da quello degli oggetti e dallo zucchero sintattico. In particolare, i tag tutti maiuscoli vengono utilizzati per i termini CIC e quelli tutti minuscoli per lo zucchero sintattico; i restanti tag, indicati con solo le iniziali maiuscole, sono utilizzati sia per i tag che specificano il tipo di oggetto, sia per delimitare gli elementi delle liste (per esempio, i singoli tipi induttivi in un blocco di tipi definiti mutuamente). Ad eccezione di target, tutti gli altri elementi di zucchero sintattico sono privi di attributi e non portano alcuna informazione. Su target vengono posti i binder, ovvero i nomi delle variabili legate nelle l-astrazioni e nei prodotti dipendenti. Se si volesse eliminare lo zucchero, il binder dovrebbe essere rispostato sull'elemento genitore: la scelta di metterlo su target è stata conforme al quinto criterio; la variabile, infatti, è legata esclusivamente nell'albero radicato in target e posizionarla su questo elemento aiuta notevolmente il colpo d'occhio.

Passiamo alle descrizioni degli ulteriori vincoli sintattici non esprimibili con il DTD e degli attributi che possono risultare non chiari:

ID Gli elementi XML corrispondenti ai termini e agli oggetti CIC hanno tutti l'identificatore univoco chiamato id. La motivazione della sua introduzione, legata esclusivamente alla presentazione, viene rimandata al paragrafo 6.1.
name Gli elementi XML corrispondenti agli oggetti hanno tutti l'attributo name che contiene il nome dell'oggetto che deve essere uguale a quello ottenuto dall'URI del file privato del suffisso. L'attributo, chiaramente ridondante, potrebbe essere eliminato nella prossima versione.
params È l'attributo degli elementi XML corrispondenti agli oggetti CIC cucinabili che specifica la lista ordinata degli ingredienti. Poiché questi sono variabili contenute nel percorso foglia-radice nell'albero delle sezioni/directory, i loro URI relativi a quella dell'oggetto hanno sempre una forma esclusivamente ascendente. Questo rende possibile utilizzare una codifica molto compatta, la cui sintassi è

n₁: v₁¹ ... v

m₁

1
n₂: v₂¹ ... v

m₂

2
... n_h: v_h¹ ... v

m_h

h

dove tutti i token debbono essere separati da un solo spazio, i due punti fanno parte del token precedente, n₁,...,n_h sono interi non negativi tali che n₁ > ... > n_h e v₁¹,...,v_h^m_^h sono nomi di variabili con la seguente semantica: il primo ingrediente da usare per cucinare l'oggetto deve essere la variabile il cui URI relativo è ottenuta giustapponendo per n_m volte la stringa ``../'' a quella vuota e concatenandoci v_mⁿ_^m e ``.var''; per le successive si ripete la stessa operazione scegliendo, nell'ordine, v_mⁿ_^m^{- 1},...,v₁¹.
paramMode È un attributo delle definizioni e dovrebbe sempre essere omesso. Viene spiegato nel paragrafo 3.4.
binder L'attributo binder associato ad un indice di de Brujin il cui valore è value deve sempre essere uguale al valore dell'omonimo attributo dell'elemento target del binder a cui si riferisce l'indice.
relUri È l'attributo di un riferimento a variabile VAR che ne indica l'URI relativo codificato come ``n,v'' dove v è il nome della variabile e n un intero non negativo con la stessa semantica di quelli dell'attributo params.
noType e noConstr Poiché ad un blocco di tipi (co)induttivi definiti in maniera mutuamente ricorsiva viene assegnato un solo file, per identificarne un tipo è necessario l'URI del file e l'indice, che viene fatto partire da zero, del tipo all'interno del blocco, memorizzato nell'attributo noType; per identificare un costruttore, alla precedente informazione è necessario aggiungere l'indice del costruttore, che viene fatto partire da uno⁵.

In appendice C è riportato, a titolo di esempio chiarificatore, il file XML corrispondente al teorema dimostrato nel paragrafo 2.3.2 e il cui l-termine è stato dato a pagina 54.

3.3 Il livello delle teorie

Come preannunciato, in HELM, oltre ai livelli dei termini e degli oggetti, che dipendono dal sistema logico, ne esiste un altro, quello delle teorie matematiche, che è indipendente dal logical framework. Nella nostra visione, una teoria è un documento matematico strutturato contenente oggetti scelti in modo quasi completamente libero da sezioni differenti. Scrivere una nuova teoria, dopo una fase preliminare nella quale vengono sviluppati nuovi oggetti, dovrebbe consistere nell'``assemblaggio'' nel documento matematico di questi oggetti e di altri definiti in precedenza.

È durante la creazione della teoria che la semantica degli oggetti viene ulteriormente arricchita e, per esempio, i teoremi vengono classificati come lemmi, fatti, corollari, etc. Ovviamente, ogni teoria, che viene codificata in un unico file XML, non include direttamente le definizioni degli oggetti, ma solamente riferimenti a questi. Come conseguenza, le teorie di HELM sono essenzialmente differenti dai file ``.v'' che nella terminologia di Coq vengono chiamati teorie. Per esempio, è possibile scrivere più teorie HELM che presentano in maniera differente gli stessi risultati, per esempio omettendo certe dimostrazioni o riportando anche i lemmi tratti da altre teorie. In Coq, questo non è possibile in quanto i teoremi comuni andrebbero replicati in entrambi i file ``.v'' e, a parte lo spreco di spazio disco, per il sistema risulterebbero completamente scorrelati.

Nelle teorie è utile prevedere un elemento di strutturazione, che chiameremo sezione, che delimiti lo scope delle dichiarazioni di variabili. Nel caso di CIC, alle sezioni della teoria corrisponderanno esplicitamente le sezioni (directory) in cui sono strutturati gli oggetti: per includere nella teoria un riferimento a una definizione D che dipende da una variabile V entrambe appartenenti ad una sezione R, è necessario aprire nel file della teoria la sezione che si riferisce a R tramite URI e mettere i due riferimenti dentro la sezione. Se non si prevedesse un meccanismo del genere, la teoria potrebbe diventare ingannevole, inducendo il lettore a credere, per esempio, che un teorema utilizzi un certo assioma, che è una variabile della sezione, quando in effetti ne utilizza un altro. Per questo motivo, nei documenti matematici si presta sempre attenzione allo scope delle ipotesi formulate.

Questa parte del progetto HELM è attualmente allo stadio embrionale, anche se esistono già come prototipi per le teorie un DTD, un proof-checker, un browser, dei meccanismi di applicazione delle notazioni e uno script in grado di generare una teoria a partire da un file ``.v''. Poiché si prevedono numerosi raffinamenti nel breve periodo, in questa tesi non verrà descritto in dettaglio lo stato attuale delle teorie; ciò nonostante, si farà talvolta loro riferimento nel seguito. Pertanto, un piccolo esempio può servire ora a chiarirne il concetto:

<?xml version="1.0" encoding="ISO-8859-1"?>
<!DOCTYPE Theory SYSTEM "http://localhost:8081/getdtd?url=maththeory.dtd">
<Theory uri="cic:/coq/INIT/Logic">
 <!-- Require Export Datatypes -->
 <DEFINITION uri="True.ind"/>
 <DEFINITION uri="False.ind"/>
 <DEFINITION uri="not.con"/>
 <SECTION uri="Conjunction">
  <DEFINITION uri="and.ind"/>
  <VARIABLE uri="A.var"/>
  <VARIABLE uri="B.var"/>
  <THEOREM id="id1" uri="proj1.con"/>
  <THEOREM id="id2" uri="proj2.con"/>
 </SECTION>
 <SECTION uri="Disjunction">
  <DEFINITION uri="or.ind"/>
 </SECTION>
</Theory>

L'esempio è un frammento di una teoria ottenuta a partire dal file ``.v'' della libreria standard di Coq in cui vengono definiti gli usuali operatori della logica proposizionale. Tutti gli URI, a parte quello di Theory, sono relativi. Quindi, per esempio, l'URI assoluto di id1 è ``cic:/coq/INIT/Logic/Conjunction/id1''. Nell'esempio viene anche mostrato l'uso delle sezioni per limitare lo scope delle variabili: quello di A e B è la sezione Conjunction.

È importante notare che, al livello delle teorie, le sezioni non vengono utilizzate per strutturare il documento in, per esempio, capitoli, paragrafi, etc.: già numerosi linguaggi di markup, istanze di XML, sono stati sviluppati per questo. In accordo allo spirito di XML, il nostro markup potrà essere liberamente e modularmente intervallato ad altri tipi di markup XML, fra cui XHTML⁶. Dunque, il nostro linguaggio può aspirare ad avere per le teorie matematiche lo stesso ruolo di MathML per le espressioni matematiche e SVG⁷ per la grafica vettoriale. Infine, è bene rilevare che il valore aggiunto dall'utilizzo del livello delle teorie rispetto alla semplice replicazione della definizione degli oggetti è non solo quello di arricchirne la semantica, ma anche quello di aggiungere vincoli di natura presentazionale, quali quello sullo scope delle variabili.

3.4 L'implementazione del modulo di esportazione

Una volta individuata tutta l'informazione da esportare, prima di passare all'implementazione bisogna deciderne la fonte. Le due uniche possibilità erano caricare i file ``.vo'' e interpretarne il contenuto, oppure estendere il sistema con un modulo in grado di accedere direttamente alle strutture dati interne. La prima soluzione è sembrata impraticabile, sia perché il formato del file, che cambia ad ogni versione di Coq, non è documentato, sia perché, cosí facendo, non avremmo potuto utilizzare nessuna delle funzioni messe a disposizione dal sistema per astrarne la rappresentazione interna: infatti il Calcolo delle Costruzioni (Co)Induttive è codificato in Coq come un'istanza di un ulteriore metalinguaggio, pensato originariamente per permettere l'estensione del sistema ad altri logical framework. Pertanto, abbiamo optato per la seconda soluzione, utilizzando i meccanismi standard messi a disposizione in Coq per estendere il sistema con opportuni moduli, scritti in OCaml⁸, che hanno accesso alle strutture dati interne. In particolare, si è scelto di scrivere un modulo per aggiungere al vernacolo⁹ i seguenti comandi:

Print XML id.: Visualizza in XML la forma disponibile più cucinata dell'oggetto il cui nome è id.
Print XML File "pathname" id.: Crea il file XML il cui pathname è pathname per la forma disponibile più cucinata dell'oggetto il cui nome è id.
Show XML Proof.: Visualizza in XML la prova parziale del teorema in corso di dimostrazione.
Show XML File "pathname" Proof.: Crea il file XML il cui pathname è pathname per la prova parziale del teorema in corso di dimostrazione.
Print XML Dir id.: Visualizza ricorsivamente in XML la sezione già chiusa il cui nome è id. Gli oggetti vengono stampati nella loro forma non cucinata, correlata con le informazioni per la cottura.
Print XML Dir Disk ``dirname'' id.: Crea ricorsivamente i directory e i file XML per le sezioni e gli oggetti contenuti nella sezione già chiusa il cui nome è id. Gli oggetti vengono stampati nella loro forma non cucinata, correlata con le informazioni per la cottura; il nome del directory che viene creato come radice è dirname.

Nonostante il compito sembrasse semplice, si sono presentati numerosissimi problemi, almeno uno dei quali non risolvibile senza modificare il sistema. Descriviamo brevemente solamente i due problemi che non sono stati risolti all'interno del sistema. Il primo è dovuto al fatto che Coq, dopo il caricamento, non mantiene internamente alcuna informazione sul pathname dei file ``.v''. Pertanto, tutti gli URI generabili sono solamente suffissi degli URI completi: per esempio, in mancanza dell'informazione sul fatto che il file ``Peano.v'' risieda nel directory ``INIT'' della libreria standard di Coq, l'unico URI associabile alla somma fra numeri naturali diventa ``cic:/Peano/plus.con'', mentre l'URI esatto è ``cic:/coq/INIT/Peano/plus.con''. Il secondo problema è dovuto al fatto che Coq mantenga per i diversi tipi di oggetti differenti informazioni per la cottura. Senza scendere nei dettagli, per le costanti l'informazione accessibile è insufficiente, costringendo a rifare il calcolo per determinarla. Questo può essere ovviamente effettuato all'interno di Coq, senza però trarne alcun beneficio; al contrario, in questo modo si è costretti a lavorare con il metalinguaggio. Il primo problema, invece, non può proprio essere risolto senza modificare Coq.

A causa dei precedenti problemi, le procedure di esportazione implementate non generano file XML corretti, in quanto tutti gli URI sono errati e la lista degli ingredienti di alcune costanti, per le quali l'attributo XML paramMode viene settato al valore POSSIBLE, possono contenere variabili spurie, ovvero variabili dalle quali l'oggetto non dipende veramente. Per riparare i file esportati, sono stati sviluppati due strumenti. Il primo è uno script Perl¹⁰ che analizza l'intero albero dei file esportati da Coq e aggiunge a tutti gli URI il prefisso mancante. La possibilità di associare in maniera univoca tale prefisso all'URI è garantita dalla politica di naming di Coq.

Il secondo strumento, scritto in OCaml, implementa una visita di tutti gli oggetti per i quali paramMode = POSSIBLE e di tutti quelli da loro riferiti per determinare quali variabili debbano essere eliminate dall'attributo param in quanto non occorrono nei l-termini da cui l'oggetto dipende.

Sia il modulo di esportazione che i due strumenti aggiuntivi non vengono qui descritti in dettaglio in quanto, entro la fine del 2000, è previsto un periodo in cui l'autore di questa tesi si recherà presso l'INRIA per riscrivere il modulo di esportazione per la nuova versione di Coq, attualmente sotto sviluppo e in fase di implementazione. La stretta collaborazione è mirata principalmente alla risoluzione dei problemi che hanno portato allo sviluppo dei moduli aggiuntivi; inoltre, verranno propagati ad HELM i cambiamenti apportati a Coq, quali la riorganizzazione del meccanismo di gestione delle sezioni e delle variabili.

3.4.1 Risultati ottenuti

Sono state esportate con successo l'intera libreria standard di Coq e una teoria di dimensioni medio-grandi. Per quanto riguarda la libreria standard, l'esportazione ha richiesto circa 4 minuti, mentre le due fasi di riparazione hanno richiesto rispettivamente 3 e 25 minuti. I file creati sono stati 2664, i directory 249; l'occupazione complessiva su disco è di 79 Mbyte, che scendono a soli 4 Mbyte se compressi con il programma gzip, basato sull'algoritmo Lempel-Ziv. Sulle dimensioni incidono notevolmente gli spazi utilizzati per indentare i tag XML: nei teoremi più grandi si trovano fino a 130 livelli di indentazione.

1: Effettivamente, in alcuni casi abbiamo esportato informazione ridondante quando questa era necessaria per la presentazione e computazionalmente molto costosa da ricavare.
2: Con coerenza si intende che l'ordinamento parziale è un sottoinsieme di quello totale.
3: Il grafo delle dipendenze è aciclico: questa proprietà è garantita dalla coerenza del sistema logico, ovvero, in ultima analisi, dalle regole di tipaggio e validità degli ambienti.
4: L'indistinguibilità delle definizioni dai teoremi può, a prima vista, stupire. Non si dimentichi, però, che la principale caratteristica del Calcolo delle Costruzioni, di cui CIC è un'estensione, è proprio l'indistinguibilità dei tipi dai termini, con la conseguente possibilità di ragionare sulle prove, ovvero di scrivere teoremi che abbiano come oggetto dimostrazioni.
5: La differenza fra la base dei due indici ha ragioni storiche: nella letteratura su Coq, infatti, sono usuali formalizzazioni di CIC in cui le definizioni dei tipi (co)induttivi non sono presenti nell'ambiente, ma vengono replicate nel l-termine ad ogni loro occorrenza, similmente a quanto avviene per i blocchi di funzioni definite mutuamente per (co)punto-fisso. In queste presentazioni, la diversa base dei due indici aiuta a contenere le dimensioni delle espressioni poste come pedici nelle formule.
6: http://www.w3.org/TR/xhtml1
7: http://www.w3.org/TR/SVG
8: OCaml è un linguaggio di programmazione fortemente tipato, funzionale, ad oggetti e con la possibilità di utilizzare anche costrutti imperativi; come Coq, è sviluppato all'INRIA. Coq e tutti i moduli che lo estendono sono scritti interamente in OCaml.
9: Il vernacolo è il linguaggio dei comandi di Coq.
10: Perl è sicuramente il linguaggio più adatto per effettuare elaborazioni di file fortemente basate sulla ricerca o sulla sostituzione di parti di testo con altre. In particolare, si noti che l'intero script tratta i file XML come semplici file di testo, sostituendo gli URI incompleti con quelli completi ricavati dall'analisi dell'albero del directory e producendo file XML validi (supposta la validità di quelli dati in input).