[Prev][Next][Index][Thread]
semantical annotations

To: w3cmatherb@w3.org

Subject: semantical annotations

From: Ron Whitney <RFW@MATH.AMS.ORG>

Date: Sun, 08 Sep 1996 10:17:32 0400 (EDT)

From w3cmatherbrequest@www10.w3.org Sun Sep 8 10: 18:09 1996

Mailsystemversion: <MultiNetMM(369)+TOPSLIB(158)+PMDF(5.0)@MATH.AMS.ORG>

Messageid: <842192252.874382.RFW@MATH.AMS.ORG>
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
htmlmath. I was also asking about whether htmlmath notation could
become embedded within semantical annotations because of the
requirement that some typetheoretic 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
typeinformation, 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 ntuples 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 typetheoretic information that no one expects to
specify. I'm certainly not familiar enough with CAS to have a good
concrete expectation of how typetheoretic 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
typetheoretic information a paper might contain, and I'm trying to
ascertain just how "free" the semantical content will be from
htmlmath.
Ron