[Om] Symbols for formal terms

[Professor James Davenport]

On Sun, October 12, 2008 10:09 pm, Lars Hellström wrote:
> I'm trying to understand how to represent formal terms (as needed for
> e.g. universal algebra) in OpenMath.
A good question.
> 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
I don't understand the difference. The formal expressions you refer to
still constitute a ring, with the result of applying '+' to '1' and '1'
being '1+1'. So if you purely want to do universal algebra, I don't see a
problem. Where I do see a problem (and one that I face myself, totally
outside the OM/MathML world, when lecturing on computer algebra) is when
you want to talk about interpretations of abstract algebra, and say that
"the normal integers" are an instance of the one-sorted algebra
<<0,1>,<->,<+,*>>. But is this any different from any other description of
homomorphisms?
> 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.
Surely, if we are in this world, we need SOME machine readable
description, but it need only be
<OMS name="abstract_ring" cd="lars_world" cdbase="..."/>
Indeed, as you evolve this theory, this symbol might evolve FMPs etc. later.

James Davenport
Hebron & Medlock Professor of Information Technology
Formerly RAE Coordinator and Undergraduate Director of Studies, CS Dept
Lecturer on CM30070, 30078, 50209, 50123, 50199
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor
IMU Committee on Electronic Information and Communication