On September 18, 2006 7:24 AM Ralf Hemmecke wrote: > > > Ralf Hemmecke wrote: > >> I agree with you [Gaby] that if D had type T then Variable(D) > >> should have type T (plus maybe some exports that allow to > >> create "indeterminates"). > > > Bill Page wrote: > > The meaning of this statement is unclear to me. Do you mean: > > If D has category T then Variable(D) should have category T? > > If so, I would disagree. Variable(D), as a universal algebra > > over some symbols must have a different (but related) type, > > perhaps Variable(D) has Universal(T)? > > Let's make it simple. Integer is a Ring. Don't you want that > Integer together with "indefinite integers" also form a ring?
Yes. At least a Ring but it will also be something else as you said parenthetically above "plus maybe some exports that allow to create indeterminates". > I don't think that I would want Universal(Ring). What is > Universal, by the way? It is some category constructor that I was imagining might be definable. This constructor adds the required additional exports. > > I understand that "indefinite" thing just as a way to encode > a delayed evaluation. In the "computation" that is done just > with the type information, you can do any tricks that you can > do with that information, but if that computation needs a value, > it has to wait until I provide one. I am not sure how to distinquish "tricks" from "computation". Perhaps you mean purely symbolic manipulation of expressions versus the appliction of algebraic operators defined by some underlying domain? What you call "delayed evaluation" (in a computer science sense) has something to do with universal algebra in a a mathematical sense. We need a mathematics (algebra) "large enough" to express this notion. > The point is, that you cannot apply an arbitrary operation on > these indefinite objects. For example if I have a very restricted > scope and not / operation can be seen then the compiler should > reject to compile a/b for indefinite integers a and b. > Yes, but that is generally true of Axiom's algebra. > ... > >> > >> Mathematically, that's not a big deal. But Aldor domains are > >> actually multi-sorted algebras. That makes the situation a little > >> more complicated. > > > I think sometimes you think too much about Aldor and not enough > > about Axiom... ;) > > I don't think that my statement is much related to Aldor. You could > replace Aldor by Axiom or SPAD, if you like. So what did you > actually mean? > What I meant was that you should look at how the algebra (such as Expression) is implemented in Axiom now. I would prefer to replace Aldor by SPAD for the purposes of this dicussion since Axiom's algebra is currently implemented in SPAD even though we are generally confident that it can be re-written in Aldor. > ... > > The interesting thing to me is that all you appear to be doing here > > is "re-inventing" the Expression domain constructor. > > > > It seems to me that 'Expression(Integer)' is a good enough name. :-) > > But inside Expression(Integer) the variables have NO type information > attached. You understand that instead of talking about Expression(Integer), as long as we do not introduce any functions, we can use instead just Polynomial, right? (Substituting EXPR for POLY below gives the same result.) But if we talk about POLY, it's implementation is already clear in Aldor. In Axiom I can write: (1) -> a1:POLY INT Type: Void (2) -> a1:=1 (2) 1 Type: Polynomial Integer (3) -> a1:=1.1 Cannot convert right-hand side of assignment 1.1 to an object of the type Polynomial Integer of the left-hand side. I want to think of 'a1' as the "typed variable". We can write: (3) -> a2:POLY INT Type: Void (4) -> (a1+a2)@POLY(INT) (4) a2 + 1 Type: Polynomial Integer But (5) -> (a1/a2)@POLY(INT) An expression involving @ Polynomial Integer actually evaluated to one of type Fraction Polynomial Integer . Perhaps you should use :: Polynomial Integer . ----------- I used '@POLY(INT)' because I wanted to tell the Axiom interpreter not to look of other coercions which would have made the interpretation of '/' possible but no longer in 'POLY INT'. Should we say that 'a1' represents an indefinite integer? Tentatively, I think so. > > > I strongly recommend that you take a close look at how Expression > > is implemented in the Axiom library. > > Thank you. But Expression is not what solves the "indefinite" > problem. You are right. Expression is too general. Not all objects in 'Expression Integer' evaluate to Integer. How about 'Polynomial Integer'? Maybe it is to restrictive and we could admit at least some other expressions not in 'Polynomial Integer' which do evaluate to Integer? > > > 'sin(a1)' which are not evaluated any further in the Expression > > domain. > > OK, let's take > > n: Expression Integer := n > z := sin(2* %Pi * n) > > Axiom knows, in fact, nothing about the n. But if it really > knew that n is an Integer, it could simplify z to 0. > > That should be a test case for indefinite computation. I do not agree that Axiom knows nothing about n. It knows for example that a1 has been assigned a value but that a2 has not. (6) -> )di prop a1 Properties of a1 : Declared type or mode: Polynomial Integer Value (has type Polynomial Integer): 1 (6) -> )di prop a2 Properties of a2 : Declared type or mode: Polynomial Integer --------- I agree that Axiom should be able to simplify z := sin(2* %Pi * a2) to 0 (where a2 is any polynomial with integer coefficients). But Axiom does not even simplify z := sin(2* %Pi) to 0. When should such a simplification take place? In general Axiom's 'simplify' operations are quite weak. > ... > > > > I don't understand. Obviously Expression is a domain that the > > SPAD compiler understands. Implementing Expression in Aldor > > should be quite straight forward. > > Of course the Expression type is known. But is should not be > built-in into the compiler. It should live in a library. > ??? Expression is not "built-in" to the SPAD compiler. Regards, Bill Page. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer