[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:

| 
| On 22 Oct 2007 10:16:33 -0500, wrote:
| > Bill Page writes:
| > ...
| > |
| > | I would like to consider what is?
| > |
| > |   1..9
| > |
| > | Right now in Axiom this is evaluated as a member of 'Segment
| > | PositiveInteger', i.e. the domain of all such segments. But in general
| > | I think I would prefer if '1..9' actually denoted a domain - a subset
| > | of the Positive Integers - with members 1, 2, 3 ... etc.
| >
| > Couold you elaborate on why `1..9' should denote a domain, and what
| > the benefits would be?
| >
| 
| Well, for one I could then write the cross-product of such domains:
| 
|   Product(1..9,1..4)

What would be its meaning?
The reason I'm after the meaning is that once I figured out what you
really want to express -- not the syntax -- then I can figure out
how to work on the syntax.

| and iterate over them like this
| 
|   for i in expand()$Product(1..9,1..4)
| 
| where 'expand' (or whatever we decide we want to call this operator
| from the category Finite). Or even better if the generator 'expand'
| also is implicit for any domain in Finite so that we could write:
| 
|   for i in Prooduct(1..9,1..4)
| 
| Of course we could also simply define some new 'CrossProduct' domain
| constructor that takes as argument something of type 'Segment Integer'
| but this seems considerably less general.

If we introduce a Cross domain, I would expect it to take a sequence
(e.g. List) of domain as argument.  Why would that be less general?

| > | I am having a little trouble actually articulating the difference
| > | between these two. It seems somewhat artificially imposed by Axiom's
| > | type hierarchy that does not easily allow domains to be members of
| > | domains. (Domains belong to categories, not other domains.).
| >
| > In fact, that is not so clear. If you ask the interpreter what is the
| > type of Domain, it would answer 'SubDomain Domain'.  And don't go query
| > the type of SubDomain Domain :-/
| >
| 
| Yes. As I have said several times before (e.g. in an exchange a few
| years with Peter Broadbery), I think this upper part of the Axiom
| domain/category type system is a little messed up. I believe Aldor
| presents one possible solution to these problems but there may be
| other solutions.

Well, my own opinions are not definite yet, but I do see some value to
the `domain theoretic' approach to this matter.  In that scheme
`Categories' are left to just to ensure the availability of certain
operators to help the compiler in semantics analysis and efficient
code-generation.  From that perspective, asking the question `what is
the type of this domain' is an ill-posed problem.  Rather, one should
be asking the question `does this domain satisfy that category?'.

Indeed, once you've queried the type of a domain, what do you do with it?

| > | We want to be able to write:
| > |
| > |   DirectProduct(4,1..9)
| > |
| > | but this does not work because '1..9' is not a type - it is an object
| > | of 'Segment PositiveInteger'.
| >
| > If it worked, what would you have liked the mathematical meaning to
| > be, and why?
| >
| 
| I would like the result to be a finite domain.

that says what property the result would have, but it does not tell me
what the meaning of the result is.  I would like to underdstand 
the mathematical meaning.

[...]

| > | Another example of this in Axiom that *does* work right now is:
| > |
| > |   DirectProduct(4,OrderedVariableList [a,b,c])
| > |
| > | OrderedVariableList is a domain constructor that takes something of
| > | List Symbol as a parameter. In order to introduce '1..9' as a domain
| > | it would be possible to introduce new domain constructor like
| > |
| > |    )abbrev domain INTS IntegerSegment
| > |    IntegerSegment(S:Segment Integer): with Finite ...
| > |
| > | that takes something of 'Segment Integer' as a parameter. Do we want
| > | 'IntegerSegment' to also be a subdomain of Integer?. In any case,
| > | then we could write:
| >
| > I do not see obvious reasons why I would want IntegerSegment to be a
| > subdomain of Integer.
| >
| 
| 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.

| > |   DirectProduct(4,IntegerSegment 1..9)
| > |
| > | But somehow the distinction between '1..9' and 'IntegerSegment 1..9'
| > | and '[a,b,c]' and 'OrderedVariableList [a,b,c]' seems artificial.
| > |
| > | It occurs to me that one might like at least the Axiom interpreter to
| > | perform some kind of automatic coercion from 'x' in a domain like
| > | 'Segment Integer' into the *category* consisting of domains
| > | 'IntegerSegment(x)'.
| > |
| > | I think Gaby recently referred to this preference for things like
| > | '1..9' and [a,b,c] to also
| > | represent domains as a more "categorical" approach.
| >
| > In general, I would like OpenAxiom to take a more categorial approach
| > to almost everything -- in particular `cross'.
| 
| Great. One should probably try to be more specific here about what one
| means by a "categorical approach". You could mean for example trying
| to provide mathematical semantics based on category theory. I have
| discussed before how one really should define 'cross' as a categorial
| limit in terms of the existence of the unique (universal) operation:
| 
|   product: (A:Type, A->X,A->Y) -> (A->%)
| 
| See: http://wiki.axiom-developer.org/SandBoxLimitsAndColimits
| 
| > However, I'm interested in some of you ideas here.  Please, could you
| > elaborate, and if possible, give some use cases?
| >
| 
| Do you mean use cases for operations like 'product' above or use cases
| of the domain 'Product' or use cases of the domain 'IntegerSegment'?
| :-)

I'm specifically after `1..9' that you would want to be a domain
and the various constructs you based on it.

-- Gaby