[Om] Multistep "equation" symbol?

[Michael Kohlhase]

Sorry for my late entry into this discussion and keeping you waiting.

On 12.05.2009 9:22 Uhr, Lars Hellström wrote:
> 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.
>    
Here I have to say that I am not quite sure of the intent of the new 
symbol here (and your first example muddies the water). I see two 
possible ways of dealing with this

   1. we view this as a proof, your first example with

          \stackrel{
            \text{(since \(\sqrt{1+x} \leq 1 + x/2\))}
          }{\leq}
           

      seems to suggest that, then you need a language (e.g. in OMDoc)
      with proof markup. Then  I think that Alberto got things right,
      and that would be the wayI would also deal with this.
   2. But I think that Lars wants something with only relations, i.e. 
      without the stackrel in the example. Then I think that we can just
      introduce a CD for this purpose. That is exactly in tune with the
      OpenMath philosophy.

So coming back to what I perceive Lars' original proposal (i.e. 2.): I 
agree with Lars, that we want to have one (orp possibly more) multi??? 
symbols for that I would probably call the one proposed by Lars 
"multirel" though in order to avoid the connotations of proof steps that 
I think have to be treated at a different level. I very much agre with 
the sentiment that the equivalent conjunction is different at a 
representational level and should be represented differently.

What needs to be done is to formulate a CD and propose it to the OM 
Society for inclusion. Here is what I would do: Propose a CD (relation5 
maybe) and add a single CDDefinition in it. Crucially, we should have a 
FMP that explains it: Let me say this in mockOM (where @ stands for OMA)

@(M,a_0,R_1,a_1,R_2\ldots,R_n,a_n) = @(and,@(R_1,a_0,a_1), 
@(M,a_1,R_2\ldots,R_n,a_n))

Now, this already points to a problem in OpenMath, we can _informally_ 
say this in a CMP, but not formally in a FMP, since OM does not have a 
concept of sequence variables (or meta-level elision) that can be 
quantified over.

But FMPs are not mandatory, so we can just skate around this issue with 
a CMP. @LARS, if you are interested in proposing such a CD, I would be 
glad to help.

Another thing that just popped up that would allow us to solve the 
formality problem (if you are prepared to accept the representational 
overhead). We could use Currying at the representational level and express
@(M,a_0,R_1,a_1,R_2\ldots,R_n,a_n) as
@(N,
      a_0,
      R_1,
      @(N,
            a_1,
            R_2,\ldots,
                    @(N,R_n,a_n)\ldots).

Or concretely in OM:  $a<b=c$ as

<OMA>
<OMS cd="relation5" name="nrel"/>
<OMV name="a"/>
<OMS cd="relation1" name="lt"/>
<OMA>
<OMS cd="relation5" name="nrel"/>
<OMV name="b"/>
<OMS cd="relation1" name="eq"/>
<OMV name="c"/>
</OMA>
</OMA>
</OMA>

then we could put use the following FMPs:
@(N,a,R,b) = @(R,a,b)
@(N,a,@(N,b,R,C)) = @(and,@(R,a,b), @(N,b,R,C))

But of course that is a matter of taste as well. Again, I would be happy 
to develop this further, as this seems to address a general problem in 
OpenMath.

Michael
-- 

----------------------------------------------------------------------
  Prof. Dr. Michael Kohlhase,       Office: Research 1, Room 62
  Professor of Computer Science     Campus Ring 12,
  School of Engineering&  Science   D-28759 Bremen, Germany
  Jacobs University Bremen*         tel/fax: +49 421 200-3140/-493140
  m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase
  skype: m.kohlhase   * on Sabbatical in Auckland (NZ) until VII/2009
----------------------------------------------------------------------