[Om] Multistep "equation" symbol?

[Bruce Miller]

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?

When I've asked such questions in the past,
I generally got James' (essentially correct) response,
that it is equivalent to a conjunction of relations.

I shared your concern that such a multi-something
is easily converted to the conjunction form, but
less reliably converted back.  Perhaps <OMR> would be
useful here?
<OMA>
   <OMS cd="relation1" name="eq"/>
   <OMV name="a"/>
   <OMwhatever id="rhs1"/>
</OMA>

<OMA>
   <OMS cd="relation1" name="eq"/>
   <OMR xref="rhs1"/>
   <OMwhatever id="rhs2"/>
</OMA>
...

While the issue is mainly about a short-hand
that you don't want to loose, there are,
I think, some subtle semantics sneaking around
behind such a common notation.

As James points out, your case seems to
be sort of a proof, or derivation. Each
rhs follows from, can be derived from, is implied
by, is the asymptotic expansion of, ...
it's associated rhs.  The set of
relation(-like) operators, and their sensible
sequences is tricky, and in general there isn't
a trivial transitivity.

The same notation is used as, eg. a < b = c <= d << e,
where there is (seemingly) less hidden semantic,
just a shorthand.

I suspect there are cases where there other
hidden semantics.

My main point being, if one _were_ to define
such a symbol, it would seem that more than one
"Multi<something>" would be called for.

> 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
> Om at openmath.org
> http://openmath.org/mailman/listinfo/om


-- 
bruce.miller at nist.gov
http://math.nist.gov/~BMiller/