[Om] Multistep "equation" symbol?

[Lars Hellström]

Michael Kohlhase skrev:
> Sorry for my late entry into this discussion and keeping you waiting.

Well, right now I'm probably about 2 days behind myself...

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

The example was chosen to be immediately familiar to all. In the 
situation where I'd like to use the "multistep" symbol, it is most 
definitely a "mathematical object" (e.g. there exist specific 
operations on it) which I want to "exchange between software systems", 
so this /should/ be a job for OM (cf. the omstd20 abstract).

OMDoc looks like it could be an /output/ format for the presentation 
generator I wrote about, but I'd rather have its overall input format 
be OM.

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

Think of the information attached using \stackrel as a *certificate* 
for that relation step; if it makes sense to attribute OM objects with 
their automorphism groups, then surely it would also make sense to 
attribute OM objects with relevant certificates? (A software system 
would probably prefer something more worked out than \sqrt{1+x} \leq 1 
+ x/2 as certificate, but chalk that down to the example being a tad 
informal.)

And yes, operations on "multistep" objects would (in the case where I'd 
like to employ them) also need to update the embedded certificates. 
(Implementing the basic operations on the certificates is one thing on 
my todo-list.)

> 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 

Is that such a strong connotation? It is my impression that there can 
be steps which aren't directly tied to a proof -- for example the steps 
of a calculation (although I suppose one could argue that any 
calculation written out in detail is a proof) -- but "multirel" is an 
acceptable name too (although possibly a bit tautologous if it was to 
come from some "relation" CD).

By the way, the concept of calculation steps suggests a generic 
application for a "multistep" symbol: report all the steps of a 
calculation. A CAS could support one operation "evaluate this" and 
another operation "evaluate this, and tell me how you did it" where the 
second could return a multistep object. For exact arithmetric all steps 
would be with relation1#eq as relation, but in fixed point arithmetic 
some steps would be relation1#eq and others relation1#approx, and in 
interval arithmetic I suppose the typical relation would rather be 
set1#subset.

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

Indeed. Maybe I didn't write it, but I certainly intended that the 
equivalence of the "multistep" and the conjunction of per-relation-OMAs 
should be a FMP. (Also I've been thinking about whether one should 
allow for other "and"s than logic1#and, but I don't have a use-case for 
that so it's probably overkill.)

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

Bummer! Could one perhaps work around it by way of lists, though? 
Hmm... there doesn't seem to be any symbol in the listN CDs which 
constructs an OMA out of a list of children, and it seems without that 
we're pretty much stuck.

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

It seems like a nice starting exercise, compared to some other CDs I'll 
need to create (those being subjects for other threads, still to come). 
I'd really like to provide an attribution (which I called "because", 
but would probably look nicer in the XML if called "since") as well.

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

Representational overhead is probably OK, but the above is not a 
particularly natural representation of the concept.

The basic problem is really the same as that one faces when saying that 
n-ary plus is a repetition of binary plus, which ought to be possible 
to state as a FMP. Binary plus is of course in principle all one needs, 
but n-ary plus is a much closer match to general linear combinations, 
and therefore to most algebraic structures employing a plus.

Lars Hellström

> 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