Ralf Hemmecke <[EMAIL PROTECTED]> writes:
[...]
| Looking at it mathematically (and simplified) then all we do is that
| we take a universal algebra D = (A, F) where A is the carrier set and
| F are the functions on it. Variable(D) is maybe a bad name, but all we
| do is that Variable(D) = (A', F') is a universal algebra where A' is
| the union of the set A, a set X of indeterminates, and all things that
| can be generated from A and X by applying functions from F'. F and F'
| behave identically on A.
yes.
| Mathematically, that's not a big deal. But Aldor domains are actually
| multi-sorted algebras. That makes the situation a little more
| complicated.
but not impossible.
In this discussion, I'm going to ignore Aldor for a moment and
concentrate on SPAD because I don't have access to Aldor source code
and anything that might transpire out of this discoussion should
probably be recorded as a feature-request for SPAD with all the
"insights" we might have gained.
| So I still disagree with you that x+y should be of type
| FreeMonoid(Variable(Integer)). From what I said above, it seems more
| natural to me that its type is Variable(Integer) (well, it's a bad
| name, maybe Indefinite(Integer) would be better).
I don't think it should be Variable(Integer). For me,
Variable(Integer) means a symbol who interpretation is of type
Integer. I don't like Indefinite(Integer) neither. So, it might very
well be that we're back to our old beloved friend Expression(Integer).
| Anyway, what we want is a nice way of adding elements and more or less
| keeping the type of the domain.
yes.
| And that is not possible if you just define "Indefinite" having one
| argument D.
I'm clear why not. Could you explain this a bit further?
| One must know the type of D
| (a category) so that the return type would be clear.
|
| Indefinite(C: Catagory)(D: C): C == add {
| Rep == Union(d: D, ???)
| ...
| }
|
| The ??? should be something that allows arbitrary expressions formed
| from D, the functions in C and some indeterminates X. (I have no idea
| how that would look like. Maybe just delayed evaluation of function
| composition.)
I suspect I'm being dense here. What would be wrong with Expression D?
| > [...]
| > | (1) -> (a1,a2,a3,a4):Expression Quaternion Fraction Integer
| > | Type: Void
| > | (2) -> m := matrix[[a1,a2],[a3,a4]]
| > | | +a1 a2+
| > | (2) | |
| > | +a3 a4+
| > | Type: Matrix Expression Quaternion Fraction Integer
| > | | given by Bill suggest that the Axiom interpreter is a bit more
| > relaxed.
| > Funny enough, I tried similar thing and sent a message before seeing
| > Bill's. That is a natural thing to do if you have a Universal Algebra
| > backgroud -- e.g. you're used to the 3M's.
|
| Maybe. I don't say that shouldn't be allowed in the interpreter, but
| the compiler would generate a matrix of 4 uninitialized entries. Now
| what happens if you print m(1,1)?
If that entry is a Variable? I would expect the output to indicate
either the name or just m(1,1). Look at what Axiom prints when you
say
m * m
That matches my expectation.
| If that prints something reasonable
| then it tells me that the compiler knows about a special domain
| constructor, namely Expression.
yes.
| Drop "Expression" from above, what
| would be on screen for "stdout << m(1,1)"?
well, it Expression is dropped then we're back to the interpretation
we all agree on: A value of type Quaternion Fraction Integer.
Consequently m(1,1) must hold value of that type.
| The interpreter can add
| smart things. I am asking for the compiler.
|
| [...]
|
| > | I guess the interpreter has to do a lot of
| > | work to find the right interpretation for such a + and it must decide
| > | for one of possibly many choices.
| > If "+" is defined as beeing an associative operation , there would
| > not
| > be much work to do.
|
| Oh, who said that + is associative? The documentation, right?
And
yes, but in my model much of the documentation is moved to code. In
this case, I would like to see properties() used to attach
mathematical properties.
| But that
| is not a nice thing to take into account for the compiler.
Why?
>From my point of view, the type of an operation is just as important
as its algebraic properties.
| It would be
| much better if Aldor allowed to state associativity in a formal manner.
SPAD does. See properties()
| > In fact I don't want the interpret to become
| > super smart. Just lift operations.
|
| I am completely with you. The interpreter should not have any
| mathematical knowledge, just look into a database (basically the Axiom
| libraries) and figure out what could be done. It should be possible to
| change the libraries and work with the same interpreter.
yes.
| > | But assume I say x+z for
| > | z: Variable(Float) := "z"
| > | what is the type of that? It is the type of its declaration:
| > Variable(Float).
|
| Oh, I meant the type of "x+z".
|
| > | Should the interpreter forbid such an
| > | addition?
|
| > there is no addition as far as I can see.
|
| But there was also no addition until you transformed Variable(Integer)
| into FreeMonoid Variable Integer.
I did not transform a variable to FreeMonoid Variable Integer.
However, I did suggest that type for th _compound expression_ "x+y"
when the question was asked.
| > | In the compiler I clearly don't want any guessing and not
| > | automatic conversion. Note that I prefer that (most of) the things
| > | that are possible in the interpreter could be compiled into stand
| > | alone programs.
| > | Anyway, if the type tower is always expanded like that you end up
| > | with the fact that
| > | (x+y)*x and x*x + x*y
| > | have types
| > | FreeMultiplicativeSemigroup FreeAdditiveSemigroup Variable Integer
| > | and
| > | FreeAdditiveSemigroup FreeMultiplicativeSemigroup Variable Integer
| > | and thus are not equal.
| > I don't see why.
|
| OK, let's turn this into a mathematical example.
|
| A := Fraction Complex Integer; a: A := 1
| B := Complex Fraction Integer; b: B := 1
|
| Clearly A and be are isomorphic as fields, but they are NOT identical.
As syntactic obejcts, no, they are not. The issue can be rephrased as
whether they should remain non-equal in other non-syntactical
intepretation. I think no.
| Not identical in Axiom and not identical in mathematics.
You have lost me on the last part. My book says that both A and B are
the same mathematical object. Why do you believe they are not?
| Note, we had a discussion whether "Fraction Fraction Integer" should
| be implemented to be the same as "Fraction Integer".
Under the mathematical interpretation they are the same. I believe
they should also be the same in Axiom -- at least if you take
dependent types seriously.
| Although I had
| even given code to do that, I believe it should not be implemented
| that way. Because an element that looks like (2/1)/(3/1) is NOT
| identical to 2/3.
By the same token we should prevent Axiom from simplifying 3+2 to 5.
| (Just consider fractions as equivalence classes of
| pairs of some type.
I don't follow.
-- Gaby
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
