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

```