A Better Role System for OpenMath
OpenMath is a standard for the representation and communication of mathematical objects,
which are built up from symbols and variables using applications, binding expressions,
and key-value attributions. OpenMath2 introduced a set of symbol roles that can be
specified in content dictionaries to restrict the occurrences of the respective
symbols. This yields a simple, high-level notion of well-formed objects.
While this system is appealing in its simplicity, the definition of well-formedness is
purely extensional without an intuitive or formal condition that distinguishes
well-formed objects from ill-formed ones. Moreover, some well-formed objects should arguably rather be ill-formed. We try to remedy that with a refined role
system while preserving the simplicity of the existing one. In particular, by
distinguishing syntactic and semantic roles, we can capture the intuitive notion of
well-formedness better.

