The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

 Hi,

> If the (number of XML markup characters / number of proof data characters)
> ratio is a constant

 just a couple of observations on this:

   1. counting the number of characters also means counting space characters
      used for the indentation. It is better to count the number of
      XML elements, i.e. it is better to add to the number of ">" characters
      the number of "/>" characters. Each XML element corresponds to one
      constructor in the data type used to represent terms internally.
      (Of course, you are neglecting the fact that different constructors
      require a different number of bytes in memory, but I think that this
      is not your point, right?)
   2. the internal representation of Coq tries to share as much as possible
      the terms (and thus also the proofs). For instance, all occurrences
      of (Rel 1) (i.e. every occurrence of the last bound variable) are
      actually shared in the internal representation. That means that a
      Coq's term is really a DAG and not a tree. On the contraty the XML
      representation is really tree-like and purpousely destroys the
      internal sharing. Once again, it is up to you to decide what do you
      want to measure.

                                                Regards,
                                                C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------