axiom-math
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: iterators and car


From: Bill Page
Subject: [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product.
Date: Mon, 22 Oct 2007 12:03:50 -0400

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.




reply via email to

[Prev in Thread] Current Thread [Next in Thread]