On Mon, May 11, 2009 at 03:37:38PM +0200, 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?
Yes, in the CDs I once wrote for RIACA http://www.win.tue.nl/~amc/oz/om/cds/relation4.xml These were once available via www.openmath.org but I do not kinow the current situation. Best regards, Arjeh > The situation I'm thinking about is that of expressing something like > the following LaTeX fragment: > > \sqrt{n^2+1} - n > = > n \left( \frac{1}{n}\sqrt{n^2+1} - 1 \right) > = > n \left( \sqrt{ 1 + \frac{1}{n^2} } - 1 \right) > \stackrel{ > \text{(since \(\sqrt{1+x} \leq 1 + x/2\))} > }{\leq} > n \left( 1 + \frac{1}{2n^2} - 1 \right) > = > \frac{1}{2n} > \to > 0 > > (This is not my motivating example -- that would instead be the > derivation of a rewrite rule from given axioms -- but this has the > advantage of being immediately familiar.) Points to note are: > > * There are several steps in this thing, yet it constitutes > a natural unit (in whatever document it is part of). > > * Not all steps employ the same relation. > > * Some instances of a relation carry remarks explaining why > that step holds. > > 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 > 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? > _______________________________________________ > Om mailing list > [email protected] > http://openmath.org/mailman/listinfo/om _______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
