[om] About new XML encoding methods for OpenMath

[Michael Kohlhase]

> Don't XML-Schema-types allow a decent approach for that. Something along 
> the lines of: "the parameter to the transc_R:exp function has to be of 
> type real and returns real" which becomes, with a kind of 
> functor/morphism describing the injection of R in C, "the parameter to 
> the transc_C:exp function has to be of type complex and returns complex".
> This looks all too simplistic and I am almost sure I am burning myself 
> at the edge of dangerous typing/logical-foundations...

This is actually, what the Isabelle people have done for a rather
expressive type theory. I am pretty sure that I could generate Schemata out
of the STS type system relatively easily. That is the allure of the
"radical namespaces" encoding. Unfortunately, XML Schemata do not support
subtypes, otherwise we could make all of the "types" subtypes of the OM
type, and do Schema testing by requiring that the content of the OMOBJ,
OMA, and OMB elements are of XMLSchema type OM. 

     Michael

--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems