[Om] Symbols for formal terms

[Lars Hellström]

I'm trying to understand how to represent formal terms (as needed for 
e.g. universal algebra) in OpenMath.

It seems clear that a term such as a+(b*c) should be encoded as 
something on the lines of

  <OMA>
    <OMS ...>
    <OMV name="a">
    <OMA>
      <OMS ...>
      <OMV name="b">
      <OMV name="c">
    </OMA>
  </OMA>

with the OMS elements being suitable symbols for addition and 
multiplication, but I've had some trouble finding such symbols in any 
existing content dictionary.

My first idea was to look in the algebra-related content dictionaries. 
For example ring1 contains symbols "multiplication", "addition", 
"negation", "zero", and "identity" which sound right, but their 
signatures are wrong: functions which return operations when applied to 
a ring, rather than (formal names for) the operations themselves. This 
is probably convenient for communication of concrete elements between 
two parties which share a terminology for describing the ring, but 
that's not the situation I'm interested in right now; also it would be 
overly restrictive to always require a machine-readable description of 
one's algebraic structures.

Violating the signatures of these symbols does not seem like a good 
idea either. Furthermore the fact that there are separate 
"multiplication" symbols in "magma1", "semigroup1", "monoid1", 
"group1", "ring1", and "field1" is another reason not to use them for 
this -- it's probably the same operation regardless of how one views 
the actual structure, so one wouldn't want to encourage the use of 
separate symbols.

But mostly by accident, I noticed that these content dictionaries also 
contain an "expression" symbol denoting the function which effectively 
evaluates a formal term within a specified algebraic structure. Since 
these formal terms make use of symbols in the "arith1" and "alg1" 
dictionaries to denote the operations, I have thus concluded that the 
established way to express the formal term a+(b*c) in OpenMath would be

  <OMA>
    <OMS cd="arith1" name="plus">
    <OMV name="a">
    <OMA>
      <OMS cd="arith1" name="times">
      <OMV name="b">
      <OMV name="c">
    </OMA>
  </OMA>

While this is workable (for now), I'm still not entirely happy with it:

1. The CD name "arith1", and also the presence in it of symbols such as 
"lcm", very much suggests that it is intended for operations on 
numbers, which is rather far from the universal algebra point of view.

2. The name "times" sounds wrong to me (suggesting \times, where I 
rather think of general multiplication as \cdot), but this could be a 
language thing.

3. More seriously, the arith1 "times" symbol is formally declared to be 
associative, which prevents using it for nonassociative rings (e.g. Lie 
algebras). A similar issue exists with the "plus" (associative and 
commutative) and "unary_minus" (inverse for "plus") symbols, although 
I'm personally less likely to be troubled by the latter.

4. There is no distinction between general multiplication and the 
scalar multiple operation (or operations: left and right). 
Syntactically these are very different, and assuming the scalar 
multiples to be special cases of general multiplication is the same as 
assuming that there is a multiplicative unit.

In view of this, I'm beginning to suspect that I will eventually have 
to create a content dictionary of my own for this, but I thought I 
should first check with your lot if there's something I've overlooked.

Lars Hellström