[Om] Multistep "equation" symbol?

[Lars Hellström]

Professor James Davenport skrev:
> 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?

Awaiting input from that side of things, then.

> The reason I say that is what you have is really a (part of) a proof here,
> especially when one looks at the annotations.

Indeed, or at least the skeleton of (part of) a proof. In my case the 
annotations would mainly specify which identity is applied and where 
(which is not at all obvious -- especially for derivations that employ 
previously derived rules).

>>   * 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".

Well, I don't see much point in formalising that; it must in the end be 
up to the party who constructs this kind of proof to draw some logical 
conclusion from it. Attempts to construct a syntactic description of 
the cases where this is possible are likely to be futile.

>>   * 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.

After a bit more though: This is not so much about presentation, as it 
is about exposition. (Vague, but probably true.)

>> 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.

Aha!


Lars Hellström