[Om] Mathematical Vernacular in formulae

[Michael Kohlhase]

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