[om] more comments on CDs

[Michael Kohlhase]

> I think I agree with David that we don't have any notion of
> "constructor" in OpenMath, certainly not in the sense that a language
> like Java has.  What is the constructor of the expression "a+x", is it
> plus?



There is precise (related) sense in which the word "constructor" is used:
in the theory of abstract (inductive) data types. We say that a set is
inductively defined, if it (only) contains elements that can be built up
from "constructors", i.e. certain special constants. The canonical example
are the natural numbers: they are built up from the constructors 0 and s
(for successor). In this definition, the notion of a constructor is tied to
a set (also called sort sometimes); in our case Nat, and does not really
make sense otherwise. Usually two additional requirements for constructors
and sorts:

- [generated; "no junk"] The sort only contains elements that are built up
  from the constructors.
- [free; "no confusion"] There are no non-trivial identitiies among the
  elements of the sort, i.e. two elements are equal, iff they are built up
  from the constructors in the same way. 

An example of a non-generated sort, is "Nat plus infinity" (unless you
count infinity as another constructor). An example of a non-free sort is
the set of positive rational numbers. It is generated from 0,s,/ (no junk
to worry about), but there are non-trivial identities, e.g. 2/4=1/2, so it
is not free. The significance of free, generated sorts (also called
abstract data types) is that for every n-ary constructor, there are n
so-called "selectors" (partial inverses; the predecessor function p is the
selector for the successor function s on the Nat). I think that the
selectors are the functions that Arjeh is looking for.  

Maybe, we can take the theory of abstract data types (which is
well-understood and a basis for the field of algebraic specification) as a
basis for our discussion. This does not mean that we need to explicitly
support that in content dictionaries; but it would help to keep this in
mind. 

In summary: it does not make sense to search for selectors on the generated
but non-free sort of rational numbers, since the "no-confuion" restriction
is not met. Of course a less naive treatment of rational numbers (e.g. by
standardizing on inter-reduced representations; which would make /
NON-CONSTRUCTOR) would allow partial inverses to /.

> As far as "rational(4,6)" goes the STS signature is (Z x Z/{0}) -> Q and
> there are no side conditions specified in the CD so I think that it is
> allowed.  We cannot define rational more tightly because we have to be
> compatible with the MathML definition.
> 
> While we probably all agree what the normal form of the rationals is, in
> many cases this won't be the case.  Whether an algebra system stores
> "a+x" (as Maple) or "x+a" (as Axiom, Reduce) is a matter of taste.  For
> most computations this is irrelevent but a big exception is the kind of
> "positional" deconstructors that you propose (what is the leading term
> of a+x?).  While we could in theory go down the road of defining
> OpenMath normal forms for everything that doesn't seem like a good idea
> to me, although I note that we can do this for polynomials (where it is
> clearly important) by for example adding an ordering attribute to a SDMP
> object.
> 
> I think if you try to define the notion of a constructor in OpenMath
> then you will have to address the question of what is a normal form and
> that will end up making it much harder to write a phrasebook.  While I
> can easily construct the object "a+x" in Axiom I believe that the only
> way to do it in Reduce is to change a global variable which will change
> the bahaviour of all similar objects in the system.  I think its much
> better to leave that kind of implementation detail to the systems
> themselves.
> 
> Regards, Mike.
> 
> On Thu, Oct 24, 2002 at 08:36:36PM +0200, Arjeh Cohen wrote:
> <snip> 
> > IN GENERAL:
> >   When a symbol is defined as a constructor, we should be clear about
> >   the conditions on the arguments when it is used as a head in an
> >   apply. For instance: is rational(4,6) allowed? If we require a
> >   normal form for 2/3, the answer is no. If we do not care, the answer
> >   is yes. But then, what does it mean to take "denominator" (not yet
> >   defined...): 2 or 4?
> >   To prevent such ambiguities I propose:
> >   a) we are very precise about the requirements on the arguments;
> >   b) we make clear whether we are dealing with a normalform for the
> >      object under construction or not. In our example, we may want to
> >   add "rational_NF" which requires that there are two arguments, each
> >   of them integers, and furthermore that the second argument be stricly
> >   positive and 1 if the first is zero, and that the gcd of the first
> >   and second argument is 1 if the first argument is nonzero.
> >   etc..
> >   
> > IN GENERAL: Wouldn't it be useful for a symbol that is used as a
> >   constructor to have default deconstructors---that is, to be able to
> >   grab the i-th argument? It is not needed for codec's, where such
> >   operations are standard (getleaf, etc.), but it is useful for
> >   formulating FMP's. Sometimes, but not always, such arguments can be
> >   retrieved by symbols defined elsewhere in a CD.  A realization of
> >   this idea could take place in a CD defining a symbol "arg" having
> >   two arguments, the first is an OM object whose root is an OMA, the
> >   second is an integer. Eg, if f is a symbol then arg(f(a,b,c,d),3) =
> >   c. The symbol "arg" would not make sense when applied top a function
> >   symbol instead of a constructor symbol.  To prevent such
> >   difficulties arising when using "arg", one might take an alternative
> >   approach by staying away from the "meta symbol" arg and requiring
> >   that each argument of a constructor symbol A is accessible via a
> >   name/symbol defined in the same CD where A is defined. This would
> >   then come close to Michael Kohlhase's suggestion of introducing structs.
> > 
> 
> _____________________________________________________________________
> This message has been checked for all known viruses by Star Internet
> delivered through the MessageLabs Virus Scanning Service. For further
> information visit http://www.star.net.uk/stats.asp or alternatively call
> Star Internet for details on the Virus Scanning Service.
> --
> 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
--
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