[Om] Symbols for formal terms

Lars Hellström Lars.Hellstrom at residenset.net
Sun Oct 12 23:09:34 CEST 2008

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