[om] more comments on CDs
Michael Kohlhase
Michael_Kohlhase at asuka.mt.cs.cmu.edu
Wed Oct 30 16:07:57 CET 2002
> 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
More information about the Om
mailing list