[Om3] Summary of the Davenport&Kohlhase Proposal
Paul Libbrecht
paul at activemath.org
Mon Mar 23 08:58:59 CET 2009
Michael, James,
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!
paul
Le 23-mars-09 à 08:38, Michael Kohlhase a écrit :
> 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
>> ----------------------------------------------------------------------
>
> _______________________________________________
> Om3 mailing list
> Om3 at openmath.org
> http://openmath.org/mailman/listinfo/om3
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2203 bytes
Desc: not available
Url : http://openmath.org/pipermail/om3/attachments/20090323/6d4b0f3b/attachment.bin
More information about the Om3
mailing list