Bill Page wrote:
>
> On 8 April 2015 at 18:20, Waldek Hebisch <[email protected]> wrote:
> > Bill Page wrote:
> >> ...
> >> What bothers me more is the meaning of the category Eltable. In
> >> typical Axiom style we are not told very much about what it means.
> >> In some cases, e.g. Ring, not much more is needed than a reference
> >> to ring as a well-known mathematical object. But really we should
> >> probably expect a set of axioms to be associated with each category.
> >> What axioms should we associate with Eltable? We are only told that
> >> the members of % are "data structures" and "algebraic structures' that
> >> have some kind of "indexed elements". My point is that I suspect that
> >> we can not specify reasonable axioms for Eltable without requiring
> >> equality on S. Maybe I am wrong.
> >
> > 1) You can use equality in axioms without having equality as
> > export.
>
> The concept of using equality in the definition of a category without
> exporting it strongly contrasts your view of the FriCAS/Axiom library
> from my own. I specifically said library and not just SPAD because
> you are perfectly correct that it is possible to do anything you like
> when using SPAD as a general purpose programming language, say for
> writing a accounting application. But in the design of the FriCAS
> library it seems to me very natural to think of every domain and
> category as a mathematical object - not just *representing* some
> mathematics but actually *being* a concrete realization of some
> mathematical concept. Of course to a greater or lesser extent the
> identification of FriCAS objects as mathematical depends on one's
> imagination but this is strongly aided by the association of exported
> operations with essential attributes of objects. In essence an object
> is defined by what it exports (and a set of axioms).
>
> So for example among a few other things RING exports:
>
> ?*? : (%,%) -> %
> ?+? : (%,%) -> %
> -? : % -> %
> ?=? : (%,%) -> Boolean
> 1 : () -> %
> 0 : () -> %
>
> with these axioms:
>
> For all a, b in %, the result of the operation a + b is also in %.
> For all a, b in %, the result of the operation a * b is also in %.
>
> There exists an element 0 in %, such that for all elements a in %, the
> equation 0 + a = a + 0 = a holds.
> For all a, b and c in %, the equation (a + b) + c = a + (b + c) holds.
> For all a and b in %, the equation a + b = b + a holds.
> For each a in %, there exists an element -a in R such that a + (-a) =
> 0, where 0 is the additive identity element.
>
> There exists an element 1 in %, such that for all elements a in %, the
> equation 1 * a = a * 1 = a holds.
> For all a, b and c in %, the equation (a * b) * c = a * (b * c) holds.
> For all a and b in %, the equation a * b = b * a holds.
>
> For all a, b and c in %, the equation (a + b) * c = (a * c) + (b * c) holds.
> For all a, b and c in %, the equation a * (b + c) = (a * b) + (a * c) holds.
>
> These axioms can all be expressed in terms of just those the operators
> that are exported. It would seem exceedingly strange to me if Ring did
> not export =.
I agree that this is nice to have close correspondence
between exported signatures and axioms. In particular
one try to use axioms which are just equalities valid
for all tuples of arguments and use signatures to
like '0' ore 'inv' to constructively represent
existential axioms. But I am affraid that consistently
requesting this is too limiting.
> > 2) I am not sure we can give nice axioms for Eltable. To say
> > the truth I am afraid that nice axioms are just product
> > of sloppy way of developing math.
>
> That is a remarkable statement!! Of course I did not claim that the
> axioms had to be "nice" whatever that means.
>
> > More precisely, we
> > can give nice axioms for isolated domains. But when we
> > try to fit them together we frequently have cases when
> > we want to use code even when assumptions are violated.
>
> For me this would mean that it was time to review the axioms.
Yes, in principle we should do this. But then axioms no
longer are nice. In particular, because they are different
than texbook version, we need to develop our own theory.
Of course for affected operations we need to prove that
they work anyway. But type correctness may force us to
propagate changes to seemingly unrelated places. Currently
one approach I use is to call 'error' in case when given
piece of code is called when real assumptions (the ones
beyond official signature) are not satisfied. But this
clearly breaks encoding of existential quantification
via signatures: since we no longer know if given function
will return, we do not know if the corresponging object
exists.
>
> > Case in point is Euclid's algorithm. Theoretically we
> > need EuclideanDomain, that is ring without zero divisors
> > to use it. But we may try to use it for polynomials over
> > product of fields. If we hit zero divisor, then we fail.
> > But if all divisons work then we get GCD.
>
> Now you introduce a new concept: "fail". To me this means that the
> logic is no longer simply Aristotelian (i.e. every statement is either
> "true" or "false"). In principle I have no objection to this but I
> think it deserves to be reconized explicitly and for the most part in
> FriCAS it is via the 'Union(%,"failed")' construct.
Well, using 'Union(%,"failed")' leads to correct code, but the
code is longer and more complicated than uncoditional code.
Also, "failed" may propagate to different places. So to
limit profileration of "failed" we may be forced to have two
versions: unconditional one (without failed) and the second
one using "failed". But now we loose advantage of generic
coding: the two versions are essentially identical, but use
different types so we need two separate copies of the code.
>
> > 3) Equality is fundamental to math, frequently it is considered
> > part of logic. Without equality it is hard to formulate
> > any axioms. So still I do not see why you worry about
> > Eltable and accept categories and domains without equality.
> >
>
> Yes you are right. In fact it seems to me that a domain without any
> kind of equality is a kind of lie. But a fundamental division in the
> FriCAS library occurs at the top of the category lattice heterarchy
> between BasicType and Aggregate. Everything below BasicType exports =
> while those below Aggregate export
>
> eq? : (%,%) -> Boolean
>
> where
>
> eq?(x,y) -> true if x is identical to y, otherwise false
>
> Presumably 'eq?' is often implemented as just EQ$Lisp. Aggregates are
> supposedly "data structure"-like objects with things of BasicType are
> supposedly "algebraic". But some domains are both, e.g. Set.
I must admit that I am not sure why 'eq?' is exported for 'Aggregate'
but not for other types. One guess may be that 'eq?' is needed
to detect cyceles in lists and graphs. It is also useful
for speeding up equality of aggregates (but may be used to
speed up equality for most types, so why no 'eq?' for other types).
> My point here is to refer again to the article by Davenport "Equality
> in Computer Algebra and Beyond".
>
> It is not clear to me whether or not Eltable is intended to be "data
> structure"-like or not and whether the index domain S should also be
> just "data structure"-like or mathematical. Right now the definition
> says it should be mathematical.
I do not think there is really any deep distinction between
"data structures" and "mathematical" domains. There is theory
of lists and array, not very deep but comparable to begining
theory of groups. And sets are both a data structuture and
a rich mathematical object.
>
> If equality really is not computable than maybe it would be more
> "natural" if equality was defined as
>
> = : (?,?) -> Union(Boolean,"failed")
Maybe. But any attempt at equality would be on "best effort"
basis. Also there are cases where failure is the expected
outcome, for example for functions given by code. So unlike
cases I metioned above where failure is rare and we can
avoid it via randomization and repeating computations we
can not avoid failure. So if we want algorithm with
guarented result, we can not use equality. And to make
sure we do not use it we should not provide it.
>
> >> > AFAICS modification to XHashTable can be done without touching
> >> > any other domain, in particular other domains will not get any
> >> > extra exports. We need to adjust categories, but relaxed
> >> > parameters do not affect any existing domain.
> >> >
> >>
> >> So, with TableAggregate(Key: Type,Entry: Type), if we specify a Key
> >> that does not export =$key will TableAggregate still export 'table()'
> >> with no arguments? If so, what will XHashTable do to implement it?
> >
> > Well, 'table()' should be a conditional export of TableAggregate...
> >
>
> So this means that TableAggregate only provides a means to create
> members of % if Key is of type SetCategory, otherwise creating members
> is somehow unique to the domain. This works but I am not sure if we
> should consider it fully satisfactory.
Actually I am affraid we can not prevent creating tables just by
restrictng signatures: Aggregate unconditionally exports 'empty()',
so trying to create empty hash table will be allowed by type
system and all we can do it to singal error when Key does not
have BasicType.
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
