[Om] Mathematical Vernacular in formulae

[Lars Hellström]

Michael Kohlhase skrev 2011-01-25 08.46:
> Dear all,
>
> Here is an issue that has been bothering me for a while. I am asking you
> for your advice.
[snip]
> In mathematical texts we often find constructions
> that have natural language _inside_ mathematical formulae. For instance,
> I found (using TeX for simplicity; what a pity we cannot use MathML in
> e-mails yet)

In this discussion, it might actually be an advantage ;-)

> $\{\langle a,b\rangle\bigl|\text{$a\in T$ and $P$ terminates for $a$ with $b$}\}$
>
> There are multiple other examples and you have probably seen many of
> them. But how do we mark this up in OpenMath (should we at all?).

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:

<OMA>
   <OMATTR>
     <OMATP>
       <OMS cd="altenc" name="vernacular"/>
       <OMBIND>
         <OMS name="lambda"/>
         <OMBVAR> <OMV name="Clause1"/> <OMV name="Clause2"/> </OMBVAR>
         <OMA><OMS name="concat-text"/>
           <OMV name="Clause1"/> <OMSTR> and </OMSTR> <OMV name="Clause2"/>
         </OMA>
       </OMBIND>
     </OMATP>
     <OMS name="logical-and"/>
   </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"/>
     </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.

Lars Hellström