[Om] Multistep "equation" symbol?

Professor James Davenport jhd at cs.bath.ac.uk
Mon May 11 15:55:04 CEST 2009


On Mon, May 11, 2009 2:37 pm, Lars Hellström wrote:
> Is there an established OM symbol for "multistep equations" (see
> example below)? If not, would it make sense as part of some official
> content dictionary?
There isn't in OpenMath, but OMDoc may well have thoughts on this - Michael?
The reason I say that is what you have is really a (part of) a proof here,
especially when one looks at the annotations.

>   * There are several steps in this thing, yet it constitutes
>     a natural unit (in whatever document it is part of).
Quite. It is a 'proof' and could be a free-standing Lemma. One might not
wish to do so for expositional reasons, but a proof ought to be capable fo
eing a chain of sub-proofs.
>   * Not all steps employ the same relation.
True, but, and this is the hard part to formalise, they must be "logically
compatible".
>   * Some instances of a relation carry remarks explaining why
>     that step holds.
Again, OMDoc comes to mind.
> Partially transformed into OM, this might become
>
> <OMA><OMS name="multistep">
>    <OMFOREIGN encoding="LaTeX">
>      \sqrt{n^2+1} - n
>    </OMFOREIGN>
>    <OMS cd="relation1" name="eq"/>
>    <OMFOREIGN encoding="LaTeX">
>      n \left( \frac{1}{n}\sqrt{n^2+1} - 1 \right)
>    </OMFOREIGN>
>    <OMS cd="relation1" name="eq"/>
>    <OMFOREIGN encoding="LaTeX">
>      n \left( \sqrt{ 1 + \frac{1}{n^2} } - 1 \right)
>    </OMFOREIGN>
>    <OMATTR>
>      <OMATP>
>        <OMS name="because">
>        <OMFOREIGN encoding="LaTeX">
>          \sqrt{1+x} \leq 1 + x/2 </OMFOREIGN>
>      </OMATP>
>      <OMS cd="relation1" name="leq"/>
>    </OMATTR>
>    <OMFOREIGN encoding="LaTeX">
>      n \left( 1 + \frac{1}{2n^2}  - 1 \right)
>    </OMFOREIGN>
>    <OMS cd="relation1" name="eq"/>
>    <OMFOREIGN encoding="LaTeX">
>      \frac{1}{2n}
>    </OMFOREIGN>
>    <OMS cd="limit1" name="tendsto"/> <!-- Not quite right? -->
>    <OMS cd="alg1" name="zero"/>
> </OMA>
>
> where an expression
>
> <OMA><OMS name="multistep">
>    x0 R1 x1 R2 x2 ... Rn xn
> </OMA>
>
> is equivalent to
>
> <OMA><OMS cd="logic1" name="and"/>
>    <OMA> R1 x0 x1 </OMA>
>    <OMA> R2 x1 x2 </OMA>
>    ...
>    <OMA> Rn xn-1 xn </OMA>
> </OMA>
>
>
> Now, I suppose it could be argued that such a "multistep" symbol is
> unnecessary because of this equivalence -- I think there has been a
> similar argument that the elementary relation symbols should not be
> n-ary as the binary forms together with logic1#and suffice for
Indeed, I led that charge, and would continue to have the same views.
But the case is different here: you WANT to mix the symbols.
As you said, what you have is a proof, which is why I'd rather Michael
commented.
> expressing the same thing -- but my gut feeling is that this
> "multistep" is more than a mere conjunction of statements, even if that
> is exactly what it amounts to as far as logic is concerned. It might be
> that I'm letting concerns for presentation affect me -- my primary
> use-case is indeed to export derivations from the program that
> discovered them to another that will generate a presentation -- but it
> seems rather onerous to request from a presentation generator that it
> will reconstruct the underlying "multistep equation" from a logic1#and
> expression such as the above. Deciding what to combine and what not to
> combine is a delicate problem, which I'd rather not delegate to
> unqualified software or personnel.
>
> Lars Hellström
>
>
> PS: While typing up the example, I noticed that it probably wouldn't be
> correct since limit1#tendsto (MathML3-ish?) is defined to be ternary,
> requesting a type-of-limit as first argument. While I suppose one could
> use a lambda to work around that, I can't help wondering why the limit
> type is an argument in the first place; wouldn't an attribution be more
> appropriate?
I expect becaus eof the 'optionality' of attributes, at least in OM1.

James Davenport
Visiting Full Professor, University of Waterloo
Otherwise:
Hebron & Medlock Professor of Information Technology and
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
IMU Committee on Electronic Information and Communication



More information about the Om mailing list