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

[Ralf Hemmecke]

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

Of course, no distiction.

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

Right. Let's make it clearer. Suppose we just take one operation. For 
simplicity let's take +. Let's take the Integers Z as a carrier set and 
define the universal algebra U = (Z, +) where + works on Z as usual. Let 
us introduce just one indefinite integer x. That means we form
(Z', +') where Z' is a superset of Z and +' restricted to Z is +.
Z' is the term algebra constructed from
Z union {x}  and the function symbol +'
where it is understood that u+'v is always replace by the actual integer 
sum u and v if they are both elements of Z.

If you want more indefinite integers, then iterate that process.

Who would be satisfied with such a way of modelling indefinite integers 
and who would not?

But note that Integer also has a operation zero?: Integer -> Boolean. So 
Z' should also deal with that. But we all know that Aldor/Axiom/SPAD 
domains are not just universal algebras but multisorted.

> What I meant was that you should look at how the algebra (such as
> Expression) is implemented in Axiom now.

I think the Expression constructor is a clever thing. In particular, 
here at RISC are several people who deal with symbolic summation. There 
one analyzes the (Mathematica) expression and basically forms a rational 
function domain which is basically something like Expression(Integer) is 
in Axiom.

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

Yes, of course.

> (Substituting EXPR for POLY below gives the same
> result.) But if we talk about POLY, it's implementation is already
> clear in Aldor.

Don't worry, I can read SPAD, but it's terribly more complicated than 
Aldor for me.

> In Axiom I can write:
>
> (1) -> a1:POLY INT
>        Type: Void
>
> (2) -> a1:=1
>
>    (2)  1
>         Type: Polynomial Integer
>
> (3) -> a1:=1.1 m
>
>    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.

Well, I would agree, if the interpreter knows how to deal with such 
"programming variables" that have no values, but neither SPAD nor Aldor 
understand that.

Have you ever typed

foo(n: Integer): Expression Integer == (k: Expression(Integer); n*k)
foo 1

into Axiom? (Save your session before doing it.)

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

No, that is not the problem. Assume that a1 is an indefinite integer.
zero?(a1) shouldn't evaluate to Integer. The point is that although you 
don't know the value of a1, the interpreter/compiler should only allow 
you to write foo(a1) if there is a function

foo: Integer -> SomeResultType

and otherwise tell you that you are doing nonsense. Note that in 
Expression(Integer) you can apply any function to a "kernel" since no 
type information is available. And another difference is: If a1 is an 
indefinite integer and e1 is an indefinite expression involving a1 then 
although you have no value, it is completely clear what type the result 
will have if you plug in a certain integer for a1 into e1. For an 
arbitrary expression from Expression(Integer) you cannot do that.

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

Why do you think an expression/polynomial that involves indefinite 
integers must evaluate to an integer? zero?(a1) would evaluate to 
Boolean, and that would be perfectly fine for me.

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

But that is the interpreter and not SPAD itself.

> ---------
>
> I agree that Axiom should be able to simplify
>
>    z := sin(2* %Pi * a2)
>
> to 0 (where a2 is any polynomial with integer coefficients).

No! That would be WRONG.
Assume that the polynomial domain is Z[x] 
SparseUnivariatePolynomial(Integer). And let f: Z[x] -> Q be the 
homomorphism of rings that maps Z[x] to the rational numbers 
(Fraction(Integer)). f should map x to 1/4. Now assume that a2=x.

sin(%Pi * a2) does not simplify to 0 in general. But if the interpreter 
"knows" that a2 is an integer, the simplification is safe.

Ralf