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
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
