[om] role of a symbol

[Paul Libbrecht]

David,

If I understand well, this CD isn't existing yet, or ?

Also, following the good OpenMath tradition, making these roles in CDs 
allows these descriptions to be extensible, and that's great! Or do I 
mistake ?

I wonder what shall be the types associated to roles symbols... that 
might be pretty hairy...

paul

On 30-Jan-04, at 01:20 Uhr, David Carlisle wrote:

>
>> I have read the new version of the standard, openmath2, and I am
>> still not sure how the "role of a symbol" is to be used.
>> Could anyone provide examples involving this?
>
> This version is still a draft and some of the detail may change (and at
> least the description should change if it is not clear) but the idea is
> that the role property is just essentially a formalisation of something
> that is implicit (or in some cases explicit in the sts files) in
> openmath 1.
>
> a symbol such as "times in arith1" is intented to be used as the head 
> of
> an application
> <OMA>
>   <OMS name="times" cd="arith1"/>
>  ....
> Symbols such as forall or lambda in suitable Cds are typically intended
> to be used not with OMA but rather with OMBIND to bind variables for
> quantification of function abstraction, respectively.
>
> A symbol such as "type" is intended to be used in neither of those
> positions but rather just as the key symbol in a symbol-value pair in 
> an
> openmath attribution, to attribute an object with a type.
>
> The idea of the Role property is that a CD should be able to formalise
> this role of a symbol (one possible benefit is that one can then
> automatically build restricted relax ng schema which restrict the
> symbols to these positions)
>
> Actually the current wording might be too restrictive (Something 
> Andreas
> spoke on at Bremen) while it is useful to be able to say a symbol is 
> intended
> to be used for application, you don't want to stop the symbol appearing
> in other positions to enable you to make statements about the symbol, 
> as
> in
> unit-of(times) = 1
> or something.
> It may be that role = "binder" should mean that the symbol should not
> appear as the head of an application or as an attribution key, but 
> could
> appear as the child of an application or omerror, so that statements 
> may
> be made, or errors reported on, the sysmbol.
>
> David
>
>
> -- 
> http://www.dcarlisle.demon.co.uk/matthew
> --
> om at openmath.org  -  general discussion on OpenMath
> Post public announcements to om-announce at openmath.org
> Automatic list maintenance software at majordomo at openmath.org
> Mail om-owner at openmath.org for assistance with any problems
--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems