The Hypertextual Electronic Library of Mathematics
Main Projectual Provisos
The next, compelling step for every tool
aimed at the automation of formal reasoning and
the mechanization of mathematics is its integration
with (and exploitation through) the World Wide Web.
This simple statement borrows already a few major
methodological provisos:
 Standardisation
By standardisation, we only mean the representation of the information
in a clearly defined, application independent format. We have no
foundational ambition, and do not aim to impose our solution.
XML, which is rapidly imposing
as a pivotal technology in the future development of
all internet applications, and the main tool for
representation, manipulation, and exchange of structured information
in the networked age, looks as a natural, almost mandatory tool
to be used in the encoding. Special dialects of XML, such as
MathML can be reasonably used as a standardisation language
for presentational and notational aspects of the information.
 DistributionThe Library must be distributed.
The overall policy must be as liberal as possible, respecting
the general philosophy of the Web: everybody
with a web or ftp space should be allowed to publish its piece
of theory.
 SimplicityThe kernel system should be as light as
possible, and try to profit of all existing technology for
webpublishing and displaying already existing on the market.
It should be conceived as an open system, in the most
general sense of the term. It should be possible to
add more functionalities and utilitites with a minimal effort
and no impact on the kernel.
Current tools are often conceived as more or less monolitich
architectures. To extend the system you are forced to use
the utilities offered by the system itself, with obvious
limitations.
Markup and semantic components
The kernel system is only meant to support
the basic management of mathematical documents
through their lifespan, but in order to support
additional functionalities the intelligence encoded
in the markup should cover all potential uses
to which such documents will be put. To this aim, we
must clearly identify all semantic components of a
typical mathematical document and classifying them
into logical categories (content, structure,
presentation, notation, metadata, \dots). As
a main methodological assumption, we try to keep
a clear distinction between all these components,
as far as possible. Similarly, we aim to reuse all
existing technology and recommended standardization
formats (such as MathML or RDF) for representing and
modeling suitable parts of the information.
We have already identified the following main components:
 low level structural information. This reflects both the
fine grane structure of mathematical expressions and
proofs. This level does usually strictly depend on the
particular formalism adopted. There is little hope to have
a uniform language at this level.
 high level structural information. This level reflects
the organization of mathematical documents as a structured
collection of atomic results. Good hope to reach some
consensus on a common representation. Still, the
distinction between lemmas, propositions, facts, theorems,
etc. (if any) is far from clear.
The relevance of standardisation at this level is mainly related
to the possibility to add relevant metadata in a uniform way.
 basic "content" information. The low level structural
information can be translated via a set of XSLT rules in an
intermediate language more suited to be directly published
in a human readable format. This look particularly important
for portability reasons. The content part of MathML
looks as a good candidate as target language. We need
backwards pointers to the low level representation, in form of
xpointers.
Similarly, content is supposed to be transformed in a
format suited to presentation by a further XSLT transformation.
Such a transfromation form content to presentation for
MathML has been already defined (add reference). Again,
we need backwards pointers to content.
In conclusion, for browsing purposes, we shall essentially need
a gtk widget able to interpret MathML presentational tags, that looks
quite feasible (again, something already exists).
 annotations information. This is meant as a natural language
annotation for proof, and it has to be integrated wwith the low
structural level (or intermediate content level), typically during
interactive editing.
 notational and stylistic information. This is to be integrated
with the low level (or intermediate level) to give a precise
description of the intended output. Notation and stylistic
information is mainly intended for expressions (not proofs).
Both annotations and notations are supposed to be used as
user defined "macros" extending and integrating the original set of
XSLT transformations to get the desired presentation.
 metadata. We could distinguish between two kinds of metadata:
intrinsic and extrinsic. By intrinsic metadata we mean all those
information wich can be automatically recovered by the structured
representation of the terms and proofs (such as, say, the list of
identifiers occurring in a term, or the main identifier in the
conclusion of a statement). As a methodological assumption,
intrinsic metadata will not be covered in the kernel system.
Anybody is free to extract them, whenever required.
Extrinsic metadata are all those auxiliary data which cannot
be inferred by the information itself (such as the name of
the author, the date, or a list of keywords). Extrinsic
metadata must be explicitly modeled. They concerns both
level of structural information.
Figure 1:
A DTD for COQ
For our development, we have
adopted COQas a
paradigmatic example of a typical logical framework.
The first phase of HELM has been centered on the problem
of exporting coq objects into XML format.
This has already an interest in its own, for at least three
reasons:

