[Om] Multistep "equation" symbol?
Lars Hellström
Lars.Hellstrom at residenset.net
Mon May 11 15:37:38 CEST 2009
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?
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?
More information about the Om
mailing list