axiom-developer
[Top][All Lists]

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

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

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.

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

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