Re: Content MathML 3 in new working draft

Dear Thomas,

sorry for the very long silence, this fell off my stack, I hope that 
this is still relevant to your interests.

Thomas E. Leathrum wrote:
>
> Michael Kohlhase wrote:
>>> 1)  Will there be a precise decision procedure for deciding whether to
>>> use "apply" or "bind"?  Do you use "bind" whenever there is a "bvar",
>>> or is there a fixed set of operators (e.g. "int," "forall")  that will
>>> require "bind"?      
>> Here we have to distinguish "strict CMathML" vs "pragmatic CMathML". The
>> former has a clear structure and a direct semantics on form of OpenMath
>> Objects. The latter has a much freer structure, and covers (almost) all
>> of what was legal in MathML2; its semantics is given in form of a
>> translation to strict CMathML. In strict CMathML, <bvar> is  not allowed
>> in an <apply>, and so <bind> has to be used. In pragmatic CMathML <bvar>
>> in <apply> is allowed in some cases; the expressions in question
>> correspond to <bind> expressions in strict CMathML.
>>   
> Yes, the question really is meant to apply to strict CMML3.  And OK, 
> yes, I had gathered that  "bvar" would imply "bind".  So I guess my 
> question really has to do with the converse:  are there going to be 
> cases where you will have to use "bind" in the absence of a "bvar", 
> because of the symbol role for the operator specified in the content 
> dictionary?
No, there will not be such cases, as <bvar> is mandatory in <bind>. Do 
you have any symbols in mind that you worry about?
>> The union example you are referring to here is a (little documented)
>> feature of MathML2, where we can use the <union/> symbol with two
>> roles.  But MathML2 also divides the functionally analogous situation
>> for addition and multiplication into distince symbols: <add/> and <sum/>
>> (and <times/> and <prod/> respectively). In strict CMathML we have
>> decided that we will always separate the operators into "small" and
>> "big" operators (following TeX nomenclature). So there should not be
>> much confusion.
>>   
> That will help, but that seems to be pointing in the direction of 
> having a set of operators that require "bind" regardless of whether 
> there is a "bvar" present.
No, the situation will be the that we will have

a binding symbol (i.e. role binding) big_union
a function symbol (i.e. role application) union.

big_union has to be used in <bind> with mandatory <bvar>
union has to be used in <apply> without <bvar>

>>> 2) Will the "pragmatic" form of CMML3 ultimately be deprecated in
>>> favor of the more verbose "canonical" form?      
>> No, it will not. The two variants serve distinct and legitimate
>> purposes. We consciously changed the names "canonical/legacy" to
>> "strict/pragmatic" to make this clear. Strict CMathML is more suited for
>> machine processing, whereas  Pragmatic CMathML is more geared towards
>> human readability and authorability. So in your case, I indeed guess
>> that pCMathML is more suitable.
>>  
>>> For my software, the "pragmatic" form would be the more realistic way
>>> to handle the source syntax for the translator, but I could add some
>>> code (or some sort of external association similar to the content
>>> dictionaries) to make sure the output is "canonical."      
>> Rather than restricting to strict CMathML as an output format I would
>> probably add a switch that allows to generate the respective variant.
>>   
> Given that my translator uses a mostly syntactic method of going from 
> its input source to CMML2 output, there is very little reference to 
> particular identifiers, so the translator as it stands now should work 
> for "pragmatic" CMML3.  So what I really need to work on is a 
> translator configuration for "strict" CMML3.  In order to continue 
> using ordinary identifiers rather than "csymbol" references to the 
> content dictionaries, though, I will need to put together some sort of 
> external association between the two, akin to the content dictionaries.
We have made some progress on the content dictionaries, you can find 
them at http://svn.openmath.org/OpenMath3/cds/MathML, there we (will) 
have a description about the pragmatic to strict mapping. We also plan a 
style sheet that does the mapping.
>>> However, relevant to the first question, the pragmatic form uses
>>> "apply" as in CMML2 in places where the canonical form would require
>>> "bind," which for my purposes just muddies the waters even more.
>>>     
>> I personally do not think that this is a problem, but maybe you would
>> care to elaborate.
>>   
> I suppose the problem would depend on whether there will be a clear 
> distinction in the mark-up between when you are using "pragmatic" or 
> "strict", the way there currently is for the distinction between 
> "presentation" and "content" (they *can* be mixed, but only by 
> enclosing the mixed code inside e.g. "semantics" tags).  If there is 
> no such clear distinction, you could have a segment of "pragmatic" 
> code with its "apply" tags inside a segment of "strict" code with its 
> "bind" tags, and the difference specified by the symbols and their 
> roles would become rather meaningless.
We are not currently thinking about a strict/pragmatic distinction 
moderated by elements. The idea is that both are proper content MathML3 
and can therefore be mixed. As pragmatic content MathML obtains its 
meaning from its translation to strict CMathML, they can be mixed, since 
there is always a strict equivalent.

I hope this helps,

Michael
>
>
> Regards,
> Tom Leathrum
>
>

-- 
----------------------------------------------------------------------
 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@jacobs-university.de http://kwarc.info/kohlhase 
 skype: m.kohlhase   * International University Bremen until Feb. 2007
----------------------------------------------------------------------

Received on Sunday, 17 February 2008 12:17:40 UTC