[Om] Content-dictionary notations draft

[David Carlisle]

Paul,
> This was in comparison to parts of ctop.xsl.

perhaps in the openmath setting, a better comparison than ctop.xsl would
be the stylesheets at 

http://www.openmath.org/cdfiles2/xsl/

They have a similar pedigree, but are already tuned to the existing core
Openmath CDs.


there are named templates for common layout forms such as an infix
operator with a given precedence so as noted in arith1.xsl, + would be
(without worrying about infix -) just


<xsl:template match="om:OMS[@cd='arith1' and @name='plus']"  >
  <xsl:param name="p"/>
  <xsl:call-template name="infix">
    <xsl:with-param name="mo"><mo>+</mo></xsl:with-param>
    <xsl:with-param name="p" select="$p"/>
    <xsl:with-param name="this-p" select="1"/>
  </xsl:call-template>
</xsl:template>

Such paramaterised templates correspond fairly naturally with what you
can do in any "purely declarative" system. Modulo syntax, the above just
says that "plus in arith1" is typeset as an infix operator of precedence
1, using the symbol +, which is about the mininmum amount of information
that needs to be specified in any system.

Looking at templates that do _not_ use call predefined named templates,,
there are the cases already discussed of unary minus, and differential
operators, also several cases involving hiding lambda terms some
constructors expect an application to a function term, forms that are
encoded in OM as apply B (lambda x. f(x)) can often more conventionally
be written as B x. f(x) with B taking on the role of a binder in the
presentation. see for example the template for suchthat in
http://www.openmath.org/cdfiles2/xsl/list1.xsl
which leads to the display you see here:
http://www.openmath.org/cd/list1.xhtml#suchthat

As I commented earlier though it may be possible by reviewing the layout
forms used for the existing CDs to come up with more "named" layout
styles that could be implemented in the XSL as named templates, and
implemented in a purely declarative non-xsl system just by refering to
the named layout. This would reduce the number of symbols for which the
existing stylesheets expose "complicated" explict xslt logic.

Bill's idea of using OpenMath to specify the computational part of the
presentational transformation is appealing but I think suffers form the
problems that you state that it's hard to tie down the computational
behaviour sufficiently, and also it offers too much power, it would
require something like a CA system to have a reasonable chance of
evaluating OM that uses anything other than a minuscule part of the core
CDs, and such a system often isn't available at the places this is
needed. A real example being the CDs themselves which do rely on a
specification of a presentation form for every symbol. Currently
we use XSL, which practically speaking is available in any web server
setup, it's harder to assume that an OpenMath aware CA system would be
available.

If a simpler purely declarative syntax can make something
legible I think we should try to specify that, but as soon as it gets
complicated at all, I think that we should not try to compete with
existing widely implemented languages that can do the same job.

David