semantical annotations

Bob writes:

>   Here is a more sophisticated example (I hope you like the type name!):
> 
>  FiniteFieldNormalBasisExtensionByPolynomial(Prime Field 3, X^^3+2*X^^3+2)

I do, I do!  (Doing `semantical' maths is easy, claims Pike.  All one has
to do is roll up one's sleeves and have at it --- as if this is a problem
in insect taxonomy.  Group members, grab your nets!)

Bob mentions that designations of mathematical objects will have to be
embedded within semantical annotations.  This suggests, as he points
out, that there will be a notational aspect to the semantical
information, although that notation might be wholly independent of
html-math.  I was also asking about whether html-math notation could
become embedded within semantical annotations because of the
requirement that some type-theoretic information will be dependent
upon identifiers and operators of the html document itself.

With respect to the particular insect above, I'm assuming that the
annotation could be parameterized so that

   FiniteFieldNormalBasisExtensionByPolynomial(Prime Field `p', X^^3+2*X^^3+2)

would type another extension field, but over the Prime Field of `p'
elements where `p' is a variable local to a certain position within a
given document.  In this way, the document notation might "infect" the
semantic information, since if the local parameter `p' is available for
inclusion then any expression which evaluates (within the paper's
local semantics) to a prime might also be used there.  If an author
is using ^ to mean "power" locally, one might then have

   FiniteFieldNormalBasisExtensionByPolynomial
                                     (Prime Field 2^{2^n}+1, X^^3+2*X^^3+2)

for semantical annotation when someone is talking about the nth Fermat
number.  (The first bit of notation is derived from the local
notation, but the second is specified by OpenMath's standard for
polynomial designation.)  Clearly OpenMath could reduce the
parameterization to just "n" by giving a more extended, verbal
notation for the sequence of Fermat numbers (as is already done with
the "FiniteField..." type), but it still strikes me that
type-information, in the most general case, will be parameterized by
identifiers and operators juxtaposed in the document's notational
scheme.  (Here I'm thinking that although one might have a type
Real(n) for n-tuples of real numbers, one probably wouldn't have a
pure type T(n) which corresponds specifically to Real(n^2+n+1).)  Or
since a CAS would have to concretize such parameters anyway, do we
simply leave the n^2+n+1 part as a "slot" to be determined later?

I may be making this more complicated than it actually is, or I may be
worrying about type-theoretic information that no one expects to
specify.  I'm certainly not familiar enough with CAS to have a good
concrete expectation of how type-theoretic information will be
generated and used by CAS in the coming several years.  (I have a
rough idea of Axiom's workings, but I'm lacking a practical knowledge
here.)  My slant is only from a purist standpoint examining all the
type-theoretic information a paper might contain, and I'm trying to
ascertain just how "free" the semantical content will be from
html-math.


-Ron