[om] role of a symbol

[Michael Kohlhase]

Paul,


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

Of course there will be OM2 versions of the core OpenMath CDs that will 
have the necessary role attributes.

> 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...

Types for these symbols is a totally orthogonal question to the role 
discussion. Since OM does not prescribe a type system, you are free to 
build one. For symbols of role binder, this is a relatively simple thing 
(with obvious ideas coming from Higher-Order Abstract Syntax and Type 
Theory). Same thing for role="annotation" and role="semantic-annotation" 
(I have references, if you are interested).

I seem to recall that a  type system for Errors has been investigated 
previously in the theory of programming languages, and STS has some 
types there already. It would be interesting to look at this in more 
detail.

Michael
--
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