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) 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. > | 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. > | 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. More interesting perhaps is if I wrote DirectProduct(4, PrimeField 7) and then the result domain inherits a lot of structure from such fields. > [I'm not being facetious, I'm trying to understand your perspectives] > Good! :-) > | 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"). > | 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'? :-) Regards, Bill Page. _______________________________________________ Axiom-math mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-math
