[Om] Multistep "equation" symbol?

[Professor James Davenport]

On Wed, May 13, 2009 12:39 am, Michael Kohlhase wrote:
> 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:
>>> 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{
>       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.
One can even have formalised reasons inside a CD - see logic3 for this.
Michael asks a good question, which I might rephrase as "which side of the
OpenMath OMDoc boundary are you interested in"?
> 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.
We've had this problem before, and maybe the time is coming to have this
debate more formally, maybe in a business session/panel at OM2009?
> 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>
Isn't this a (somewhat perverse) nassoc operator?
> 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.

James Davenport
Visiting Full Professor, University of Waterloo
Otherwise:
Hebron & Medlock Professor of Information Technology and
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
IMU Committee on Electronic Information and Communication