Re: [Om3] Summary of the Davenport&Kohlhase Proposal

[Paul Libbrecht]

Michael, James,












paul


Le 23-mars-09 à 08:38, Michael Kohlhase a écrit :

although I still need to think about it, it appears acceptable to me. Three comments: - I would prefer to have a single child that would encapsulate all conditions; it would feel muuuuch safer (I guess a logic1#and would be enough in most cases and that is the semantic that is meant). - isn't there a systematic translation from the newer case to the older? I guess this is of interest for all. - can you tell more about possible dangers of this extension? I don't see any thus far but there must be some. - Do you really need extra symbols for that? (the new "allowed encodings" seem to be only invalid with the former encodings). I don't like arith7!

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


<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

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

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


now define more mathematical symbols and represent more objects.


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 ...

</CDDefinition>



<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>


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

is simple to define new symbols (probably in new CDs) that make the
representation in OpenMath simpler and more intuitive.


of OpenMath.

Michael

expression, and only i is bound. MathML2 would probably represent this as variables, whereas the original mathematical representation on Wikipedia only had one. Of course, we could have used i in the first one instead OpenMath binding objects by allowing more than one "argument": A binding So we are proposing a liberalization of OpenMath objects: all OpenMath2 objects are extended Objects and retain their original meanings. But can In our example, we would propose to develop a new CD (e.g. arith7; I do ... An FMP that defines this product, e.g. a recursive definition ... With this symbol, we can then represent the Lagrange Base Polynomical as Note that this is a very direct translation of the TeX representation of and retain their meaning). Moreover, as the example above has shown, it We should extend OpenMath to gain this freedom and extend the usability

-----Original Message-----
From: Michael Kohlhase [mailto:m.kohlh...@jacobs-university.de]
Sent: Wednesday, March 18, 2009 9:11 PM
To: David Carlisle
Cc: Robert Miner; j...@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

stands. Maybe to the Lagrange base polynomial one below?

all for changing the example, we have too many integral examples as it

<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

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.

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

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.kohlh...@jacobs-university.de http://kwarc.info/kohlhase
skype: m.kohlhase   * on Sabbatical in Auckland (NZ) until VII/2009
----------------------------------------------------------------------

_______________________________________________
Om3 mailing list
Om3@openmath.org
http://openmath.org/mailman/listinfo/om3

smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
Om3 mailing list
Om3@openmath.org
http://openmath.org/mailman/listinfo/om3