Parole chiave: Librerie digitali; Matematica formale; XML; MathML; Proof-assistant

Chapter 1   Introduzione

• Ricerca di tutte le teorie riguardanti l'analisi numerica
• Ricerca di tutti i teoremi di analisi numerica che utilizzano il lemma di Zorn
• Ricerca di tutti i teoremi dei quali una data formula è un'istanza della tesi
• Ricerca di tutti i teoremi direttamente applicabili a partire da un dato insieme di ipotesi

1. Problemi ``tecnologici'' legati alla mancanza di formati orientati al contenuto per la codifica di espressioni matematiche.
2. Problemi ``fondazionali'' e di formalizzazione della matematica (e delle altre scienze esatte)

1.1   L'eXtensible Markup Language

1.2   I Proof-Assistant

1.2.1   La storia del theorem proving

1.2.2   I moderni proof-assistant

1. Eccessiva difficoltà di scrittura delle dimostrazioni
2. Eccessiva difficoltà (se non impossibilità) di comprensione delle dimostrazioni
3. Eccessiva dimensione delle prove
4. Problemi fondazionali
5. Problemi di natura notazionale
6. Problemi tecnologici

Difficoltà di scrittura delle dimostrazioni

Difficoltà o impossibilità di comprensione delle dimostrazioni

Dimensione delle prove

Problemi fondazionali

Problemi notazionali

Problemi tecnologici

1.3   Il progetto HELM

1.3.1   Requisiti di HELM

1. Utilizzo di formati standard. Tutti i documenti che formano la libreria e i metadati su di essi devono essere descritti in XML. Per le elaborazioni sui documenti devono essere utilizzati, quando possibile, standard già definiti (per esempio, XSLT per le trasformazioni fra file XML).
2. Distribuzione e replicazione. La libreria deve essere distribuita e, per motivi di efficienza e fault-tolerance, deve prevedere l'esistenza di più copie di uno stesso documento. Per motivi di rilocabilità e bilanciamento del carico, devono essere utilizzati nomi logici per individuare gli elementi della libreria. Conseguentemente, devono essere definiti e realizzati opportuni meccanismi per la risoluzione dei nomi.
3. Facilità di pubblicazione e accesso. La disponibilità di uno spazio HTTP o FTP deve essere l'unico requisito per poter contribuire alla libreria. In particolare, non si può fare nessuna assunzione sul server utilizzato per la pubblicazione dei documenti, come la possibilità di mandare in esecuzione particolari programmi. Analogamente, per poter consultare la libreria, dovrà essere fornita un'interfaccia Web usufruibile con un comune browser. Interfacce di altro tipo potranno essere fornite per elaborazioni che richiedano una maggiore interattività, come la scrittura di nuovi teoremi.
4. Modularità. Gli strumenti utilizzati per accedere e contribuire alla libreria dovranno essere il più modulari possibile. In particolare, il livello dell'interazione con l'utente deve essere chiaramente separato da quello dell'elaborazione per permettere l'implementazione di diversi tipi di interfacce (interfacce testuali, grafiche e Web).
5. Sfruttamento dell'informazione già codificata. Devono essere implementati strumenti che permettano di esportare verso la libreria HELM l'informazione già codificata nei proof-assistant esistenti. Il progetto non ha scopi fondazionali: non si propone un unico formalismo logico in cui codificare tutta la libreria. Al contrario, i formalismi esistenti non devono essere eliminati o modificati, ma standardizzati descrivendoli in formato XML.

1.3.2   Architettura generale di HELM

1.3.3   Lo sviluppo di HELM

1. Definizione del formato XML per i documenti descritti nel sistema logico di Coq (CIC, Calculus of (Co)Inductive Constructions); progettazione e implementazione del modulo di esportazione da Coq; definizione del modello di distribuzione della libreria e realizzazione dei tool necessari.
2. Progettazione e realizzazione di un CIC proof-checker per i file della libreria.
3. Definizione del meccanismo per l'associazione della notazione ai documenti, tramite l'uso di stylesheet; scrittura di stylesheet per i documenti della libreria; implementazione di interfacce, basate sul proof-checker e su processori XSLT standard, per la consultazione della libreria.
4. Definizione dei metadati associati ai documenti. Implementazione dei meccanismi di indicizzazione e ricerca.
5. Studio sperimentale di metodi per la rappresentazione delle prove.

1.4   Lavori correlati

1. Basi di dati bibliografiche
2. Cataloghi di biblioteche (OPAC)
3. Riviste elettroniche prodotte da editori accademici
4. Server di pre-pubblicazioni e letteratura grigia
5. Indici di risorse matematiche in rete

Studio e progettazione di un modello RDF per biblioteche matematiche elettroniche [Ric99] è uno studio preliminare, risalente al 1999, sulla possibilità di codificare i metadati della libreria di HELM nel formato standard RDF. Nonostante l'architettura di HELM descritta in questo lavoro sia stata pesantemente modificata, la parte di lavoro inerente ai metadati rappresenta un ottimo punto di partenza per le future scelte progettuali.

Content Centric Logical Environments [APSSa] è una breve introduzione ai benefici che HELM porterà nell'ambito dei proof-assistant.

Towards a Library of Formal Mathematics [APSSc] presenta l'intero progetto nell'ottica del precedente articolo.

XML, Stylesheets and the Re-mathematization of Formal Content [APSSd] affronta il problema della rimatematizzazione del contenuto formale.

Formal Mathematics in MathML [APSSb] è una descrizione di HELM dal punto di vista del web-publishing, incentrato sull'utilizzo di MathML.

1.5   Organizzazione della tesi

1

http://www.w3c.org

2

http://www.mizar.org

3

Il progetto Mizar fu iniziato circa venti anni fa. La scarsità di documentazione, unita all'utilizzo di codice proprietario, può far nascere sospetti sulla correttezza dell'intero sistema.

4

In Coq è naturalmente possibile definire la funzione appartenenza che, presi in input un insieme I e un elemento x, ritorna il risultato dell'applicazione di I ad x. Quindi si può arguire che, se si vuole la notazione x Î I, allora si deve utilizzare la funzione appartenenza. Anche se in linea di principio questo è giusto, si avrebbe un consistente aumento della dimensione delle prove. Inoltre, in presenza di isomorfismi, l'utilizzo di simili artifizi è pratica comunemente accettata in matematica.

5

http://www.cs.unibo.it/helm

6

I membri attuali sono: Prof. Andrea Asperti, Dott. Luca Padovani, Sig. Claudio Sacerdoti Coen e Dott. Irene Schena.

7

L'idea del progetto risale alla fine del 1997. L'autore contribuisce attivamente al suo sviluppo dall'estate del 1999, quando è stata definita l'architettura generale ed è iniziata la fase implementativa.

8

XSLT è lo standard per la descrizione di trasformazioni fra documenti XML. Un foglio di stile è un documento XSLT che definisce un insieme di regole di trasformazione.

9

http://www.emis.de/projects/EULER/

10

http://zermelo.dcs.ed.ac.uk/proofgen

11

12

http://www-unix.mcs.anl.gov/qed

13

Una prima conferenza fu tenuta nel 1994 ad Argonne, seguita da una seconda a Varsavia nel 1995.

14

Vedi il primo requisito del paragrafo 1.3.1.

15

http://www.mathweb.org

16

Con Omega viene ancora indicato il sotto-progetto mirato al raggiungimento degli obiettivi originari.

Chapter 2   Il proof-assistant Coq

2.1   Il Calcolo delle Costruzioni (Co)Induttive

2.1.1   La sintassi

• V una famiglia numerabile di nomi di variabili, x,y,z,... Î V.
• C una famiglia numerabile di nomi di costanti, c,c₁,...,c_n Î C.
• I una famiglia numerabile di nomi di tipi (co)induttivi, i,i₁,...,i_n Î I.
• K una famiglia numerabile di nomi di costruttori di tipi (co)induttivi,
  k,k₁,...,k_n,k₁¹,...,k_n1¹,...,k₁^m,..., k_nm^m Î K.

---

t ::= x identificatori   | c costanti   | i tipi (co)induttivi   | k costruttori di tipi (co)induttivi   | Set | Prop | Type(j) sort   | t t applicazione   | l x:t.t l-astrazione   | P x:t.t prodotto dipendente   | <t>CASESi t OF analisi per casi      k1  x Þ t | ... | kn  x Þ t       END     | FIXl {x/n1 : t := t ; ... ; x/nm : t := t} definizione per punto fisso   | COFIXl {x : t := t ; ... ; x : t := t} definizione per co-punto fisso

Table 2.1: Sintassi dei termini di CIC

---

1. tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrano liberi in t,t₁,...,t_h
2. i ¹ x
3. Se i dipende da k parametri e il suo arity è P x₁:T₁... P x_l : T_l.s, allora h = k + l
4. i occorra solo strettamente positivamente in T

• tutti i tipi mutuamente induttivi con i non occorrono in T oppure
• T = P x : T₁.T₂ e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono liberi in T₁ e i occorre solo strettamente positivamente in T₂ oppure
• T = (i' t₁... t_n) e i' è un tipo mutuamente induttivo con i e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono liberi in t₁ ... t_n oppure
• T = (i' t₁ ... t_n) e i', diverso da i, è l'unico tipo mutuamente induttivo del suo blocco, dipendente da m < n parametri, e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono liberi in t_m+1,...,t_n e occorrono solo positivamente in modo debole in tutti i tipi dei costruttori di i'

• C = (i t₁ ... t_n) oppure
• C = T ® C' e i appare solo positivamente in modo debole in C' e i appare solo strettamente positivamente in T dove i' venga sostituito con una variabile x fresca oppure
• C = P x:T.C' e i occorre solo positivamente in modo debole in C' e tutti i tipi mutuamente induttivi con i (compreso i stesso) non occorrono in T dove i' venga sostituito con una variabile x fresca

2.1.2   Le riduzioni e la convertibilità

Contesti e ambienti

b-riduzione, d-riduzione, i-riduzione e unfolding (o espansione)

La convertibilità

2.1.3   Le regole di tipaggio

Regole del Calcolo delle Costruzioni

Regole per i tipi (co)induttivi

• se T = P z : M.N e GD{l,M} e GD{l,N} valgono
• se T = l z : M.N e GD{l,M} e GD{l,N} valgono
• se T = (x_j t₁... t_{nj - 1} t_nj t_{nj + 1}... t_n) se (GD{l,t_h})_h=1,...,n vale eRS{x₁,...,x_m,n₁,...,n_m,x,l,t_j} vale dove j Î {1,...,m}
• se T = (t t₁ ... t_n) dove t {x₁,...,x_m} e (GD{l,t_h})_h=1,...,n vale
• se T è una variabile o una costante o un tipo induttivo o un costruttore di un tipo induttivo o una sort
• se T = FIX_j {y₁/n'₁ : T₁ := f₁ ; ... ; y_d/n'_d : T_d := f_d} e (GD{l,T_h})_h=1,...,d e (GD{l,f_h})_h=1,...,d valgono
• se T = COFIX_j {y₁ : T₁ := f₁ ; ... ; y_d : T_d := f_d} e (GD{l,T_h})_h=1,...,d e (GD{l,f_h})_h=1,...,d valgono
• se T= (

  <U>CASESi t OF

  k1  x1 Þ f1 | ... | kd  xd Þ fd

  END

  ) e vale una delle seguenti tre condizioni mutuamente esclusive:
  • i è un tipo induttivo e t = (z t₁ ... t_r) dove z Î l È {x} e valgono GD{l,U}, GD{l,t} e (GD{l È PR{k_h,x^h},G'_h})_h=1,...,d dove PR{k_h,(x₁,...,x_r)} = {x_j / il j-esimo parametro del costruttore k_h è ricorsivo in uno dei tipi induttivi mutuamente ricorsivi con il suo tipo} e G_h = l y₁:t₁ ... l y_nh:t_nh.G'_h dove n_h è il numero dei parametri del costruttore k_h.
  • i è un tipo coinduttivo e valgono GD{l,U}, GD{l,t} e (GD{l,f_h})_h=1,...,d
  • i è un tipo induttivo, non vale t = (z t₁ ... t_r) dove z Î l È {x} e valgono GD{l,U}, GD{l,t} e (GD{l,f_h})_h=1,...,d

• se T = (z t₁ ... t_n) dove z Î l
• se T = l z : M.N e RS{l,M} e RS{l,N} valgono
• se T = FIX_j {y₁/n'₁ : T₁ := f₁ ; ... ; y_d/n'_d : T_d := f_d} e (RS{l,f_h})_h=1,...,d vale
• se T = COFIX_j {y₁ : T₁ := f₁ ; ... ; y_d : T_d := f_d} e (RS{l,f_h})_h=1,...,d vale
• se T= (

  <U>CASESi t OF

  k1  x1 Þ f1 | ... | kd  xd Þ fd

  END

  ) e vale una delle seguenti tre condizioni mutuamente esclusive:
  • i è un tipo induttivo e t = (z t₁ ... t_r) dove z Î l È {x} e valga (RS{l È PR{k_h,x^h},G'_h})_h=1,...,d dove PR{k_h,(x₁,...,x_r)} = {x_j / il j-esimo parametro del costruttore k_h è ricorsivo in uno dei tipi induttivi mutuamente ricorsivi con il suo tipo} e G_h = l y₁:t₁ ... l y_nh:t_nh.G'_h dove n_h è il numero dei parametri del costruttore k_h.
  • i è un tipo coinduttivo e vale (RS{l,f_h})_h=1,...,d
  • i è un tipo induttivo, non vale t = (z t₁ ... t_r) dove z Î l È {x} e vale (RS{l,f_h})_h=1,...,d

• se T = (z t₁ ... t_n) dove z Î {x₁,...,x_m} e h = 1 e x₁,...,x_m non occorrono libere in t₁,...,t_n
• se T = (k t₁ ... t_n) dove k è il costruttore di un tipo coinduttivo che aspetta n parametri e per ogni j Î {1,...,n} se k è ricorsivo nel j-esimo parametro allora vale GC₁{t_j}, altrimenti x₁,...,x_m non occorrono libere in t_j
• se T = (t t₁ ... t_n) dove t {x₁,...,x_m} e t non è un costruttore di un tipo coinduttivo e x₁,...,x_m non appaiono libere in t,t₁,...,t_n
• se T è una sort o un tipo (co)induttivo o un costruttore di un tipo (co)induttivo
• se T = l z:M.N e x₁,...,x_m non occorrono libere in M e vale GC_h{N}
• se T = FIX_j {y₁/n'₁ : T₁ := f₁ ; ... ; y_d/n'_d : T_d := f_d} e x₁,...,x_m non occorrono libere in f₁,...,f_d,T₁,...,T_d
• se T = COFIX_j {y₁ : T₁ := f₁ ; ... ; y_d : T_d := f_d} e x₁,...,x_m non occorrono libere in f₁,...,f_d,T₁,...,T_d
• se T= (

  <U>CASESi t OF

  k1  x1 Þ f1 | ... | kd  xd Þ fd

  END

  ) e x₁,...,x_m non occorrono libere in U e t e vale una delle due seguenti condizioni mutuamente esclusive:
  • U = l z:M.(i t₁ ... t_r) dove i è un tipo coinduttivo e vale (GC_h{f_l})_{l Î {1,...,d}}
  • U ¹ l z:M.(i t₁ ... t_r) dove i è un tipo coinduttivo e x₁,...,x_m non occorrono libere in f₁,...,f_d

2.2   Il Calcolo delle Costruzioni (Co)Induttive in Coq

2.2.1   Alcune estensioni a CIC

Livelli degli universi impliciti

Cast

Metavariabili

Termini impliciti

2.2.2   Particolarità implementative

2.2.3   Il livello degli oggetti, ovvero la manipolazione degli ambienti

2.2.4   Le sezioni e il meccanismo di cottura

Section S.
 Variable A : Prop.
 Variable B : Prop.

 Theorem AB_A_B : (A -> B) -> A -> B.
 Proof.
  Exact [ab:(A ->B)][a:A](ab a).
 Qed.

 Theorem A_AB_B : A -> (A -> B) -> B.
 Proof.
  Exact [a:A][ab:(A->B)](AB_A_B ab a).
 Qed.
End S.

Theorem AB_A_B : (A:Prop)(B:Prop)(A -> B) -> A -> B.
Proof.
 Exact [A:Prop][B:Prop][ab:(A ->B)][a:A](ab a).
Qed.

Theorem A_AB_B : (A:Prop)(B:Prop)A -> (A -> B) -> B.
Proof.
 Exact [A:Prop][B:Prop][a:A][ab:(A->B)](AB_A_B A B ab a).
Qed.

2.2.5   Nomi e section path

Section S1.
 Axiom A : Prop.
End S1.

Section S2.
 Axiom A : Prop.
End S2.

2.3   Il sistema Coq

2.3.1   Parsing e pretty-printing

• Le regole grammaticali sono fattorizzate sintatticamente: Camlp4 non tenta di espandere i non terminali per individuare ulteriori fattorizzazioni. Pertanto, l'utente deve fattorizzare a mano tutte le regole.
• Quando si aggiunge una nuova regola di parsing, non viene controllato che la grammatica resti LL(1), con conseguenti problemi durante il parsing.
• Le regole vengono rimosse all'uscita delle sezioni, permettendo esclusivamente la definizione di notazioni locali e costringendo, quindi, a definire le varie regole al top-level.
• A parte pochi esempi, la notazione testuale è del tutto insufficiente per la rappresentazione delle espressioni matematiche, normalmente scritte usando consolidate notazioni bidimensionali a cui è bene non rinunciare, pena un considerevole aumento della difficoltà di interpretazione dei termini.

2.3.2   Un esempio d'utilizzo di Coq

Coq < Theorem easy: (n:nat)(n = O \/ (EX m : nat | (plus (S O) m) = n)).
1 subgoal
  
  ============================
   (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n)

easy < Intro.
1 subgoal
  
  n : nat
  ============================
   n=O\/(EX m:nat | (plus (S O) m)=n)

easy < Elim n.
2 subgoals
  
  n : nat
  ============================
   O=O\/(EX m:nat | (plus (S O) m)=O)

subgoal 2 is:
 (n0:nat)
  n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ->(S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

easy < Left.
2 subgoals
  
  n : nat
  ============================
   O=O

subgoal 2 is:
 (n0:nat)
  n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ->(S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

easy < Reflexivity.
1 subgoal
  
  n : nat
  ============================
   (n0:nat)
    n0=O\/(EX m:nat | (plus (S O) m)=n0)
    ->(S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

easy < Intros.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0))

easy < Right.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (EX m:nat | (plus (S O) m)=(S n0))

easy < Simpl.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (EX m:nat | (S m)=(S n0))

easy < Exists n0.
1 subgoal
  
  n : nat
  n0 : nat
  H : n0=O\/(EX m:nat | (plus (S O) m)=n0)
  ============================
   (S n0)=(S n0)

easy < Reflexivity.
Subtree proved!

easy < Qed.

Coq < Print easy.
easy = 
[n:nat]
 (nat_ind [n0:nat]n0=O\/(EX m:nat | (plus (S O) m)=n0)
   (or_introl O=O (EX m:nat | (plus (S O) m)=O) (refl_equal nat O))
   [n0:nat; _:(n0=O\/(EX m:nat | (plus (S O) m)=n0))]
    (or_intror (S n0)=O (EX m:nat | (plus (S O) m)=(S n0))
      (ex_intro nat [m:nat](S m)=(S n0) n0 (refl_equal nat (S n0)))) n)
     : (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n)

Coq < Natural easy.
Theorem : easy.
Statement : (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n).
Proof : 
Consider an element n of nat.
We will prove n=O\/(EX m:nat | (plus (S O) m)=n) by induction on n.
Case 1. (base):
  We have directly O=O.
  With this result we have O=O\/(EX m:nat | (plus (S O) m)=O).
Case 2. (inductive):
  We know an element n0 of nat such that
  n0=O\/(EX m:nat | (plus (S O) m)=n0) (H).
  We will prove (S n0)=O\/(EX m:nat | (plus (S O) m)=(S n0)).
  We have directly (S n0)=(S n0).
  With this result we have
  (EX m:nat | (S m)=(S n0)) which is equivalent to
  (EX m:nat | (plus (S O) m)=(S n0)).
Q.E.D.

Theorem : easy.
Statement : (n:nat)n=O\/(EX m:nat | (plus (S O) m)=n).
Proof : 
Consider an element n of nat.
We will prove n=O\/(EX m:nat | (plus (S O) m)=n) by induction on n.
Case 1. (base):
  We have directly O=O.
Case 2. (inductive, n=(S n0)):
  We will prove (EX m:nat | (plus (S O) m)=(S n0)).
  Since (plus (S O) m)=(S m) we can choose n0 for m,
  yelding the thesis.
Q.E.D.

1

Il teorema di incompletezza di Gödel impedisce la dimostrazione in CIC della sua stessa strong normalization, in quanto dimostrarlo implicherebbe, come semplice corollario, la consistenza di CIC. Infatti, in un sistema strong normalizable, la forma canonica di ogni termine che abita un tipo induttivo ha come testa un costruttore, di cui il tipo induttivo False che rappresenta ^ è privo; ne consegue che False non è abitato, ovvero che il sistema è logicamente consistente.

2

In questo caso non valgono le ipotesi del teorema di incompletezza di Gödel; di conseguenza, è stato possibile dimostrare anche la strong normalization

3

Per il ragionamento è sufficiente la forma normale di testa debole.

4

La chiusura per contesti è quella standard, che asserisce le proprietà di congruenza di =_bdi, e non ha relazioni con i contesti definiti in precedenza.

5

B.Werner in [Wer94] dimostra la normalizzazione forte di una versione più primitiva di CIC anche nel caso in cui si consideri la h-conversione. Il risultato è fortemente basato sugli studi di Geuvers [Geu93]

6

La condizione viene introdotta in [Gim94] dove è semplicemente il controllo che T sia un identificatore appartenente a l. La forma presentata qui, che è inedita a conoscenza dell'autore, è stata ricavata ex-novo (e successivamente implementata) assieme al Dott. Luca Padovani partendo dall'osservazione del comportamento di Coq. Non è stata, però, data alcuna prova di correttezza (ovvero non è stata provata la normalizzazione forte del sistema quando si utilizzi questa definizione). Pertanto, la definizione può essere considerata ``sospetta''.

7

Questa affermazione è falsa nello studio delle teorie che dipendono pesantemente dalla stratificazione degli universi, come la Teoria delle Categorie, in cui si devono distinguere le categorie grandi da quelle piccole, e quella degli insiemi, in cui non vanno confusi gli insiemi grandi e piccoli. In queste teorie, è usuale procedere duplicando sintatticamente le stesse definizioni contenenti Type al solo fine di fare inferire al sistema diversi livelli per gli universi: le definizioni con il livello minore diverranno quelle piccole, le altre le grandi.

8

L'affermazione è falsa se il livello degli universi viene inferito, come avviene in Coq.

9

Le regole di parsing sono quelle che permettono di associare alla notazione testuale utilizzata dall'utente la rappresentazione interna dei l-termini. Le regole di pretty-printing compiono l'operazione inversa.

Chapter 3   Esportazione in XML da Coq di oggetti CIC

• 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.

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

1. 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.
2. È 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.

3.2   Il DTD per il livello dei termini e degli oggetti

1. 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.
2. 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.
3. 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.
4. Utilizzo degli URI per riferirsi ad altri oggetti
5. 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.

• 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 è

  n1: v11 ... v

  m1   1

  n2: v21 ... v

  m2   2

  ... nh: vh1 ... v

  mh   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<sub>m</sub><sup>n<sub>m</sub></sup> e ``.var''; per le successive si ripete la stessa operazione scegliendo, nell'ordine, v_m^{n_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⁵.

3.3   Il livello delle teorie

<?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>

3.4   L'implementazione del modulo di esportazione

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.

3.4.1   Risultati ottenuti

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).

Chapter 4   Il modello di distribuzione

1. Scarsa efficienza e fault-tolerance Un URL identifica il server su cui risiede l'unica copia del documento. Pertanto, tralasciando la possibile esistenza di proxy o cache, il server rappresenta un collo di bottiglia per le prestazioni e un single point of failure¹.
2. Mancata rilocabilità dei documenti Modificare la posizione fisica di un documento, per esempio spostandolo su un altro server, cambia il suo URL, con conseguenti problemi di collegamenti interrotti (broken link). Questi sono inaccettabili, in particolar modo in una libreria di documenti matematici formali, in quanto di un oggetto si può fare il type-checking esclusivamente se sono accessibili tutti i documenti dai quali esso dipende.
3. Impossibilità per l'editore di un documento di cancellarlo È un problema strettamente legato al precedente, ma distinto. Può accadere che qualcuno pubblichi un documento che, a distanza di tempo, non ritenga più utile. Pertanto, deve essere libero di cancellarlo (qualsiasi affermazione contraria sarebbe, a dir poco, utopistica). Questa operazione, però, invalida tutti i documenti che da quello dipendono.

4.1   Il getter

1. Un modo per l'utente di specificare un insieme di server da contattare e un insieme di regole da utilizzare per generare un ordinamento parziale, dipendente dal singolo documento, fra i server che lo forniscono.
2. Una funzione di update, da eseguirsi in modo batch, per costruire un cache che associ ad ogni URI un URL, basandosi sui due insiemi dati in precedenza.
3. Una funzione, chiamata get, che, dato un URI, restituisca il documento associato.

1. Metodi intelligenti di scaricamento basati sulla località dei riferimenti. Per esempio, il getter potrebbe autonomamente effettuare il download di tutti i documenti riferiti dal documento scaricato e successivamente richiesti con alta probabilità.
2. Scaricamento di file compressi. Se il server che fornisce il documento lo fornisce, staticamente o su richiesta, anche o solamente in modalità compressa, il getter diventa responsabile non solo dello scaricamento, ma anche della successiva decompressione.
3. Scaricamento di più file contemporaneamente. Al getter potrebbe venire richiesto di effettuare il download di un insieme di file. La funzionalità diventa particolarmente interessante se combinata con le precedenti.
4. Ricostruzione ``al volo'' di documenti. Il getter potrebbe saper gestire URI che identificano documenti che debbono essere creati assemblando opportunamente informazioni ricavate da fonti distinte, per esempio effettuando la fusione di documenti residenti su diversi server o ottenuti contattando database remoti.

4.1.1   Il getter con interfaccia OCaml

Progettazione

1. Ogni server, di tipo HTTP o FTP, mantiene i file della libreria di HELM strutturati secondo la gerarchia descritta nel precedente capitolo. Come conseguenza, alla radice della gerarchia resta associato un URL. Inoltre, un server può mantenere più gerarchie distinte identificandole con URL distinti.
2. Ogni server fornisce, nel directory base della gerarchia, un file contenente la lista degli URI di tutti gli oggetti esportati. Il formato del file può essere ragionevolmente sia testuale (un URI per linea), sia XML. Poiché la lista non deve subire elaborazioni particolari, a causa della banalità del parsing del formato testuale e per motivi di efficienza (le liste conterranno mediamente diverse migliaia di elementi), si è scelto di utilizzare il formato testuale, che richiede meno spazio su disco e tempi di parsing molto minori.
3. Ogni client mantiene un file di configurazione per ogni utente, con possibilità di condivisione del file, in cui viene elencata una lista ordinata di URL di gerarchie. Gli URL sono ordinati secondo l'ordine di preferenza crescente dell'utente per i vari server. Questa scelta corrisponde alla politica più semplice che soddisfa il primo requisito obbligatorio: l'ordinamento fra i server è totale e indipendente dall'URI particolare. Anche in questo caso il formato del file può essere ragionevolmente sia testuale che XML. Il numero degli elementi della lista, però, sarà sempre ragionevolmente basso e saranno sicuramente implementati in futuro vari tipi di elaborazioni sul file, quali modifiche, confronti, fusioni e riordinamenti. Pertanto, la scelta cade ragionevolmente sul formato XML, anche se, per il momento, l'implementazione utilizza un semplice file testuale³.
4. Ogni client mantiene, per ogni file di configurazione, un semplice database con una sola tabella in cui ad ogni URI viene associato l'URL ottimale, scelto in accordo con l'ordinamento del file. L'unica query possibile sul database è la richiesta di quale URL è associato ad un determinato URI. La struttura del database e la forma della query suggeriscono fortemente l'adozione come database di un file Berkeley DB, che a sua volta è usualmente implementato come un BTree e che è uno standard consolidato in ambiente Unix, ma di cui esistono implementazioni anche sotto altri sistemi operativi (es. Microsoft).
5. Vengono forniti tre moduli OCaml, il cui grafo delle dipendenze è mostrato in figura 4.1

   ---

   

   ---

   Figura 4.1: Grafo delle dipendenze per i moduli dell'implementazione del getter come modulo OCaml
    
   Il primo modulo, chiamato UriManager, fornisce il tipo di dato astratto uri, la funzione eq per determinare l'uguaglianza fra uri e due funzioni di conversione fra il tipo di dato astratto e la sintassi concreta, chiamate string_of_uri e uri_of_string. La signature del modulo è la seguente:

   type uri
   val eq : uri -> uri -> bool
   val uri_of_string : string -> uri
   val string_of_uri : uri -> string
    

   Il secondo modulo, chiamato Configuration, ha la seguente signature:

   val tmpdir : string
   val indexname : string
   val servers_file : string
   val uris_dbm : string
   val dest : string
    

   dove servers_file è il path assoluto del file descritto al punto 3, uris_dbm quello del file Berkeley DB descritto al punto 4, indexname il nome del file descritto al punto 2, dest il path del cache e tmpdir il path del directory da utilizzare per la creazione di file temporanei. Il modulo deve essere implementato in modo da leggere i parametri da un file XML specificato in qualche modo dall'utente.
   
   Il terzo modulo, chiamato Getter e dipendente dai precedenti, fornisce esclusivamente l'implementazione dei due metodi update e get, basata sulle decisioni prese nei precedenti punti. La signature del modulo è la seguente:

   (* get : uri -> filename *)
   val get : UriManager.uri -> string
   
   (* synchronize with the servers *)
   val update : unit -> unit
    

   Il metodo update si occupa di rigenerare il database contattando tutti i server elencati nel file di configurazione. Il metodo get cerca in cache il file il cui URI viene dato come parametro. Se non lo trova, lo scarica utilizzando l'URL a cui l'URI è associato nel database e ne mette una copia in cache. In entrambi i casi ritorna il path assoluto del file in cache.

Implementazione

update

Vengono scaricati, utilizzando wget, gli indici dei file esportati di tutti i server specificati dall'utente e letti dall'apposito file. A questo punto si svuota il database e, partendo dall'ultimo indice scaricato e procedendo a ritroso, si inseriscono nel database tutte le coppie URI---URL per le quali non è già stata inserita una coppia con lo stesso URI.

get

A partire dall'URI dato in input, si ricava il pathname del file in cache che sarà il valore ritornato. Se il file è già lí  presente, la funzione termina; altrimenti, si ricava dal database l'URL da contattare e si usa wget per scaricare il file.

4.1.2   Il getter con interfaccia HTTP

Progettazione

1. Il file di configurazione, quello in cui vengono elencati i siti da contattare, il database e il cache su disco sono condivisi con il primo prototipo.
2. Il prototipo si comporta come un server HTTP, mettendosi in ascolto su una porta specificata dall'utente e rispondendo alle richieste i cui percorsi (ovvero la parte dell'URL che segue quella che identifica l'host) sono istanze dei seguenti schemi:
   • /get?url=uri Utilizzato per chiedere una copia del documento il cui URI è uri.
   • /annotation?url=uri Descritto nel capitolo 6
   • /getdtd?url=nome Utilizzato per ottenere una copia del DTD il cui nome è nome⁹.
   • /conf Utilizzato per sintetizzare un documento XML contenente alcuni dei parametri di configurazione del getter.
   Per esempio, per richiedere la definizione del tipo induttivo dei numeri naturali al getter che gira sulla porta 8081 dell'host phd.cs.unibo.it, si utilizza il seguente URL:
   ``http://phd.cs.unibo.it:8081/get?uri=cic:/coq/INIT/Datatypes/nat.ind''
3. Il getter è implementato ricorrendo a due moduli Perl, dei quali uno è responsabile esclusivamente della gestione dei parametri di configurazione.

Implementazione

• HTTP::Daemon che implementa un semplice server HTTP che è facilmente personalizzabile scrivendo il codice che viene richiamato ogni volta che viene effettuata una chiamata al server. La libreria, inoltre, facilita la manipolazione di tutti i parametri, sia in entrata che in uscita, della richiesta HTTP.
• LWP:UserAgent che implementa un client HTTP, gestendo tutti i dettagli della connessione.
• DB_File che è una libreria per la gestione di vari tipi di database implementati come file, fra cui quelli Berkeley DB.
• XML::Parser che implementa un semplice parser XML fornendo un'interfaccia ad eventi simile a SAX¹⁰.

• se la richiesta è di tipo conf, restituisce un documento XML creato al volo in cui vengono indicati alcuni dei propri parametri di configurazione.
• se la richiesta è di tipo getdtd, carica il DTD richiesto da disco e lo restituisce.
• se la richiesta è di tipo get, effettua le stesse operazioni eseguite dal metodo get del modulo Getter del primo prototipo; invece di restituire il nome del file, però, restituisce il contenuto del file scaricato o, se questo era già presente in cache, il contenuto della copia in cache.

1

L'affermazione deve essere mitigata. Nel caso in cui il server sia a sua volta un sistema distribuito con bilanciamento del carico e replicazione in spazio, i problemi citati non si presentano. Attualmente, però, la maggior parte degli utenti ha accesso esclusivamente a sistemi non fault-tolerant costituiti da un singolo host, per cui vale l'affermazione.

2

http://www.debian.org

3

Il passaggio al formato XML dovrebbe avvenire a breve.

4

Per una implementazione nient'affatto banale data durante lo sviluppo del proof-checker, si veda il paragrafo 5.1.1.

5

http://www.ocaml-programming.de/packages/documentation/pxp

6

Nel solo parsing di tutti i file XML che compongono la libreria standard di Coq, Markup è risultato circa 5 volte più veloce del parser validante per SGML scritto in C da J. Clark e chiamato SP (SGML Parser) e ha avuto approssimativamente le stesse prestazioni di expat che è un parser XML non validante scritto in C sempre da J. Clark.

7

wget è un utility free, sviluppato dal consorzio GNU, per il download non interattivo di singole pagine o di interi siti. Può utilizzare indistintamente i protocolli HTTP o FTP.

8

Il server potrebbe efficientemente restituire al client la locazione su disco del documento, in conformità al protocollo HTTP. Questa opzione non è , però, possibile, in quanto il prototipo, come descritto nel capitolo 6, effettua anche sintesi al volo di file ottenuti a partire da più di un documento alla volta.

9

I DTD in HELM non vengono identificati da un URI, ma semplicemente dal loro nome.

10

SAX è un'interfaccia ad eventi per i parser XML che è diventata uno standard di fatto in ambiente Java.

11

Le operazioni compiute se la richiesta è di tipo annotation verranno descritte nel capitolo 6.

Chapter 5   Un proof-checker per i file CIC della libreria

1. La scrittura del proof-checker ha permesso di determinare se tutta l'informazione degli oggetti CIC è stata esportata.
2. Il proof-checker rappresenta la dimostrazione concreta della possibilità di reimplementare tutte le funzionalità dei moderni proof-assistant monolitici in maniera modulare, basandosi sul formato XML. In particolare, l'architettura e l'implementazione risultanti sono estremamente più semplici ed eleganti di quelle del proof-checker integrato in Coq. Inoltre, nonostante il codice non sia stato particolarmente ottimizzato e gli algoritmi adottati siano fra i più semplici noti, le prestazioni del proof-checker sono comparabili a quelle di Coq, se si escludono le rispettive fasi di parsing.
3. A partire da una implementazione completa e funzionante del proof-checker, diventa possibile sperimentare modifiche al sistema logico, per esempio per affrontare il problema delle dimensioni delle prove.
4. Alcune sottigliezze del sistema logico possono essere comprese solamente durante la progettazione e l'implementazione di un proof-checker, che assumono, quindi, importanti valenze didattiche.

5.1   Progettazione

5.1.1   UriManager

type uri
val eq : uri -> uri -> bool
val uri_of_string : string -> uri
val string_of_uri : uri -> string  (* complete uri *)
val name_of_uri   : uri -> string  (* name only (without extension)*)
val buri_of_uri   : uri -> string  (* base uri only *)
val depth_of_uri  : uri -> int     (* length of the path *)

(* relative_depth curi uri cookingsno                            *)
(* is the number of times to cook uri to use it when the current *)
(* uri is curi cooked cookingsno times                           *)
val relative_depth : uri -> uri -> int -> int

Raffinamento della specifica

1. Due URI identici devono condividere la stessa rappresentazione. In altre parole, la uri_of_string, se richiamata due volte su stringhe uguali, deve restituire in entrambi i casi la stessa (in senso fisico) struttura dati.
2. Le funzioni eq, string_of_uri, name_of_uri, buri_of_uri e depth_of_uri devono appartenere a O(1).
3. La funzione relative_depth deve appartenere a O(depth_of_uri(u)) dove u è l'URI dato in input.

1. La complessità computazionale media della depth_of_uri su un URI già incontrato deve essere al più O(log(n)) dove n è il numero di URI già incontrati.

5.1.2   Cic

1. Lo zucchero sintattico è scomparso, riavvicinandosi alla rappresentazione data nella descrizione della teoria. In particolare, i binder, che nella rappresentazione XML erano stati spostati sull'elemento target, sono tornati ad essere attributi di Lambda o Prod.
2. Tutti gli URI, che in XML erano in parte assoluti e in parte relativi, hanno la stessa rappresentazione interna, determinata dal modulo UriManager.
3. Tutti gli URI che si riferiscono ad oggetti cucinabili hanno sempre associato un indice, indicato in commento con cookingsno, che indica il livello di cottura voluto per l'oggetto. Questo deve essere calcolato durante il parsing e modificato ad ogni cottura dell'oggetto. Il motivo che ci ha spinto ad esplicitare l'indice, che poteva comunque essere calcolato al volo all'occorrenza, è dovuto alla complessità computazione dell'operazione, che, pur non essendo troppo elevata (vedi paragrafo 5.1.1), diventava influente per l'alto numero di applicazioni della funzione relative_depth che sarebbero state richieste.
4. La rappresentazione interna degli ingredienti di un oggetto è una buona sintesi, in termini di efficienza, fra quella dei file XML e quella come lista di coppie. In pratica, è una lista di liste di URI avente un elemento per ogni token numerico presente nel file XML, ovvero per ogni livello di cottura; la lista elemento contiene tutti gli URI degli ingredienti per quel livello.
5. La rappresentazione OCaml dei costruttori prevede un ulteriore parametro, assente sia nella teoria che nel DTD XML, che è un reference ad una lista di booleani, possibilmente non specificata: durante il parsing, la lista non viene specificata; durante il proof-checker del tipo induttivo del costruttore, vengono individuati i parametri in cui il costruttore è ricorsivo, nel senso del paragrafo 2.10, e l'informazione viene memorizzata nella lista di booleani per essere poi utilizzata più volte durante le verifiche delle condizioni GC e GD, con conseguente incremento delle prestazioni.

5.1.3   CicParser

val term_of_xml : string -> UriManager.uri -> Cic.obj

5.1.4   CicCache

1. Il grafo diretto delle dipendenze fra gli oggetti di CIC è aciclico⁶.
2. Anche se la riduzione è definita per termini qualsiasi, ai fini del proof-checking può essere sempre richiamata esclusivamente su termini che abbiano già superato il type-checking.

exception CircularDependency of string;;

(* get_obj uri                                                   *)
(* returns the uncooked form of the cic object whose URI is uri. *)
(* If the term is not just in cache, then it is parsed via       *)
(* CicParser.term_of_xml from the file whose name is the result  *)
(* of Getter.get uri                                             *)
val get_obj : UriManager.uri -> Cic.obj

type type_checked_obj =
   CheckedObj of Cic.obj    (* cooked obj *)
 | UncheckedObj of Cic.obj  (* uncooked obj *)

(* is_type_checked uri cookingsno                               *)
(* returns (CheckedObj object) if the object has been           *)
(* type-checked otherwise it returns (UncheckedObj oject) and   *)
(* freeze the object for the type-checking                      *)
(* set_type_checking_info must be called to unfreeze the object *)
val is_type_checked : UriManager.uri -> int -> type_checked_obj

(* set_type_checking_info uri                                   *)
(* must be called once the type-checking of uri is finished     *)
(* The object whose URI is uri is unfreezed and cooked at every *)
(* possible level using the !cook_obj function                  *)
(* Therefore, is_type_checked will return a CheckedObj          *)
val set_type_checking_info : UriManager.uri -> unit

(* get_cooked_obj uri cookingsno *)
(* returns the object whose URI is uri cooked cookingsno levels *)
val get_cooked_obj : UriManager.uri -> int -> Cic.obj

val cook_obj :
 (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) ref

5.1.5   CicCooking

val cook_obj : Cic.obj -> UriManager.uri -> (int * Cic.obj) list

5.1.6   CicSubstitution, CicReduction e CicTypeChecker

CicSubstitution:

val lift : int -> Cic.term -> Cic.term
(* subst t1 t2  substitutes t1 for the first free variable in t2 *)
val subst : Cic.term -> Cic.term -> Cic.term

CicReduction:

val whd : Cic.term -> Cic.term
val are_convertible : Cic.term -> Cic.term -> bool

CicTypeChecker:

exception NotWellTyped of string
val typecheck : UriManager.uri -> unit

5.2   Implementazione

5.2.1   UriManager

5.2.2   CicParser

5.2.3   CicCache

5.2.4   CicCooking

5.2.5   CicSubstitution, CicReduction

5.2.6   CicTypeChecker

5.2.7   Risultati ottenuti

1

Come conseguenza immediata della regola Ax-Acc si ha Type:Type; in presenza di questa regola è ben nota (vedi [Coq86]) l'inconsistenza del sistema logico, nel quale è possibile codificare un paradosso analogo a quello di Russel.

2

Durante lo sviluppo non è stato in effetti possibile riusare nessuna parte del codice di Coq, principalmente a causa della rappresentazione interna di questo basata sulla codifica di CIC come istanza di un metalinguaggio.

3

Affinché B registri funzioni presso A è necessario che B dipenda staticamente da A.

4

Oltre a quella, già citata, sull'assenza della gestione dei livelli degli universi, che sono espliciti nella sintassi di CIC, impliciti nella rappresentazione XML, ma ancora assenti nella rappresentazione OCaml.

5

Una possibile rappresentazione dell'albero è il DOM, ovvero un API standard definito dal W3C. La natura tipicamente imperativa di questo, però, si armonizza male in un linguaggio con feature imperative, ma spirito funzionale quale OCaml. Pertanto, nessun parser XML per questo linguaggio lo implementa, preferendogli un'API proprietario dalle caratteristiche similari.

6

Almeno nel caso delle costanti, è facile convincersi dell'aciclicità: se questa venisse violata, esisterebbe una catena infinita di d-espansioni; conseguentemente, il sistema non sarebbe fortemente normalizzabile e, pertanto, nemmeno consistente. Nel caso dei tipi mutuamente (co)induttivi, invece, l'argomento è più complesso, ma semplicemente a causa della particolare formulazione di CIC proposta.

7

Esistono due posizioni filosofiche sul ruolo della riduzione nelle dimostrazioni formali. La prima cerca di evitarla il più possibile, in quanto essa nasconde le motivazioni della correttezza delle prove, che vengono basate esclusivamente sulla correttezza delle regole di riduzione, ovvero sulla metateoria. La seconda la accetta sostenendo che, una volta che ci si fidi della metateoria, le prove per riduzione non debbono essere più comprese. Un esempio può chiarire il punto: si voglia provare il teorema 2 + 3 = 3 + 2; una prima prova risulta immediata utilizzando la proprietà commutativa dell'addizione; un metodo alternativo è giustificare l'uguaglianza poiché entrambi i termini riducono a 5 e la riduzione preserva l'uguaglianza di Leibniz: in questo caso, quindi, la prova è immediata per la proprietà riflessiva dell'uguaglianza di Leibniz.

8

È in questo momento che viene utilizzata la regola Conv.

9

Non bisogna dimenticare che il tempo richiesto dal parsing di Coq è estremamente basso in quanto il formato dei file ``.vo'' è binario.

Chapter 6   La presentazione delle prove

• Problemi notazionali per le espressioni (tipi): è necessario effettuare una ``rimatematizzazione'' delle espressioni formali, associando agli operatori matematici la loro usuale notazione bidimensionale ed astraendo dalla particolare definizione degli operatori nel sistema logico, mantenendo però riferimenti precisi ai termini formali.
• Problemi di comprensibilità per le prove (termini): è necessario associare ai termini che rappresentano prove nel sistema logico una loro descrizione in linguaggio naturale, con l'auspicabile possibilità di poter aumentare o diminuire il livello di dettaglio della prova, fino a giungere al l-termine sottostante (livello di dettaglio massimo).

6.1   L'architettura generale delle trasformazioni presentazionali

6.2   Gli stylesheet notazionali

1. Uno o più stylesheet dal formato CIC a quello MathML content che descrivano le trasformazioni di default; ad ogni elemento specificato dal DTD deve essere associata una trasformazione.
2. Un meccanismo che permetta agli utenti di scrivere nuovi stylesheet dal formato CIC a quello MathML content che descrivano le trasformazioni particolari associate alle varie notazioni. Durante l'applicazione degli stylesheet, se nessuna notazione particolare è applicabile ad un elemento, allora deve essere utilizzata la trasformazione di default. È necessario fornire un'opportuna politica per la risoluzione di eventuali conflitti, ovvero i casi in cui ad un elemento venga associata più di una notazione.
3. Uno stylesheet per ogni formato di output che descriva la trasformazione dal formato intermedio a quello voluto. Tale trasformazione non è affatto banale, in quanto è responsabile del layout del documento generato. In altre parole, è in questa fase che è necessario decidere l'indentazione del documento, basandosi sulle dimensioni della pagina e sulla semantica delle formule.

<apply>
 <gt/>
 <ci>n</ci>
 <ci>0</ci>
</apply>

<xsl:template match="APPLY" mode="noannot">
    <m:apply helm:xref="{@id}">
    <m:csymbol>app</m:csymbol>
     <xsl:apply-templates mode="noannot" select="*"/>
    </m:apply>
</xsl:template>

<xsl:template match="
  APPLY[
   CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
   and (count(child::*) = 2)
   and APPLY[CONST[
    attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con'
   ]]
  ]" mode="noannot">
    <xsl:variable name="no_params">
     <xsl:call-template name="get_no_params">
      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
      <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
     </xsl:call-template>
    </xsl:variable>
    <xsl:choose>
     <xsl:when test=
       "(count(APPLY/child::*) - number($no_params)) = 3">
      <m:apply helm:xref="{@id}">
       <m:notin/>
       <xsl:apply-templates select="*[2]/*[3+$no_params]"
        mode="noannot"/>
       <xsl:apply-templates select="*[2]/*[2+$no_params]"
        mode="set"/>
      </m:apply>
     </xsl:when>
     <xsl:otherwise>
      <xsl:apply-imports/>
     </xsl:otherwise>
    </xsl:choose>
</xsl:template>

6.3   Alcune idee per la resa delle prove

6.3.1   Le annotazioni

1. Se il nodo corrente è privo di annotazione, richiama la regola opportuna dello stylesheet per i termini non annotati, ovvero quello per la resa del l-termine.
2. Altrimenti itera su ogni elemento dell'annotazione in questo modo:
   1. Se incontri un elemento del markup di output, ricopialo.
   2. Se incontri un riferimento ad un attributo del nodo corrente, stampa il valore dell'attributo.
   3. Se incontri l'elemento che indica la descrizione formale del nodo corrente, richiama la regola opportuna dello stylesheet per i termini non annotati.
   4. Se incontri un riferimento ad un altro nodo, processa con la regola più esterna il nodo puntato.

Applicazione più esterna:

``<<riferimento all'applicazione più interna>> Da qui, per la proprietà transitiva <<riferimento al primo figlio della funzione>> e l'ipotesi <<riferimento al terzo figlio della funzione>>, si ha la tesi.''

Applicazione più interna:

``Per la proprietà transitiva <<riferimento al primo figlio della funzione>> applicata alle ipotesi <<riferimento al secondo figlio della funzione>> e <<riferimento al terzo figlio della funzione>> si ha X>Y.

1. Non vi è alcuna garanzia che l'annotazione di un nodo corrisponda alla descrizione informale e corretta del nodo stesso.
2. Poiché annotare un termine è tanto difficile quanto capire la prova formale, annotare termini di grosse dimensioni è impraticabile.

6.3.2   La generazione automatica delle annotazioni.

6.4   Risultati ottenuti.

1

Si vedano rispettivamente il modulo Natural di Coq [CKT95] e quello Proverb di Omega [Hor99].

2

L'operazione non è semplice come può sembrare a prima vista in quanto esistono tattiche che compiono trasformazioni complesse sul l-termine. Inoltre, l'implementazione più semplice di una tattica non si preoccupa mai della verifica che il termine generato sia il più naturale possibile, prediligendo la facilità implementativa, ma generando termini ingiustificatamente complessi, che vengono talvolta successivamente semplificati, per esempio procedendo all'eliminazione di alcuni dei tagli introdotti.

3

Le osservazioni derivano in larga parte dallo studio del Prof. Asperti che, nell'ambito del progetto HELM, sta realizzando un primo prototipo di generatore automatico.

4

Lo standard XSLT 1.0 prevede l'implementazione di funzioni di estensione, ma non specifica alcuno standard per l'interfacciamento di tali funzioni con il processore XSLT. Lo standard XSLT 1.1 affronterà il problema, ma non sarà disponibile che fra diversi mesi. Ciò nonostante, esiste già ora un modo non ufficiale, ma funzionante con ogni processore, per ottenere un risultato analogo: la scrittura della funzione come metodo di un HTTP server o come CGI. Il getter descritto nel paragrafo 4.1.2 utilizza esattamente tale stratagemma.

5

Nella particolare formulazione proposta.

6

Più dettagliatamente, le variabili possono memorizzare result tree fragment (rtf), ovvero alberi XML come quelli restituiti dall'applicazione dell'istruzione ``value-of'' ad un XPath contenente l'invocazione della funzione ``document''; quello che non si può fare è applicare funzioni XPath agli rtf, impedendo quindi la selezione di nodi dell'albero memorizzato nell'rtf. Nella prossima versione dello standard quest'ultima limitazione verrà semplicemente eliminata; attualmente, comunque, tutti i processori XSLT implementano come estensione proprietaria una funzione che trasforma un rtf in un node set, sul quale è possibile applicare funzioni XPath. Per poter scrivere lo stylesheet per la sintesi automatica, più dettagliatamente per poter implementare la funzione di sostituzione, è stato necessario ricorrere ad una di tali estensioni.

Chapter 7   Le interfacce utente

7.1   I siti di presentazione

• l'URI dell'annotazione o del file a livello del sistema logico;
• una lista di URI di stylesheet che complessivamente descrivano la trasformazione dal livello del sistema logico a quello content;
• una lista di URI di stylesheet che complessivamente descrivano la trasformazione dal livello content a quello presentation.

7.1.1   Risultati ottenuti

1. La mancanza di browser in grado di riconoscere il formato MathML
2. Gli elevati tempi di elaborazione

7.2   L'interfaccia sviluppata in Gtk

1. Visualizzazione di un menu ad albero in cui sono riportati tutti gli oggetti e le teorie a conoscenza del getter.
2. Visualizzazione degli oggetti o delle teorie in formato MathML presentation, ottenuto applicando agli oggetti le trasformazioni descritte nel precedente capitolo³.
3. Possibilità di invocare il proof-checker sull'oggetto o la teoria attualmente visualizzati.
4. Navigazione ipertestuale ottenuta tramite hyperlink che associano alle occorrenze dei nomi degli oggetti le loro definizioni⁴.
5. Possibilità di selezionare esclusivamente le espressioni che corrispondono alla presentazione di un nodo CIC annotabile.
6. Possibilità di (ri)annotare il nodo selezionato scrivendo manualmente il markup che costituisce l'annotazione. Per l'introduzione degli elementi di ricorsione e di quelli che selezionano gli attributi del nodo corrente, l'interfaccia propone anche una palette dei suggerimenti: ogni pulsante della palette, quando premuto, inserisce nella posizione corrente dell'annotazione il markup corrispondente al suggerimento.

7.2.1   Progettazione

Prima fase

1. L'interfaccia deve basarsi sull'emergente standard Gtk per sfruttarne le caratteristiche di portabilità. La libreria Gtk, infatti, è oggi disponibile per diverse architetture e sotto diversi sistemi operativi; inoltre, esistono binding per Gtk per tutti i linguaggi di programmazione più diffusi, compreso OCaml.
2. Deve essere possibile con poco sforzo implementativo utilizzare un qualunque processore XSLT scritto in un qualunque linguaggio. L'obiettivo è quello di massimizzare la modularità ed è reso particolarmente significativo dalle scarse prestazioni degli attuali processori: deve essere possibile utilizzare in ogni momento quello dalle prestazioni migliori.
3. Il linguaggio utilizzato nell'implementazione è OCaml. La scelta di utilizzare nuovamente OCaml semplifica l'integrazione nell'interfaccia del proof-checker. Inoltre, mentre le caratteristiche funzionali del linguaggio sono meno significative nell'ambito dello sviluppo di interfacce grafiche, il sofisticato sistema di type-inference unito alle feature object-oriented permettono di raggiungere elevati livelli di produttività e di correttezza e pulizia del codice.

• MmlInterface è il modulo radice, la cui interfaccia è vuota, che si occupa della gestione dei widget e delle finestre che compongono l'interfaccia grafica, invocando i (meta)moduli ProofChecker e XsltProcessor per le elaborazioni.
• GtkMathView è il binding per OCaml del widget MathView, la cui interfaccia è⁵

  exception ErrorLoadingFile of string
  class math_view_signals :
    ([> `container | `widget | `math_view] as 'b) Gtk.obj ->
    object ('a)
      method jump :
        callback:(string -> unit) -> GtkSignal.id
    end
  class math_view :
    Gtk_mathview.math_view Gtk.obj ->
    object
      method coerce : GObj.widget
      method connect : math_view_signals
      method get_selection : string option
      method load : filename:string -> unit
    end
  val math_view :
    ?adjustmenth:GData.adjustment ->
    ?adjustmentv:GData.adjustment ->
    ?border_width:int ->
    ?width:int ->
    ?height:int ->
    ?packing:(GObj.widget -> unit) ->
    ?show:bool -> unit -> math_view
   

• ProofChecker è il metamodulo logico comprendente tutti i moduli che compongono il proof-checker descritto nel capitolo 5.
• XsltProcessor è il modulo che fornisce il binding per i processori XSLT e la cui interfaccia è:

    (* (process filename usecache mode) calls the XSLT      *)
    (* processor on the XML file whose name is filename.    *)
    (* mode could be either "theory" or "cic"               *)
    (* If usecache is true and the result of the processing *)
    (* is already in cache, then it is reused without       *)
    (* calling again the real XSLT processor.               *)
    process : string * bool * string -> string
   

Seconda fase

1. Fornire una rappresentazione interna dei termini annotati e un cache per essi.
2. Fornire un parser per i file di annotazioni.
3. Fornire una funzione di salvataggio che, data la rappresentazione interna dei termini annotati, crei il file XML contenente le annotazioni.
4. Fornire un modulo che, data la rappresentazione interna di un termine annotato e dato un XPointer, ritorni il nodo selezionato dall'XPointer.
5. Fornire un modulo che, data la rappresentazione interna di un termine e il riferimento ad uno dei nodi, ritorni la lista dei suggerimenti da utilizzare per annotare tale nodo.

• Per quanto riguarda i punti 1 e 2, al modulo Cic già sviluppato per il proof-checker è stata aggiunta la nuova rappresentazione interna e sono stati modificati per utilizzarla sia il metamodulo CicParser che il modulo CicCache.
• Per implementare le funzioni dei punti 3 e 4 sono stati creati due nuovi moduli, chiamati rispettivamente Cic2Xml e CicXPath, che espongono ognuno una sola funzione e le cui interfacce sono ovvie. Il modulo CicXPath riconosce esclusivamente il sottoinsieme banale di XPath effettivamente utilizzato in HELM.
• Per implementare il punto 5 è stato creato un ulteriore modulo che espone una sola funzione che restituisce come suggerimenti una lista ordinata di stringhe di markup XML da associare ai pulsanti della palette.

7.2.2   Risultati ottenuti

1. Ristrutturare gli stylesheet in modo che sia possibile applicarli ad un sotto-termine.
2. Dotare il widget di un'interfaccia DOM o equivalente che permetta la modifica di una sotto-espressione.
3. Riprogettare il prototipo in modo da utilizzare i precedenti meccanismi.

1

http://xml.apache.org

2

Xalan-C è il porting in C++ del processore Xalan-J sviluppato nell'ambito dell'Apache XML Project e attualmente utilizzato da Cocoon nei siti di presentazione del progetto HELM.

3

Al momento, le teorie vengono rese giustapponendo la rappresentazione dei singoli oggetti che le compongono.

4

Gli hyperlink sono collegamenti conformi allo standard XLink introdotti durante le trasformazioni dal formato del sistema logico a quello content e successivamente propagati nella successiva trasformazione. Non sono ancora riconosciuti dai browser standard e, pertanto, non sono ancora usufruibili usando la precedente interfaccia.

5

Vengono riportati solamente i metodi effettivamente utilizzati, tranne quelli ereditati dalla superclasse GContainer.container, che vengono tutti omessi.

6

A patto di essere pazienti! Poiché viene utilizzato lo stesso processore XSLT usato con Cocoon, le prestazioni sono deludenti per le stesse motivazioni esposte a pagina 7.1.1.

Chapter 8   Conclusioni

• 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.

8.1   Confronto fra i progetti HELM e MathWeb

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

8.1.1   Il contenuto informativo delle prove

8.1.2   La presentazione delle prove

8.1.3   Il formato dei documenti matematici

8.1.4   Il modello di distribuzione

8.1.5   I meccanismi di indicizzazione e ricerca

8.2   Lavori Futuri

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.

Appendix A   Il DTD per il livello dei termini e degli oggetti di CIC

<?xml encoding="ISO-8859-1"?>

<!--*****************************************************************-->
<!-- DTD FOR CIC OBJECTS:                                            -->
<!--  First draft: September 1999, Claudio Sacerdoti Coen            -->
<!--  Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena -->
<!--  Next Revision: April 4 2000, Claudio Sacerdoti Coen            -->
<!--  Next Revision: June 19 2000, Claudio Sacerdoti Coen            -->
<!--  Last Revision: June 20 2000, Claudio Sacerdoti Coen            -->
<!--*****************************************************************-->

<!-- CIC term declaration -->

<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|CONST|
                  MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX)'>

<!-- CIC objects: -->

<!ELEMENT Definition (body, type)>
<!ATTLIST Definition
          name       CDATA      #REQUIRED
          params     CDATA      #REQUIRED
          paramMode  (POSSIBLE) #IMPLIED
          id         ID         #REQUIRED>

<!ELEMENT Axiom (type)>
<!ATTLIST Axiom
          name   CDATA #REQUIRED
          params CDATA #REQUIRED
          id     ID    #REQUIRED>

<!ELEMENT CurrentProof (Conjecture*,body,type)>
<!ATTLIST CurrentProof
          name CDATA #REQUIRED
          id   ID    #REQUIRED>

<!ELEMENT InductiveDefinition (InductiveType+)>
<!ATTLIST InductiveDefinition
          noParams NMTOKEN #REQUIRED
          params   CDATA   #REQUIRED
          id       ID      #REQUIRED>

<!ELEMENT Variable (type)>
<!ATTLIST Variable
          name CDATA #REQUIRED
          id   ID    #REQUIRED>

<!-- Elements used in CIC objects, which are not terms: -->

<!ELEMENT InductiveType (arity,Constructor*)>
<!ATTLIST InductiveType
          name      CDATA        #REQUIRED
          inductive (true|false) #REQUIRED>

<!ELEMENT Conjecture %term;>
<!ATTLIST Conjecture
          no NMTOKEN #REQUIRED>

<!ELEMENT Constructor %term;>
<!ATTLIST Constructor
          name CDATA #REQUIRED>

<!-- CIC terms: -->

<!ELEMENT LAMBDA (source,target)>
<!ATTLIST LAMBDA
          id ID #REQUIRED>

<!ELEMENT PROD (source,target)>
<!ATTLIST PROD
          id ID #REQUIRED>

<!ELEMENT CAST (term,type)>
<!ATTLIST CAST
          id ID #REQUIRED>

<!ELEMENT REL EMPTY>
<!ATTLIST REL
          value  NMTOKEN #REQUIRED
          binder CDATA   #REQUIRED
          id     ID      #REQUIRED>

<!ELEMENT SORT EMPTY>
<!ATTLIST SORT
          value CDATA #REQUIRED
          id    ID    #REQUIRED>

<!ELEMENT APPLY (%term;)+>
<!ATTLIST APPLY
          id ID #REQUIRED>

<!ELEMENT VAR EMPTY>
<!ATTLIST VAR
          relUri CDATA #REQUIRED
          id     ID    #REQUIRED>

<!ELEMENT META EMPTY>
<!ATTLIST META
          no NMTOKEN #REQUIRED
          id ID      #REQUIRED>

<!ELEMENT CONST EMPTY>
<!ATTLIST CONST
          uri CDATA #REQUIRED
          id  ID    #REQUIRED>

<!ELEMENT MUTIND EMPTY>
<!ATTLIST MUTIND
          uri    CDATA   #REQUIRED
          noType NMTOKEN #REQUIRED
          id     ID      #REQUIRED>

<!ELEMENT MUTCONSTRUCT EMPTY>
<!ATTLIST MUTCONSTRUCT
          uri      CDATA   #REQUIRED
          noType   NMTOKEN #REQUIRED
          noConstr NMTOKEN #REQUIRED
          id       ID      #REQUIRED>

<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
<!ATTLIST MUTCASE
          uriType CDATA   #REQUIRED
          noType  NMTOKEN #REQUIRED
          id      ID      #REQUIRED>

<!ELEMENT FIX (FixFunction+)>
<!ATTLIST FIX
          noFun NMTOKEN #REQUIRED
          id    ID      #REQUIRED>

<!ELEMENT COFIX (CofixFunction+)>
<!ATTLIST COFIX
          noFun NMTOKEN #REQUIRED
          id    ID      #REQUIRED>

<!-- Elements used in CIC terms: -->

<!ELEMENT FixFunction (type,body)>
<!ATTLIST FixFunction
          name     CDATA   #REQUIRED
          recIndex NMTOKEN #REQUIRED>

<!ELEMENT CofixFunction (type,body)>
<!ATTLIST CofixFunction
          name     CDATA   #REQUIRED>

<!-- Sintactic sugar for CIC terms and for CIC objects: -->

<!ELEMENT source %term;>

<!ELEMENT target %term;>
<!ATTLIST target
          binder CDATA #IMPLIED>

<!ELEMENT term %term;>

<!ELEMENT type  %term;>

<!ELEMENT arity %term;>

<!ELEMENT patternsType  %term;>

<!ELEMENT inductiveTerm  %term;>

<!ELEMENT pattern  %term;>

<!ELEMENT body  %term;>

Appendix B   La rappresentazione OCaml dei termini e degli oggetti CIC

type sort =
   Prop
 | Set
 | Type
and name =
   Name of string
 | Anonimous
and term =
   Rel of int                             (* DeBrujin index *)
 | Var of UriManager.uri                  (* base uri, name *)
 | Meta of int				  (* numeric id *)
 | Sort of sort                           (* sort *)
 | Cast of term * term                    (* value, type *)
 | Prod of name * term * term             (* binder, source, target *)
 | Lambda of name * term * term           (* binder, source, target *)
 | Appl of term list                      (* arguments *)
 | Const of UriManager.uri * int          (* uri, number of cookings*)
 | MutInd of UriManager.uri * int * int   (* uri, cookingsno, typeno*)
 | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
    int * int                             (*  typeno, consno  *)
 | MutCase of UriManager.uri * int *      (* ind. uri, cookingsno, *)
    int *                                 (*  ind. typeno,         *)
    term * term *                         (*  outtype, ind. term   *)
    term list                             (*  patterns             *)
 | Fix of int * inductiveFun list         (* funno, functions *)
 | CoFix of int * coInductiveFun list     (* funno, functions *)
and obj =
   Definition of string * term * term *         (* id, value, type,         *)
    (int * UriManager.uri list) list            (*  parameters              *)
 | Axiom of string * term *
    (int * UriManager.uri list) list            (* id, type, parameters     *)
 | Variable of string * term                    (* name, type               *)
 | CurrentProof of string * (int * term) list * (* name, conjectures,       *)
    term * term                                 (*  value, type             *)
 | InductiveDefinition of inductiveType list *  (* inductive types,         *)
    (int * UriManager.uri list) list * int      (*  parameters, n ind. pars *)
and inductiveType = 
 string * bool * term *                   (* typename, inductive, arity *)
  constructor list                        (*  constructors              *)
and constructor =
 string * term * bool list option ref     (* id, type, really recursive *)
and inductiveFun =
 string * int * term * term               (* name, ind. index, type, body *)
and coInductiveFun =
 string * term * term                     (* name, type, body *)
;;

Appendix C   Un esempio di file XML per un oggetto CIC

<?xml version="1.0" encoding="ISO-8859-1"?>

<!DOCTYPE Definition SYSTEM "http://localhost:8081/getdtd?url=cic.dtd">


<Definition name="easy" id="i0" params="">
  <body>
    <LAMBDA id="i1">
      <source>
        <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i2"/>
      </source>
      <target binder="n">
        <APPLY id="i3">
          <CONST uri="cic:/Datatypes/nat_ind.con" id="i4"/>
          <LAMBDA id="i5">
            <source>
              <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i6"/>
            </source>
            <target binder="n0">
              <APPLY id="i7">
                <MUTIND uri="cic:/Logic/or.ind" noType="0" id="i8"/>
                <APPLY id="i9">
                  <MUTIND uri="cic:/Logic/eq.ind" noType="0" id="i10"/>
                  <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                   id="i11"/>
                  <REL value="1" binder="n0" id="i12"/>
                  <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
                   noConstr="1" id="i13"/>
                </APPLY>
                <APPLY id="i14">
                  <MUTIND uri="cic:/Logic/ex.ind" noType="0" id="i15"/>
                  <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                   id="i16"/>
                  <LAMBDA id="i17">
                    <source>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i18"/>
                    </source>
                    <target binder="m">
                      <APPLY id="i19">
                        <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                         id="i20"/>
                        <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                         id="i21"/>
                        <APPLY id="i22">
                          <CONST uri="cic:/Peano/plus.con" id="i23"/>
                          <APPLY id="i24">
                            <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                             noType="0" noConstr="2" id="i25"/>
                            <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                             noType="0" noConstr="1" id="i26"/>
                          </APPLY>
                          <REL value="1" binder="m" id="i27"/>
                        </APPLY>
                        <REL value="2" binder="n0" id="i28"/>
                      </APPLY>
                    </target>
                  </LAMBDA>
                </APPLY>
              </APPLY>
            </target>
          </LAMBDA>
          <APPLY id="i29">
            <MUTCONSTRUCT uri="cic:/Logic/or.ind" noType="0"
             noConstr="1" id="i30"/>
            <APPLY id="i31">
              <MUTIND uri="cic:/Logic/eq.ind" noType="0" id="i32"/>
              <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i33"/>
              <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
               noConstr="1" id="i34"/>
              <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
               noConstr="1" id="i35"/>
            </APPLY>
            <APPLY id="i36">
              <MUTIND uri="cic:/Logic/ex.ind" noType="0" id="i37"/>
              <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i38"/>
              <LAMBDA id="i39">
                <source>
                  <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                   id="i40"/>
                </source>
                <target binder="m">
                  <APPLY id="i41">
                    <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                     id="i42"/>
                    <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                     id="i43"/>
                    <APPLY id="i44">
                      <CONST uri="cic:/Peano/plus.con" id="i45"/>
                      <APPLY id="i46">
                        <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                         noType="0" noConstr="2" id="i47"/>
                        <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                         noType="0" noConstr="1" id="i48"/>
                      </APPLY>
                      <REL value="1" binder="m" id="i49"/>
                    </APPLY>
                    <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                     noType="0" noConstr="1" id="i50"/>
                  </APPLY>
                </target>
              </LAMBDA>
            </APPLY>
            <APPLY id="i51">
              <MUTCONSTRUCT uri="cic:/Logic/eq.ind" noType="0"
               noConstr="1" id="i52"/>
              <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i53"/>
              <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
               noConstr="1" id="i54"/>
            </APPLY>
          </APPLY>
          <LAMBDA id="i55">
            <source>
              <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i56"/>
            </source>
            <target binder="n0">
              <LAMBDA id="i57">
                <source>
                  <APPLY id="i58">
                    <MUTIND uri="cic:/Logic/or.ind" noType="0"
                     id="i59"/>
                    <APPLY id="i60">
                      <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                       id="i61"/>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i62"/>
                      <REL value="1" binder="n0" id="i63"/>
                      <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                       noType="0" noConstr="1" id="i64"/>
                    </APPLY>
                    <APPLY id="i65">
                      <MUTIND uri="cic:/Logic/ex.ind" noType="0"
                       id="i66"/>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i67"/>
                      <LAMBDA id="i68">
                        <source>
                          <MUTIND uri="cic:/Datatypes/nat.ind"
                           noType="0" id="i69"/>
                        </source>
                        <target binder="m">
                          <APPLY id="i70">
                            <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                             id="i71"/>
                            <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                             id="i72"/>
                            <APPLY id="i73">
                              <CONST uri="cic:/Peano/plus.con"
                               id="i74"/>
                              <APPLY id="i75">
                                <MUTCONSTRUCT
                                 uri="cic:/Datatypes/nat.ind"
                                 noType="0" noConstr="2" id="i76"/>
                                <MUTCONSTRUCT
                                 uri="cic:/Datatypes/nat.ind"
                                 noType="0" noConstr="1" id="i77"/>
                              </APPLY>
                              <REL value="1" binder="m" id="i78"/>
                            </APPLY>
                            <REL value="2" binder="n0" id="i79"/>
                          </APPLY>
                        </target>
                      </LAMBDA>
                    </APPLY>
                  </APPLY>
                </source>
                <target binder="H">
                  <APPLY id="i80">
                    <MUTCONSTRUCT uri="cic:/Logic/or.ind" noType="0"
                     noConstr="2" id="i81"/>
                    <APPLY id="i82">
                      <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                       id="i83"/>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i84"/>
                      <APPLY id="i85">
                        <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                         noType="0" noConstr="2" id="i86"/>
                        <REL value="2" binder="n0" id="i87"/>
                      </APPLY>
                      <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                       noType="0" noConstr="1" id="i88"/>
                    </APPLY>
                    <APPLY id="i89">
                      <MUTIND uri="cic:/Logic/ex.ind" noType="0"
                       id="i90"/>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i91"/>
                      <LAMBDA id="i92">
                        <source>
                          <MUTIND uri="cic:/Datatypes/nat.ind"
                           noType="0" id="i93"/>
                        </source>
                        <target binder="m">
                          <APPLY id="i94">
                            <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                             id="i95"/>
                            <MUTIND uri="cic:/Datatypes/nat.ind"
                             noType="0" id="i96"/>
                            <APPLY id="i97">
                              <CONST
                               uri="cic:/Peano/plus.con" id="i98"/>
                              <APPLY id="i99">
                                <MUTCONSTRUCT
                                 uri="cic:/Datatypes/nat.ind"
                                 noType="0" noConstr="2" id="i100"/>
                                <MUTCONSTRUCT
                                 uri="cic:/Datatypes/nat.ind"
                                 noType="0" noConstr="1" id="i101"/>
                              </APPLY>
                              <REL value="1" binder="m" id="i102"/>
                            </APPLY>
                            <APPLY id="i103">
                              <MUTCONSTRUCT
                               uri="cic:/Datatypes/nat.ind"
                               noType="0" noConstr="2" id="i104"/>
                              <REL value="3" binder="n0" id="i105"/>
                            </APPLY>
                          </APPLY>
                        </target>
                      </LAMBDA>
                    </APPLY>
                    <APPLY id="i106">
                      <MUTCONSTRUCT uri="cic:/Logic/ex.ind" noType="0"
                       noConstr="1" id="i107"/>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i108"/>
                      <LAMBDA id="i109">
                        <source>
                          <MUTIND uri="cic:/Datatypes/nat.ind"
                           noType="0" id="i110"/>
                        </source>
                        <target binder="m">
                          <APPLY id="i111">
                            <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                             id="i112"/>
                            <MUTIND uri="cic:/Datatypes/nat.ind"
                             noType="0" id="i113"/>
                            <APPLY id="i114">
                              <MUTCONSTRUCT
                               uri="cic:/Datatypes/nat.ind"
                               noType="0" noConstr="2" id="i115"/>
                              <REL value="1" binder="m" id="i116"/>
                            </APPLY>
                            <APPLY id="i117">
                              <MUTCONSTRUCT
                               uri="cic:/Datatypes/nat.ind"
                               noType="0" noConstr="2" id="i118"/>
                              <REL value="3" binder="n0" id="i119"/>
                            </APPLY>
                          </APPLY>
                        </target>
                      </LAMBDA>
                      <REL value="2" binder="n0" id="i120"/>
                      <APPLY id="i121">
                        <MUTCONSTRUCT uri="cic:/Logic/eq.ind"
                         noType="0" noConstr="1" id="i122"/>
                        <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                         id="i123"/>
                        <APPLY id="i124">
                          <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                           noType="0" noConstr="2" id="i125"/>
                          <REL value="2" binder="n0" id="i126"/>
                        </APPLY>
                      </APPLY>
                    </APPLY>
                  </APPLY>
                </target>
              </LAMBDA>
            </target>
          </LAMBDA>
          <REL value="1" binder="n" id="i127"/>
        </APPLY>
      </target>
    </LAMBDA>
  </body>
  <type>
    <CAST id="i128">
      <term>
        <PROD id="i129">
          <source>
            <MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i130"/>
          </source>
          <target binder="n">
            <APPLY id="i131">
              <MUTIND uri="cic:/Logic/or.ind" noType="0" id="i132"/>
              <APPLY id="i133">
                <MUTIND uri="cic:/Logic/eq.ind" noType="0" id="i134"/>
                <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                 id="i135"/>
                <REL value="1" binder="n" id="i136"/>
                <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
                 noConstr="1" id="i137"/>
              </APPLY>
              <APPLY id="i138">
                <MUTIND uri="cic:/Logic/ex.ind" noType="0" id="i139"/>
                <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                 id="i140"/>
                <LAMBDA id="i141">
                  <source>
                    <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                     id="i142"/>
                  </source>
                  <target binder="m">
                    <APPLY id="i143">
                      <MUTIND uri="cic:/Logic/eq.ind" noType="0"
                       id="i144"/>
                      <MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
                       id="i145"/>
                      <APPLY id="i146">
                        <CONST uri="cic:/Peano/plus.con" id="i147"/>
                        <APPLY id="i148">
                          <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                           noType="0" noConstr="2" id="i149"/>
                          <MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
                           noType="0" noConstr="1" id="i150"/>
                        </APPLY>
                        <REL value="1" binder="m" id="i151"/>
                      </APPLY>
                      <REL value="2" binder="n" id="i152"/>
                    </APPLY>
                  </target>
                </LAMBDA>
              </APPLY>
            </APPLY>
          </target>
        </PROD>
      </term>
      <type>
        <SORT value="Prop" id="i153"/>
      </type>
    </CAST>
  </type>
</Definition>

Bibliografia

[APSSa]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. Content Centric Logical Environments. Short Presentation at LICS 2000.

[APSSb]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. Formal Mathematics in MathML. To be presented at MathML International Conference 2000.

[APSSc]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. Towards a Library of Formal Mathematics. Accepted at TPHTOOLS 2000.

[APSSd]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. XML, Stylesheets and the re-mathematization of formal content. Submitted to LPAR 2000.

[Bar92]

Barendregt H. Lambda Calculi with Types. In Abramsky, Samson and others, editor, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.

[BBC⁺97]

Barras B., Boutin S., Cornes C., Courant J., Filliatre J. C., Giménez E., Herbelin H., Huet G., Munoz C., Murthy C., Parent C., Paulin-Mohring C., Saibi A., and Werner B. The Coq Proof Assistant Reference Manual : Version 6.1. Technical Report RT-0203, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1997.

[Ber89]

Berners-Lee T. Information Management: A Proposal. 1989.

[BW97]

Barras B. and Werner B. Coq in Coq. Submitted, 1997.

[CKT95]

Coscoy Y., Kahn G., and Thery L. Extracting Text from Proofs. Technical Report RR-2459, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1995.

[Coq86]

Coquand T. An Analysis of Girard's Paradox. In Symposium on Logic in Computer Science, Cambridge, 1986. MA. IEEE press.

[dBr80]

de Bruijn N. G. A survey of the project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 589--606. Academic Press, 1980.

[Geu93]

Geuvers H. Logics and Type Systems. Ph.D. dissertation, Catholic University Nijmegen, 1993.

[Gil60]

Gilmore P. C. A proof method for quantification theory: Its justification and realization. In IBM Journal of research and development, volume 4, pages 28--35, 1960.

[Gim94]

Giménez E. Codifying guarded definitions with recursive schemes. In Types'94: Types for Proofs and Programs, volume 996 of LNCS. Springer-Verlag, 1994. Extended version in LIP research report 95-07, ENS Lyon.

[Gim98]

Giménez E. A Tutorial on Recursive Types in Coq. Technical Report RT-0221, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1998.

[GLT89]

Girard J. Y., Lafont Y., and Taylor P. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Har94]

Harrison J. The QED Manifesto. In Automated Deduction - CADE 12, volume 814 of Lecture Notes in Artificial Intelligence, pages 238--251. Springer-Verlag, 1994.

[Har96]

Harrison J. A Mizar Mode for HOL. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, pages 203--220, Turku, Finland, 1996. Springer-Verlag.

[HKP98]

Huet G., Kahn G., and Paulin-Mohring C. The Coq Proof Assistant. A Tutorial, 1998.

[Hor99]

Horacek H. Presenting Proofs in a Human Oriented Way. In 16th International Conference on Automated Deduction, 1999.

[ISO8879]

Standard Generalized Markup Language (SGML). ISO 8879:1986.

[Jut94]

Jutting van L. S. B. Checking Landau's ``Grundlagen'' in the AUTOMATH System. Ph d. thesis, Eindhoven University of Technology, 1994. Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732.

[Luo90]

Luo Z. An Extended Calculus of Constructions. PhD thesis, 1990.

[Mac95]

MacKenzie D. The automation of proof: A historical and sociological exploration. In IEEE: Annals of the History of Computing, 1995.

[Mas64]

Maslow S. J. An inverse method for establishing deducibility in classical predicate calculus. In Doklady Akademii Nauk, volume 159, pages 17--20, 1964.

[NL98]

Necula G. C. and Lee P. Efficient Representation and Validation of Proofs. In Proceedings of the 13th Annual symposium on Logic in Computer Science,, Indianapolis, 1998.

[NS56]

Newell A. and Simon H. A. The logic theory machine. In IRE Transactions on Information Theory, volume 2, pages 61--79, 1956.

[Pau89]

Paulin-Mohring C. Extraction de programmes dans le Calcul des Constructions. Thèse d'université, Paris 7, January 1989.

[Pra60]

Prawitz D. An improved proof procedure. In Theoria, volume 26, pages 102--139, 1960.

[Ric99]

Ricci A. Studio e progettazione di un modello RDF per biblioteche matematiche elettroniche, 1999.

[Rob65]

Robinson J. A. A machine-oriented logic based on the resolution principle. In Journal of the ACM, volume 2, pages 23--41, 1965.

[SH95]

Saibi A. and Huet G. Constructive Category Theory. In Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory, Goteborg (Sweden), January 1995.

[W3Ca]

Extensible Markup Language (XML) 1.0 W3C Reccomendation. http://www.w3.org/TR/1998/REC-xml-19980210.

[W3Cb]

Mathematical Markup Language (MathML) 1.01 W3C Reccomendation. http://www.w3.org/TR/REC-MathML.

[Wan60]

Wang H. Toward mechanical mathematics. In IBM Journal of research and development, volume 4, pages 2--22, 1960.

[Wer94]

Werner B. Une Théorie des Constructions Inductives. Ph.D. dissertation, Universite Paris 7, May 1994.

[Wer97]

Werner B. Constructive Category Theory. In Proocedings of the International Symposium on Theoretical Aspects of Computer Software, 1997.