On 09/17/2006 04:25 PM, Gabriel Dos Reis wrote:
Ralf Hemmecke <[EMAIL PROTECTED]> writes:
| > | > Intuitively I would expect Variable to mean simply "an
| > | > unspecified specific instance of a Domain/Type/what have you"
| > | > with ALL domains being possible - just so long as you specify
| > | > the type of the variable, e.g.:
| > | > | > a1 : Variable(Matrix Quaternion Fraction Integer)
| > | > | | Suppose there was such a domain constructor named
| > Variable(D: domain)
| > | which had the properties you suggest. What operations would you expect
| > | this domain to export? Would it have the same operations as D? For
| > | example '+'. Given two objects from the domain Variable(Integer),
| > | say 'x' and 'y', what is the type of the result of 'x+y'? Is it
| > | still in Variable(Integer)?
| > FreeMonoid Variable Integer
|
| Gaby, do you really believe that? But in order to say x+y you have to
| have the type of Variable(D: domain) in the first place.
yes. My working assumption is that if we had Variable(D: domain) to
mean anything, it would be such that operations of D would be *lifted*
to Variable(D: domain) and would work as if we had an algebra (in the
Universal Algebra sense). In this case "+" would be lifted to
Variable Integer, so that x + y can be interpreted as an element a a
free monoid generated symbols. That is not rocket science.
I agree with you that if D had type T then Variable(D) should have type
T (plus maybe some exports that allow to create "indeterminates").
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.
Mathematically, that's not a big deal. But Aldor domains are actually
multi-sorted algebras. That makes the situation a little more complicated.
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).
Anyway, what we want is a nice way of adding elements and more or less
keeping the type of the domain. And that is not possible if you just
define "Indefinite" having one argument D. 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.)
[...]
| (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 prints something reasonable then it
tells me that the compiler knows about a special domain constructor,
namely Expression. Drop "Expression" from above, what would be on screen
for "stdout << m(1,1)"? 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? But that
is not a nice thing to take into account for the compiler. It would be
much better if Aldor allowed to state associativity in a formal manner.
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.
| 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.
| 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.
Not identical in Axiom and not identical in mathematics.
Note, we had a discussion whether "Fraction Fraction Integer" should be
implemented to be the same as "Fraction Integer". 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.
(Just consider fractions as equivalence classes of pairs of some type.
Ralf
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer