RE: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory)

[Bill Page]

> Bill Page writes:
> | > | All domains that have SetCategory are required to have a
> | > | hash| into SmallInteger.
> | >
> | Gaby wrote:
> | > That is not a mathematical requirement.
> |
> Bill Page wrote; 
> | I would tend to agree but perhaps Kurt Gödel would not have...
> | ;-)
> 

On November 14, 2006 12:01 AM Gaby wrote:

> From constructive mathematics point of view, the only things
> that are required for a set are:
> 
>   (1) say how to build element of a set
>   (2) equality test.
> 

No, there is a lot more to the mathematics of set than that. It
would mean that all sets are finite and that is quite far from
the case. Rather, sets should be strongly related to types.

I think the "constructive mathematics" that is most suitable
to Axiom is probably is probably Intuitionist type theory
(Martin-Löf). See:

http://en.wikipedia.org/wiki/Constructive_type_theory

"A logical framework, such as Martin-Löf's takes the form of
closure conditions on the context dependent sets of types and
terms: that there should be a type called Set, and for each set
a type, that the types should be closed under forms of dependent
sum and product, and so forth."

In Axiom types are implemented as domains or categories. So this
means that for examle the set

  {1,2,3}

should not be considered as just member of the domain Set, but
rather it should denote a *domain* which has as members the
Integers 1, 2 and 3 in other words a sub-domain of Integer (or
PositiveInteger, NNI, etc.). And Integer itself can be viewed
as a set.

As a domain constructor Set(T) is best viewed as a "powerset"
type, i.e. the type associated with all subsets of a given type
T.

Axiom (SPAD) does have a "subdomain" construction which is used
for example to define NonNegativeInteger and PositiveInteger
from the type Integer. This is one of the less developed ideas
in Axiom but I think this is exactly the place where computer
algebra meets proof theory and is therefore ripe for further
development.

Regards,
Bill Page.