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 _______________________________________________ Axiom-math mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-math
