[Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product.

[Gabriel Dos Reis]

On Mon, 22 Oct 2007, Bill Page wrote:

| > [...]
| > |
| > | Well for example, maybe I would want to write:
| > |
| > |   x:IntegerSegment 1..9
| > |   y:=x + 1
| > |
| > | where the type of 'y' might be Union(IntegerSegment 1..9,"failed").
| >
| > So, you are actually after a domain that constrains all operations on
| > the values of its objects to deliver a value in a specified bound.  I
| > can be persuaded that IntegerSegment convays such meaning, but I'm not
| > sure the notation `1..9' is intuitive to me, given its other existing
| > meaning.
| 
| Do you have another suggestion?

Until I fully understand what you want and its meaning, and why, my
suggestion would be to keep things simple and explore what (e.g. the
abstractions) you want to express and why you can't express it with
the current lanaguage.

| > ...
| > I'm specifically after `1..9' that you would want to be a domain
| > and the various constructs you based on it.
| >
| 
| Ok. Well as I said, I am willing to live with '1..9' being a member of
| the domain 'Segment PositiveInteger' provided that there is also a
| coercion of such objects to an equivalent Finite domain so then at

Would you be happy if we added something like

    if S has impliesFiniteSegment then Finite

where impliesFiniteSegment is some predefined attribute?  Or do you
really insist on a coerce?  If so, how different would the target
domain be?

-- Gaby