[Om] Mathematical Vernacular in formulae

[Kohlhase, Michael]

On 25.1.11 21:15, Professor James Davenport wrote:
> On Tue, January 25, 2011 5:59 pm, Lars Hellström wrote:
>> Professor James Davenport skrev 2011-01-25 17.42:
>>> On Tue, 25 Jan 2011, Lars Hellström wrote:
>>>> My gut feeling for the \text part is that this is an alternate markup
>>>> for
>>>> some combination of formal symbols, and should be encoded as such,
>>>> i.e., as
>>>> the value of some hypothetical altenc/vernacular symbol. Totally
>>>> ignoring the
>>>> cd's of symbols, that would make the \text part equivalent something
>>>> like:
>>> certainly nice if one can do it, but quite often one uses text becuase
>>> there aren't standard symbols for what one wants, I fear.
>> As long as some CD defines the symbol it should be OK. Or is your point
>> that OMDOC documents must be able to employ undefined concepts?
> The latter.
I am not sure, let's consider the situation for a moment.

For OMDoc (which integrates OpenMath into a document context), the situation is less a problem, we can always define a concept terminates-with in the same theory (in fact, the concept will usually defined somewhere if we use it. So we can allways use Lars' suggestion (or the last one in my original post in content MathML; they are equivalent up to beta-reduction). If need be, OMDoc can even hide the definition from being shown to the user in the document, so that we are always at liberty to add it.

My worry is more about OpenMath on its own, which (as a formula representation format) does not have access to such definitions, and needs content dictionaries. Lars is right in pointing this out. And there will usually not be a CD foo  whith a CDDefinition for the symbol <OMS name="terminates-for-with" cd="foo"/> around. [OMdoc has the luxury of "dynamic" CDs]

So maybe we can interpret the attribution

      <OMATP>
         <OMS cd="altenc" name="vernacular"/>
         <OMBIND>
           <OMS name="lambda"/>
           <OMBVAR>
             <OMV name="term1"/>  <OMV name="term2"/>  <OMV name="term3"/>
           </OMBVAR>
           <OMA><OMS name="concat-text"/>
             <OMV name="term1"/>  <OMSTR>  terminates for</OMSTR>
             <OMV name="term2"/>  <OMSTR>  with</OMSTR>  <OMV name="term3"/>
           </OMA>
         </OMBIND>
       </OMATP>
       <OMS name="terminates-for-with"/>
     </OMATP>

as an "inline CDDefinition" for

 <OMS name="terminates-for-with"/>

which legitimizes its use (I guess that I would use a different key symbol then). After all, many of the CNPs in our standard CDs do not say much more about the concept they define. Using this idea we could go even furhter and attribute a CDDefinition and a notation definition and have some thing like (embarrassing, I am in the train and cannot look up the CD notation; please forgive syntactical blunders)

<OMATTR>
<OMATP>
  <OMS cd="inlineCD" name="definition"/>
  <OMFOREIGN encoding="OMCD">
    <CDDefinition>
      <Name>terminates-for-with</Name>
      <CMP>
        Applied to three arguments P, a, and b, this expresses that
        procedure P terminates on input a with result b.
      </CMP>
    </CDDefinition>
  </OMFOREIGN>
  <OMS cd="inlineCD name="notation">
  <OMFOREIGN encoding="NTN">
    <notation>
      <prototype>
        <om:OMA>
          <om:OMS name="terminates-for-with"/>
          <expr name="proc"/>
     <expr name="arg"/>
     <expr name="result"/>
        </om:OMA>
      </prototype>
      <rendering class="vernacular">
        <m:mtext>
    <m:math><render name="proc"/></m:math>
          terminates on
          <m:math><render name="arg"/></m:math>
          with
          <m:math><render name="result"/></m:math>
       </m:mtext>
    </rendering>
  </notation>
</OMATP>
<OMA class="vernacular">
  <OMS name="terminates-for-with/>
  <OMV name="P"/>
  <OMV name="a"/>
  <OMV name="b"/>
</OMA>
</OMATTR>

In the presence of (an extension of) the NTN notation system this would give me the desired result. And even better, this would do so without taking recourse to using "lambda" and "concat-text".

Maybe something like this is a good way to go forward. The main question to be solved here is what the scope of the inline CDDefinition might be. Formally, I guess it cannot be much more than the current OMOBJ, But maybe OMR can help here.

>>>>        <OMS name="logical-and"/>
>>> By this do you mean the usual<OMS cd="logic1" name="and"/>
>>> or something else?
>> The usual "and", yes. (I simply didn't have the time to look up what
> Fine.
>> standard
>> CD defines it. Same thing with "set-in" and "lambda". I don't know how
>> well "concat-text" can be identified with anything standard.)
> Good question.
I think that the concat-text idea will not work too well, well actually concat-text is fine semantically, it is more the notion of using it with OMSTR  - which is a technical device for transporting strings in CASes rather than a container for natural language texts to make mixed markup (text + OMOBJ) that scares me. Recall that OpenMath does not have a built-in notion of evaluation (and that was a very good decision IMHO).
>>>>      </OMATTR>
>>>>      <OMA><OMS name="set-in"/>
>>>>        <OMV name="a"/>   <OMV name="T"/>
>>>>      </OMA>
>>>>      <OMA>
>>>>        <OMATTR>
>>>>          <OMATP>
>>>>            <OMS cd="altenc" name="vernacular"/>
>>>>            <OMBIND>
>>>>              <OMS name="lambda"/>
>>>>              <OMBVAR>
>>>>                <OMV name="term1"/>   <OMV name="term2"/>   <OMV
>>>> name="term3"/>
>>>>              </OMBVAR>
>>>>              <OMA><OMS name="concat-text"/>
>>>>                <OMV name="term1"/>   <OMSTR>   terminates for</OMSTR>
>>>>                <OMV name="term2"/>   <OMSTR>   with</OMSTR>   <OMV
>>>> name="term3"/>
>>>>              </OMA>
>>>>            </OMBIND>
>>>>          </OMATP>
>>>>          <OMS name="terminates-for-with"/>
>>> And this, of course, is a symbol we don't (currently) have.
>> But any author using the concept in an OM-enabled document ought to create
>> a definition of it if none already exists.
> If we knew what it meant - I didn't, and still don't.
I hope to have fixed this with the inline CDDefinition idea above.
>>>>        </OMATTR>
>>>>        <OMV name="P"/>
>>>>        <OMV name="a"/>
>>>>        <OMV name="b"/>
>>>>      </OMA>
>>>> </OMA>
>>>>
>>>> At least for the most common uses of text within math, namely logical
>>>> conjunctions, this should be the natural way to go as it allows tools
>>>> ignorant of natural language to process the formula.
> I absolutely agree that, WHERE it works, it has that, truly important
> advantage.
>
> James Davenport
> Lecturer on XX10190 and CM30070
> Hebron&  Medlock Professor of Information Technology, University of Bath
> OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
> IMU Committee on Electronic Information and Communication
> Council of the British Computer Society
> Federal Council, International Foundation for Computational Logic
>
> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://openmath.org/mailman/listinfo/om 
________________________________________
From: om-bounces at openmath.org [om-bounces at openmath.org] on behalf of Professor James Davenport [jhd at cs.bath.ac.uk]
Sent: Tuesday, January 25, 2011 8:15 AM
To: "Lars Hellström"
Cc: Professor James Davenport; om at openmath.org
Subject: Re: [Om] Mathematical Vernacular in formulae

On Tue, January 25, 2011 5:59 pm, Lars Hellström wrote:
> Professor James Davenport skrev 2011-01-25 17.42:
>> On Tue, 25 Jan 2011, Lars Hellström wrote:
>>> My gut feeling for the \text part is that this is an alternate markup
>>> for
>>> some combination of formal symbols, and should be encoded as such,
>>> i.e., as
>>> the value of some hypothetical altenc/vernacular symbol. Totally
>>> ignoring the
>>> cd's of symbols, that would make the \text part equivalent something
>>> like:
>> certainly nice if one can do it, but quite often one uses text becuase
>> there aren't standard symbols for what one wants, I fear.
>
> As long as some CD defines the symbol it should be OK. Or is your point
> that OMDOC documents must be able to employ undefined concepts?
The latter.

>>>       <OMS name="logical-and"/>
>> By this do you mean the usual<OMS cd="logic1" name="and"/>
>> or something else?
>
> The usual "and", yes. (I simply didn't have the time to look up what
Fine.
> standard
> CD defines it. Same thing with "set-in" and "lambda". I don't know how
> well "concat-text" can be identified with anything standard.)
Good question.
>>>     </OMATTR>
>>>     <OMA><OMS name="set-in"/>
>>>       <OMV name="a"/>  <OMV name="T"/>
>>>     </OMA>
>>>     <OMA>
>>>       <OMATTR>
>>>         <OMATP>
>>>           <OMS cd="altenc" name="vernacular"/>
>>>           <OMBIND>
>>>             <OMS name="lambda"/>
>>>             <OMBVAR>
>>>               <OMV name="term1"/>  <OMV name="term2"/>  <OMV
>>> name="term3"/>
>>>             </OMBVAR>
>>>             <OMA><OMS name="concat-text"/>
>>>               <OMV name="term1"/>  <OMSTR>  terminates for</OMSTR>
>>>               <OMV name="term2"/>  <OMSTR>  with</OMSTR>  <OMV
>>> name="term3"/>
>>>             </OMA>
>>>           </OMBIND>
>>>         </OMATP>
>>>         <OMS name="terminates-for-with"/>
>> And this, of course, is a symbol we don't (currently) have.
>
> But any author using the concept in an OM-enabled document ought to create
> a definition of it if none already exists.
If we knew what it meant - I didn't, and still don't.
>>>       </OMATTR>
>>>       <OMV name="P"/>
>>>       <OMV name="a"/>
>>>       <OMV name="b"/>
>>>     </OMA>
>>> </OMA>
>>>
>>> At least for the most common uses of text within math, namely logical
>>> conjunctions, this should be the natural way to go as it allows tools
>>> ignorant of natural language to process the formula.
I absolutely agree that, WHERE it works, it has that, truly important
advantage.

James Davenport
Lecturer on XX10190 and CM30070
Hebron & Medlock Professor of Information Technology, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
IMU Committee on Electronic Information and Communication
Council of the British Computer Society
Federal Council, International Foundation for Computational Logic

_______________________________________________
Om mailing list
Om at openmath.org
http://openmath.org/mailman/listinfo/om