[Om3] On 'restricting bound variables' in Basic OpenMath

Michael Kohlhase m.kohlhase at jacobs-university.de
Thu Nov 6 08:37:00 CET 2008



Chris Rowley wrote:
> James wrote --
>
>   
>>> More formally, we need complete information about the content for
>>> <OMC>: is it any valid OpenMath expression?  Thanks!
>>>       
>> I think Michael is expecting it to be a Boolean-valued expression in the 
>> lose sense: since OM is not a CA system, we can't ask much more. 
>>     
>
> But can we even ask this without a 'Boolean type' in Basic Openmath?
>   
We do have the "Boolean CDs" logic1 and quant1 though, which supply much
of the functionality at the CD level. I think OpenMath should stay with
the structural properties of mathematical langauge and it is arguable
whehter the existance of a Boolean type is one of them. It seems that
the discussion has moved away from having one; for instance MathML1 had
the <rel> variant of <apply> that was used for applying predicates. It
is now one of the few deprecated elements of MathML.
>>> My problem is that the 'number of variables' seems to be irrelevant to
>>> a mathematician.  Two Reals is just one element of R^2 so a single
>>>       
>> I disagree. It is irrelevant IN PRINCIPLE, but in practice (and if we want 
>> to be reasonably close to "the mathematical vernacular") it does matter.
>>     
>
> Agreed; my point is that the somewhat arbitrary(??) restrictions on
> typing to 'one variable' seem irrelevant from a mathematical viewpoint.
>
>   
They are actually relevant for mathematical (structural) practice I think.

Michael
> chris
>
> _______________________________________________
> Om3 mailing list
> Om3 at openmath.org
> http://openmath.org/mailman/listinfo/om3
>   

-- 
----------------------------------------------------------------------
 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   * International University Bremen until Feb. 2007
----------------------------------------------------------------------



More information about the Om3 mailing list