Exporting from Coq internal representation to an open representation, such
as XML, will make the libraries survive system Coq when one day it will be
outpassed. This is important because a lot of theories developed in old
proof checkers are now unuseful only because they were stored in internal
representations that are now unreadable.

The existing libraries of Coq are a good starting point for developing
new theories. They are also an interesting challenge for a brand new
typechecker for the Calculus of (Co)Inductive Construction.

Coq has a powerful, but not yet well explored, system of sections that
make possible to develop new theories defining their axioms and then
use them from other theories instatiating the axioms (that
behave like variables). This is an interesting idea, but in our opinion
the actual implementation of Coq does not exploit it well. An extension
of the theory of cic that would include also sections as ``first class
objects'' looks feasible and really very interesting.
What should NOT be exported from Coq?
Not all information useful to Coq should be exported. In particular we have
choosed not to export:

Parsing and prettyprinting rules and information

Parsing rules should depend only on the proof engine. To be able to
use other proof engines different from Coq we need not to rely on Coq's own
rules. Similarly, prettyprinting rules should depend only on the browser.
 Tacticsrelated information

This, too, are proof engine dependent.
 Redundant information added by Coq to the terms of cic

Coq adds in several places a lot of information to cic terms in order to
fasten the typechecking. This information is clearly redundant, is
unuseful for browsing and could be unuseful also for other typecheckers.
What should be exported from Coq?
The following Coq objects are exported:

Constants (definitions/theorems/axioms)

Constant objects of Coq are used to represent definitions, theorems and
also axioms. Definitions and theorems are syntactically identical and have
a body and a type. The only difference is semantical: theorems are usually
opaque (only their type is used in cic terms) because of proofirrelevance,
while definitions are transparent (their body is substituted in their
occurrences in other terms during type checking). Axioms, instead, are
constants with a type but without a body. We choose, during extraction,
to discriminate only axioms from definitions and theorems, that become
undistinguishable once extracted. We suppose that there will exist another
level (a semantical one) responsible of ``marking'' non axiom constants as
theorems, definitions, lemma, facts, ...
Due to the sectioning machinery of Coq, constants defined inside
a section are found in the environment many times: once in the uncooked
form and once for each section in their section path. We choosed to export
a constant in its uncooked form, but adding informations (the list of
variables on which it depends) gotten from the most cooked form.
 Variables

Variables have only a type and not a body. A variable behaves like an
axiom inside the theory where it is defined and as a parameter when
using that theory.
 (Co)Inductive Definitions

In Coq, you can define also blocks of mutual (co)inductive definitions.
Each definition inside such a block has a name, a type (also called
arity in Coq) and a possibly empty list of constructors. Each
constructor has a name and a type. A simple example is the inductive type
of naturals whose name is nat, whose type is Set and whose
constructors are O of type nat and S of type
(nat > nat). Blocks, as constants, could depend on variables;
the
list of variables (parameters) on which all the definitions in the block
depend is also exported from Coq.
 Proof in progress

We choosed also to export unterminated proofs. As terminated theorems,
an unterminated proof has a name, a type and a body; moreover, it has also
a list of conjectures on which the body depends. Each conjecture has a type
but not a body: to end the proof you must provide a body
for each conjecture.
Sections and cookings in Coq
In Coq it's possible to use sections. To make a section, you must open it,
fill it and then close it. Filling a section means declaring in it other
objects, i.e. variables, constants, local definitions, mutual (co)inductive
types or subsections. So the structure describing sections and subsections in
Coq is naturally a tree.
The names given to objects in the current environment must ever be unique:
for example, if in a supersection an axiom A is defined, you can't
define another one in the current section. When you close a section, though,
all the variables and the local definitions defined in it are discharged and
all the constants and (co)inductive definitions in it are cooked, i.e.
lambdaabstracted with respect to all the discharged variables (ingredients)
that are used, directly or indirectly, inside their bodies. The body of a
local definition, instead, is substituted to all the references to it inside
each cic term of a notdischarged object. Example:
Section a.
Variables V1,V2 : Prop.
Axiom A1 : V1 > V2.
Axiom A2 : (P:Prop)P > V1.
Local Apply := [x:V1>V2][y:V1](x y).
Theorem T : (P:Prop)P > V2.
Exact [P:Prop ; H:P](Apply A1 (A2 P H)).
Qed.
End a.
After End a. the variables V1 and V2 and the local definition
Apply are discharged. The other objects become equal to the ones defined,
without using sections, in this way:
Axiom A1 : (V1,V2:Prop)V1 > V2.
Axiom A2 : (V1,P:Prop)P > V1.
Theorem T : (V1,V2,P:Prop)P > V2.
Exact [V1:Prop ; V2:Prop ; P:Prop ; H:P](A1 V1 V2 (A2 V1 P H)).
Qed.
Note that A2 is abstracted only w.r.t. V1 because it doesn't
depend on V2 and that T is abstracted also w.r.t. V1
on which it depends only implicitly through A1 and A2.
In order to improve performance, Coq implementation of cooking is not uniform
on all the objects:

