[om] role of a symbol

[David Carlisle]

> 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