[Top][All Lists]

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

Re: [Axiom-developer] Question concerning types...

From: Ralf Hemmecke
Subject: Re: [Axiom-developer] Question concerning types...
Date: Mon, 18 Sep 2006 13:23:50 +0200
User-agent: Thunderbird (X11/20060719)

I agree with you that if D had type T then Variable(D) should have type T (plus maybe some exports that allow to create

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? I don't think that I would want Universal(Ring). What is Universal, by the way?

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. 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.

Looking at it mathematically (and simplified) then all we do is that we take a universal algebra D = (A, F) where A is the
carrier set and F are the functions on it. Variable(D) is maybe
a bad name, but all we do is that Variable(D) = (A', F') is a
universal algebra where A' is the union of the set A, a set X of indeterminates, and all things that can be generated from A
and X by applying functions from F'. F and F' behave identically
on A.

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?

So I still disagree with you that x+y should be of type FreeMonoid(Variable(Integer)). From what I said above, it seems
more natural to me that its type is Variable(Integer) (well,
it's a bad name, maybe Indefinite(Integer) would be better).

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.

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.

'sin(a1)' which are not evaluated any further in the Expression

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.

Now what happens if you print m(1,1)? If that prints something reasonable then it tells me that the compiler knows about a special
domain constructor, namely Expression.


Drop "Expression" from above, what would be on screen for "stdout
<< m(1,1)"? The interpreter can add smart things. I am asking for
the compiler.

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.


reply via email to

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