Objects that are thought to be used often, i.e. inductive definitions and
``destructor'' functions on inductive definition (the ones ending in
``ind'', ``rec'' and ``rect'') are replaced with the
cooked ones: this is the trivial implementation.

Other constants (all the definitions, axioms and functions that
are not destructors of inductive definition) are replaced with
recipes. A recipe is a pointer to an uncooked term or to another
recipe plus an ordered list of ingredients and some other information.
During typechecking, every time an expression (Apply R P_{1} ... P_{n})
is met where R is a recipe whose content is R' and whose list of
ingredients is P'_{1} ... P'_{m} with m < n, then the expression is
reduced to (Apply R'[P_{1}/P'_{1} ... P_{n}/P'_{n}] P_{m+1} ... P_{n}).
The DTD
Here is the current draft of a DTD for the low level structure of
Coq term
<?xml encoding="ISO88591"?>
<!*****************************************************************>
<! DTD FOR CIC OBJECTS: >
<! First draft: September 1999, Claudio Sacerdoti Coen >
<! Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena >
<!*****************************************************************>
<! CIC term declaration >
<!ENTITY % term '(LAMBDACASTPRODRELSORTAPPLYVARMETAIMPLICITCONST
ABSTMUTINDMUTCONSTRUCTMUTCASEFIXCOFIX)'>
<! CIC objects: >
<!ELEMENT Definition (body, type)>
<!ATTLIST Definition
name CDATA #REQUIRED
params CDATA #REQUIRED
param_mode (POSSIBLE) #IMPLIED>
<!ELEMENT Axiom (type)>
<!ATTLIST Axiom
name CDATA #REQUIRED
params CDATA #REQUIRED>
<!ELEMENT CurrentProof (Conjecture*,body,type)>
<!ATTLIST CurrentProof
name CDATA #REQUIRED>
<!ELEMENT InductiveDefinition (InductiveType+)>
<!ATTLIST InductiveDefinition
noParams NMTOKEN #REQUIRED
params CDATA #REQUIRED>
<!ELEMENT Variable (type)>
<!ATTLIST Variable
name CDATA #REQUIRED>
<! Elements used in CIC objects, which are not terms: >
<!ELEMENT InductiveType (arity,Constructor*)>
<!ATTLIST InductiveType
name CDATA #REQUIRED
inductive (truefalse) #REQUIRED>
<!ELEMENT Conjecture %term;>
<!ATTLIST Conjecture
no NMTOKEN #REQUIRED>
<!ELEMENT Constructor %term;>
<!ATTLIST Constructor
id CDATA #REQUIRED>
<! CIC terms: >
<!ELEMENT LAMBDA (source,target)>
<!ELEMENT PROD (source,target)>
<!ELEMENT CAST (term,type)>
<!ELEMENT REL EMPTY>
<!ATTLIST REL
value NMTOKEN #REQUIRED>
<!ELEMENT SORT EMPTY>
<!ATTLIST SORT
value CDATA #REQUIRED>
<!ELEMENT APPLY (%term;)+>
<!ELEMENT VAR EMPTY>
<!ATTLIST VAR
relUri CDATA #REQUIRED>
<!ELEMENT META EMPTY>
<!ATTLIST META
no NMTOKEN #REQUIRED>
<!ELEMENT IMPLICIT EMPTY>
<!ELEMENT CONST EMPTY>
<!ATTLIST CONST
uri CDATA #REQUIRED>
<!ELEMENT ABST EMPTY>
<!ATTLIST ABST
uri CDATA #REQUIRED>
<!ELEMENT MUTIND EMPTY>
<!ATTLIST MUTIND
uri CDATA #REQUIRED
noType NMTOKEN #REQUIRED>
<!ELEMENT MUTCONSTRUCT EMPTY>
<!ATTLIST MUTCONSTRUCT
uri CDATA #REQUIRED
noType NMTOKEN #REQUIRED
noConstr NMTOKEN #REQUIRED>
<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
<!ATTLIST MUTCASE
uriType CDATA #REQUIRED
noType NMTOKEN #REQUIRED>
<!ELEMENT FIX (FixFunction)+>
<!ATTLIST FIX
noFun NMTOKEN #REQUIRED>
<!ELEMENT COFIX (CofixFunction)+>
<!ATTLIST COFIX
noFun NMTOKEN #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 patternsType %term;>
<!ELEMENT inductiveTerm %term;>
<!ELEMENT pattern %term;>
<!ELEMENT body %term;>
2.1.9 The code
We have firmly choosed not to modify Coq at all to export XML files. So we have
written a brand new ``tactic'' named Xml (to be stored in
tactics/contrib/xml). The tactic is very dependent on the internal
data structures of Coq, that are now changing version after version. So we hope
that the tactic will be accepted in the set of standard contributions to Coq
(so that it will be considered when modifing Coq's code). Once loaded via
``Require Xml.'', four new commands become availables to Coq users:
...SPIEGAZIONE DELLE TATTICHE
To implements these new commands we have written some OCaml modules and a
vernacular file Xml.v:
Figure 1:
Parsing
Once exported in XML, we need to parse CIC objects and
put them in memory in an internal, useful representation. While the XML
representation should be kept small and unredundant as much as possible
(redundancy means more space occupied and more consistency checks), the
internal representation is thought to fasten the subsequent accesses to the
information (e.g. duging typechecking), at the price of overloading the
parsing phase.
Our parser has been built using Markup. Markup is a generic validating XML
parser written by ??? entirely and from scratch in OCaml. Being a validating
XML parser, it is really fast (as fast as the nsgml parser written by J. Clarck
for SGML and faster than the validating XML parser XML::Parser ??? written in
Perl). Absolutely speaking, though, it is not too fast (it takes about six
minutes to parse all the standard library of Coq): this is due to the huge
dimensions of the XML files (the standard library of Coq is about 80Mb in
uncompress form and reduces to 34Mb once compressed) and perhaps also to
validation.
How to fasten parsing time
First of all, should we really need a validating XML parser? The first answer
seems to be yes because it is really important for a system like ours to be
able to detect errors. But in fact a lot of controls have subsequently been
added during parsing and will be in subsequently phases, up to typechecking
the entire proof. So, in next phases, when we'll have a clear view of how
heavy is parsing on the entire computation, we'll turn back and consider again
the use of a validating parser.
Another point is how much syntactic sugar should we put in XML files? Up to now
we have put a lot (50%) of syntactic sugar in XML files so that the files are
easily readable to anyone knowing CIC. For debugging purpouses this is great.
But, once finished, should XML files really be easily readable by humans? This
is one of the aims (a lesser one, thoug) of XML, but we must remember that in
CIC it doesn't exist a short proof: non trivial proofs are at least of some
hundreds of lines of XML and really very difficult to understand without a
proofchecker. It is also quite impossible to anyone to write a proof directly
in CIC without the help of a proof engine. So, in next phases, we'll reconsider
also if getting rid of the syntactic sugar.
The internal representation
Once parsed, the objects of CIC are stored internally using two concrete
datatypes (term for the term level and obj for the object level)
whose constructors are chosen to match exactly the entities present in the
CIC DTD. Uris are all translated during parsing in absolute uris, even if
they
are encoded in the XML file as relative ones. In subsequent phases we will
need a fair elaborate datastructure for the uris to be able, for example,
to determine fastly if two uris are equal of if one uri is a prefix of another.
So we introduce an UriManager, i.e. an OCaml module declaring an abstract
data type uri and the functions to use it.
The code
Markup's main function takes in input the name of the xml file to parse, and
a bunch of options; then it parses and validates the file building the concrete
syntax tree that is returned. There are two possible ways to use the tree:

Functional style:
 the type of the concrete syntax tree is a concrete
datatype. So it is simple to write a bundle of recursive functions to
navigate the tree retrieving the information needed.
 Object Oriented style:
 it is possible to write a set of classes with
the same interface, instantiate each class to a clonable object called a
prototype and tell markup to link each node of the tree to a copy of
a particular prototype. The map from XMLelement names to prototypes is
called a DOM in markup. Therefore, it is possible to access the tree
in an objectoriented way simply calling the methods of the objects linked
to each node of the tree.
None of the two solutions is better of the other:
The functional style takes less memory (no prototypes and objects) than
the objectoriented style, but it may be less efficient: the recursive
functions used to navigate the tree for each node of the tree must try to
match the XMLelement name to decide what action should be performed. This
means a lot of string comparisons that are notoriously slow. In the
objectoriented style the stringmatches are done only one, when choosing
which prototype to clone, and an hashtable is used to fasten the search.
Thereafter, for each method called, only a method (dynamic) dispatch is needed,
which is not so heavy. From the point of view of software engineering,
though, the objectoriented style seems preferable.
What we need is a parser able to translate the generic XML concrete syntax tree
to our internal representation of the same tree (defined in the OCaml module
Cic).
The dtd of CIC has two welldistinct levels: the level of the objects and that
of the terms. We have choosed to use the functional style when accessing the
object level (that has only few XMLelement types) and the objectoriented
style when accessing the term level. So we have splitted the implementation of
the parser into three different modules:

CicParser
 The toplevel parser. It's main functions, given the name
of an XML file containing a CIC object, returns the internal representation
of that object once parsed. This should be the only module accessed from
other OCaml modules; next two modules should be used directly only by this
one.
 CicParser2
 The objectlevel parser. In this module are defined the
recursive functions to convert the objectlevel nodes of markup trees to
the internal representation. It uses next module every time that one node
has a subnode at the terms level.
 CicParser3
 The termlevel parser. It defines the DOM for translating
a termlevel node of markup to the internal representation.
Figure 2:
aggiungere la spiegazione su come vengono risolte le uri relative
cambiare get_term in CicParser2 to get_obj
Overall architecture
Figure 3:
Figure 3 shows the overall architecture of helm at this phase.
At this early stage we consider only the
term and object levels, i.e. the single theorem, axiom, and so on. Obviously
we will need to build another level, the theory level, in which whole theories
(=structured sequences of theorems, axioms, etc.) will be taken into account.
As said, we want to isolate the modules depending on CIC in order to be able
to substitute easily the logical framework with another one.
At the top level we will have many interfaces to browse and
typecheck the single objects. Actually we plan at least to put together a
textual interface and a gtk interface. We require also that adding a brand
new toplevel interface should be easy and should not require modifications
to lowerlevel modules.
Then we have some modules that are strictly dependent
on the logical framework: the pretty printer(s) (CicPp) will be able to
translate the internal format to something that could be used by the toplevel
(mathml, for example). Probably many pretty printers will be developed. The
typechecker (CicTypeChecker) proofchecks objects once put in the internal
format. Every time one of these modules needs one object, it requires it to
the cache (CicCache). If a cache miss occurs, the cache is responsible to
ask the getter (Getter) to retrieve the XML file describing the object from
the Internet; once retrieved, the XML file is passed to the parser
that returns the internal representation of the object to be put into the
cache. As just said, the parser, the prettyprinter, the cache and the parser
depends heavily on the logical framework and on the internal representation
of it's objects, that will be described by the Cic module. Instead, the Getter
and the UriManager modules should be independent of the logical framework.
In order to test the parsing modules and to debug the tactic developed to
export terms from Coq, during this phase we have implemented all the remaining
modules (but the typechecker) in a trivial way: uris and filenames are the
same thing so that the getter actually does nothing at all and the UriManager
is easily coded. The cache is simply implemented as an hashtable (nothing is
never flushed from the cache). Finally the prettyprinter translates the
internal representation to the same textual description used by system Coq
and the two interfaces simply display that description, either in a terminal
(Experiment) or in a gtk text area (GtkInterface).