[Om3] Summary of the Davenport&Kohlhase Proposal
Michael Kohlhase
m.kohlhase at jacobs-university.de
Mon Mar 23 08:38:50 CET 2009
Dear all,
I promised to summarize the proposal I announced a couple of days ago
(see http://kwarc.info/kohlhase/submit/mkm09-MMLOM3.pdf for a longer
version).
I will use the j-th Lagrange base polynomial of order k
(see e.g. http://en.wikipedia.org/wiki/Lagrange_polynomial) as an
example, as the integration examples we use in the paper are wrought
with other complexities.
The polynomial is represented as
$Pi_{i=0,i\ne j}^k\frac{x-x_i}{x_j-x_i}$ where j and k are free in the
expression, and only i is bound. MathML2 would probably represent this as
<apply>
<product/>
<bvar><ci type="nat">i</ci></bvar>
<lowlimit><cn>0</cn></lowlimit>
<uplimit><ci>k<ci></uplimit>
<condition>
<apply><ne/><ci>i</ci><ci>j</ci></apply>
</condition>
<apply><divide/>...</apply>
</apply>
In OpenMath we would have to represent this as
<OMA>
<OMS cd="arith1" name="product"/>
<OMA> <!-- j, k (free), new dummy variable z (bound) -->
<OMS cd="set1" name="suchthat"/>
<OMA>
<OMS cd="interval1" name="integer_interval"/>
<OMI>0</OMI>
<OMV name="k"/>
</OMA>
<OMBIND>
<OMS cd="fns1" name="lambda"/>
<OMBVAR><OMV name="z"/></OMBVAR>
<OMA>
<OMS cd="relation1" name="ne"/>
<OMV name="z"/>
<OMV name="j"/>
</OMA>
</OMBIND>
</OMA>
<OMBIND>
<OMS cd="fns1" name="lambda"/>
<OMBVAR><OMV name="i"/></OMBVAR>
<OMA>
<OMS cd="arith1" name="divide"/>
...expression in x, j (free) and i (bound) ...
</OMA>
</OMBIND>
</OMA>
James and I don't like that this has two binds and two unrelated dummy
variables, whereas the original mathematical representation on Wikipedia
only had one. Of course, we could have used i in the first one instead
of z, in which case there would still be two binds with two different
bound variables.
To remedy this situations (and others) James and I propose to extend
OpenMath binding objects by allowing more than one "argument": A binding
object would have the form
bind(O,v_1,...,v_n,A_1,...A_n)
rather than the current.
bind(O,v_1,...,v_n,A)
Correspondingly the XML encoding would extend the content model of the
OMBIND object to
omel,OMBVAR,omel+
instead of the current
omel,OMBVAR,omel
So we are proposing a liberalization of OpenMath objects: all OpenMath2
objects are extended Objects and retain their original meanings. But can
now define more mathematical symbols and represent more objects.
In our example, we would propose to develop a new CD (e.g. arith7; I do
not remember that is free) with a new symbol productcond. Which could
have the following description
<CDDefinition>
<Name>productcond</Name>
<Description>
The productcond sysymbol is a ternary binding operator that
takes a bound variable and three arguments. The first argument
is a set, and the second one an expression in the bound variable.
Together these determine the range of the bound variable: The
binding object constructed via the productcond symbol is the
product of all instances of the third arguments with all
those members of the set in the first argument that satisfy the
expression in the second argument.
</Description>
... some examples ...
... An FMP that defines this product, e.g. a recursive definition ...
</CDDefinition>
With this symbol, we can then represent the Lagrange Base Polynomical as
<OMBIND>
<OMS cd="arith7" name="productcond"/>
<OMBVAR><OMV name="i"/><OMBVAR>
<OMA>
<OMS cd="interval1" name="integer_interval"/>
<OMI>0</OMI>
</OMA>
<OMA>
<OMS cd="relation1" name="ne"/>
<OMV name="i"/>
<OMV name="j"/>
</OMA>
<OMA>
<OMS cd="arith1" name="divide"/>
...expression in x, j (free) and i (bound) ...
</OMA>
</OMBIND>
Note that this is a very direct translation of the TeX representation of
Wikipedia. In particular, we only have one bound variable.
We argue that OpenMath should give authors the freedom to express the
mathematical objects directly and succinctly and intuitively as
possible. We argue that even though this is an extension of OpenMath
binding objects, it is conservative (all OpenMath2 objects stay valid
and retain their meaning). Moreover, as the example above has shown, it
is simple to define new symbols (probably in new CDs) that make the
representation in OpenMath simpler and more intuitive.
We should extend OpenMath to gain this freedom and extend the usability
of OpenMath.
Michael
> -----Original Message-----
> From: Michael Kohlhase [mailto:m.kohlhase at jacobs-university.de]
> Sent: Wednesday, March 18, 2009 9:11 PM
> To: David Carlisle
> Cc: Robert Miner; jhd at cs.bath.ac.uk
> Subject: Re: Chapter 4, pragmatic2strict translation, condition
>
>
>
> David Carlisle wrote:
> >> Are you seriously suggesting that the example we use in the MathML3
> spec
> >> to explain how to translate the condition element is malformed?
> >>
> >
> > yes, it's certainly a very bad example to use to illustrate mapping
> to
> > strict or OM, as it leaves much unspecified. Nowhere does it state
> that
> > it's over the reals or, as you say, the direction of integration.
> > Now perhaps we want to say that integration defaults to the reals
> > which would be a reasonable thing to say but obviously that would be
> > specific to int and not something applicable to an arbitrary
> function.
> >
> all of these are true, but irrelevant to the discussion at hand. I am
> all for changing the example, we have too many integral examples as it
> stands. Maybe to the Lagrange base polynomial one below?
> > <bind>
> > <apply><csymbol>productcond</csymbol>
> >
> <apply><csymbol>integer_interval</csymbol><ci>0</ci><infty/></apply>
> > </apply>
> > <apply><ne/><ci>i</ci><ci>j</ci></apply>
> > <apply><divide/>...</apply>
> > </bind>
> >
> >
> > this is on the face of it shorter, but structurally it's far more
> > complicated, and frankly weird. using a constructed term as the
> binding
> > symbol is hardly an intuitive or natural construct. Actually I
> struggle
> > to read it at all. You have a bind without a bvar, presumably you
> > intended to bind i so there should be a <bvar><ci>k</ci></bvar>
> >
> Sorry about the missing bvar, it should actually be
> <bvar><ci>i</ci></bvar>
>
> OK, I agree that the complex binding constructor takes a bit getting
> used to, therefore I had added the alternative form. which you do not
> quote (this time with the bvar) here to focus the discussion:
>
> <bind>
> <csymbol>altproductcond</csymbol>
> <bvar><ci>k</ci></bvar>
> <apply><csymbol>integer_interval</csymbol><ci>0</ci><infty/></apply>
> <apply><ne/><ci>i</ci><ci>j</ci></apply>
> <apply><divide/>...</apply>
> </bind>
>
> > then you construct a complex binding operator by applying productcond
> > to a set, then use bind to apply that to two children, a predicate
> and
> > an expression (something that isn't allowed in OM2's OMBind or the
> > current draft of mathml's bind) This is structurally very obscure,
> > hard to read and incompatible with OM2 isn't it?
> >
> I am a bit frustrated here, did you even read the first e-mail and the
> proposal we made there?
>
> Let me re-iterate the tail of the original e-mail: We propose to
>
> > 1. to adopt the generalization to n-ary binding constructions in
> > OpenMath and strict MathML
> > 2. to extend the MathML CD group with the necessary xxxcond symbols
> > for the big operators
> > 3. to elaborate the p2s translation in the MathML3 spec to make use
> > of these.
>
> > In essence this proposal is to recognize the first-order
> representation
> > of MathML2 as valuable and give it a meaning rather than relegate it
> to
> > "pragmatic MathML" and translate it away.
>
>
> Making the extension to binding objects (generalizing both current
> MathML3 and OM3) is at the center of the proposal, and that is what I
> would like to talk about in this series of e-mails. And once you think
> about it a bit, this is structurally not sooo weird. <apply> allows an
> operator and an arbitrary list of arguments (unary, binary, ...
> operators), so <bind> could allow bvars and an arbitrary list of
> arguments (unary, binary, ... binding operators). It would in fact be
> more symmetric than the state we have now. And I think that the
> examples
> we have shown above show that this is quite natural --- but I agree a
> change from OM2, but one that is conservative, since all the OM2
> objects
> stay the same.
>
> > David has said in an earlier mail (quoting from memory) "I will
> oppose
> > any p2s translation that does not go via domainofapplication". And I
> > basically agree with this statement, since MathML2 said that all
> > qualifiers are special cases of <domainofapplication>. But I think
> that
> > our the representational style James and I propose is not in
> > contradiction to that. As the example above shows, and in all the
> > examples James and I looked at, the "condition" argument to the new
> > binary binding operators is just a domain of application expressed
> via a
> > bound variable shared with the binding scope.
>
> > James and I are currently working on the proposed CD extensions, but
> I
> > would have time to make the necessary changes in the spec in the
> coming
> > week. Since I am stalled until we have resolved this issue, I would
> like
> > to come to a conclusion soon.
>
> Let me re-iterate, I would like to come to a (positive) conclusion
> about
> this soon, so that I can continue working on the spec.
>
> Michael
>
>
>
> >
> >
> >> That is not something I can accept in a specification, I think that
> we
> >> should have a definite set of rules that assign meaning to full
> MathML
> >> expressions.
> >>
> >
> > If you have a set defined by restriction from some unspecified
> universal
> > set (which was the case here) then the expression has no meaning
> unless
> > you supply a universal set from somewhere. For int it may be
> reasonable
> > to assume the reals but in general this requires domain knowledge
> about
> > the function being encoded that we can't put in the spec. Because of
> the
> > nature of mathml qualifiers it's pretty much impossible to make such
> > constructs invalid mathml.
> >
> >
> >> If you agree in principle,
> >>
> >
> > No, this is just too weird.
> >
> > 3. translate all the qualifiers (except for condition) to
> > domainofapplication; in particular uplimit/lowlimit pairs into
> > intervals and apply the binding csymbol to it making a complex
> > binding symbol
> >
> >
> > using a complex binding operator makes the result incredibly hard to
> > understand and quite unlike any normal mathematical presentation,
> also
> > special casing condition causes equivalent expressions to be
> translated
> > differently. Also It requires a new symbol in each case, which means
> that
> > you can't translate a general symbol without inventing new Cds on the
> > fly to hold your xxxcond terms.
> >
> > min (x^2) as x ranges over |R is 0 and could be written as
> (abbreviated)
> >
> > <apply><min/>
> > <bvar><ci>x</ci></bvar>
> > <condition><apply><in/> x <reals/> </apply></condition>
> > <apply> x^2</apply>
> > </apply>
> >
> > or
> >
> > <apply><min/>
> > <bvar><ci>x</ci></bvar>
> > <domainofapplication> <reals/> </domainofapplication>
> > <apply> x^2</apply>
> > </apply>
> >
> > which are naturally (and explictly) equivalent formualtions.
> >
> > If I understand your 8 point plan, the first ends up as
> >
> > <bind><csymbol>mincond</csymbol>
> > <bvar><ci>x</ci></bvar>
> > <apply><csymbol>in</csymbol> <ci>x</ci><csymbol>reals</csymbol>
> </apply>
> > <apply> x^2</apply>
> > </bind>
> >
> > or perhaps you _have_ to construct a complex binding symbol by
> appying
> > mincond to some (inferred) domainofapplication? either way the result
> > doesn't look like the translation of the second form which is, I
> think
> >
> >
> > <bind>
> > <apply><csymbol>mincond</csymbol><csymbol>reals</csymbol></apply>
> > <bvar><ci>x</ci></bvar>
> > <csymbol>true</csymbol>
> > <apply> x^2</apply>
> > </bind>
> >
> > (using a condtion of true, but perhaps you'd instead use a different
> > symbol from mincond that constructed a binder that dodn't require a
> > condition, but that just increases the proliferation of generated
> names.
> >
> > David
> >
> >
> _______________________________________________________________________
> _
> > The Numerical Algorithms Group Ltd is a company registered in England
> > and Wales with company number 1249803. The registered office is:
> > Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.
> >
> > This e-mail has been scanned for all viruses by Star. The service is
> > powered by MessageLabs.
> >
> _______________________________________________________________________
> _
> >
>
> --
> ----------------------------------------------------------------------
> Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62
> Professor of Computer Science Campus Ring 12,
> School of Engineering & Science D-28759 Bremen, Germany
> Jacobs University Bremen* tel/fax: +49 421 200-3140/-493140
> m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase
> skype: m.kohlhase * on Sabbatical in Auckland (NZ) until VII/2009
> ----------------------------------------------------------------------
More information about the Om3
mailing list