[Om] Multistep "equation" symbol?

[Michael Kohlhase]

On 14.05.2009 0:03 Uhr, Professor James Davenport wrote:
> 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.
>    
Ah, I was unaware of logic3, I will have to have a look at that. And of 
course, this corresponds very much to what we are using in OMDoc as 
"proof terms" via the Curry/Howard Isomorphism (CHI). And indeed using 
the CHI, one could  interpret the equations as Proof terms (embedded 
into) mathematical discourse in general. As I said, I will have to think 
about an example here.
> 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?
>    
I am not sure that the business section would be the right spot, but I 
think we may have to make a panel for open issues, which this certainly 
is. Given that I have been thinking about the "semantics of OpenMath", 
we also have to talk about the "linguistics of OpenMath", I think. It 
seems to me that formulae in mathematical texts are used and have a 
meaning on two levels (which is something we see in linguistics):

   1. the "compositional" level (I do not have a good word for this, so
      I will try this). Here we have the formulae as interpreted
      objects, where we cannot look into them (therefore the word
      compositional, since there the meaning of a complex object is only
      determined by the meanings of the operator and arguments). The
      compositional meaning of 2+3 _is_ 5 (as an indivisible
      mathematical object).
   2. the "representational" level, where an object is just a formula
      (tree) i.e. (almost) an OpenMath Object. Here we can talk about
      subterms (and names of bound variables in fact). This level is
      also used in Math, we can point to subformulae (that are
      inaccesible at the compositional level): e.g. in "... note that
      the second argument of the left hand side of the equation above is
      not in standard form, so..."

I think that in a "discourse theory of mathematics" (as I am attempting 
to make in OMDoc) this  is an important thing to understand. And I think 
that it may be important for OM as well.

OK, I hope you are not too bored at my attempts of philosophy.

Michael

But I am not sure what to
>> 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
>
>    

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