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

[Bill Page]

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.