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
_______________________________________________
Om mailing list
[email protected]
http://openmath.org/mailman/listinfo/om
