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

[Ralf Hemmecke]

On 09/17/2006 09:18 PM, Gabriel Dos Reis wrote:
> Ralf Hemmecke <address@hidden> 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.

That's OK for me. But it is easier for me to speak Aldor, because it has 
a reasonable language description. I am not at all fluent in SPAD, so 
maybe we need a translator sometimes.

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

OK, I can live with that. But that is saying that you don't just *lift* 
the operations from Integer to Variable(Integer). In Integer you would have

+: (%, %) -> %;

in Variable(Integer) you'd have

+: (%, %) -> FreeMonoid %;

So that is saying, for each operation you have to figure out the right 
return type. And since the signatures belong to the argument of the 
function "Variable", you'd have to build a universal constructor 
("Variable") that does this for arbitrary arguments.

Good luck to figure out the return type foo for Variable(MyInteger) and

MyInteger: IntegerType with {foo: %->%} == Integer add {foo(x:%):%==x}

> I don't like Indefinite(Integer) neither.  So, it might very
> well be that we're back to our old beloved friend Expression(Integer).

No, definitely not. The difference to Expression Integer is that the 
"Integer" in the argument says something about the coefficients in the 
internal representation (Remember Axiom stores Expression(D) as a 
quotient of multivariate polynomials over D in "kernels" as variables.)
So Expression(D) does NOT say anything about the variables. In fact, I 
believe that the argument of Expression is more or less only there for 
technical reasons. The domains Expression(Integer) and Expression(Float) 
or Expression(AlgebraicNumber) are all different. But an element of

Expression SUP Integer

could as well live in Expression Integer. Expression in Axiom is a way 
to remove type information. Good for interactive stuff, but I still 
believe that people should be more specific (ie add appropriate types) 
when they write libraries.

So what I want (and I think also you want that) is such a lifting 
procedure where the *types of the variables* would be known. So the 
whole expression whould type-check. It's a kind of TypedExpression 
domain. Expression and TypedExpression looks similar to lamda calulus 
and typed lambda calculus to me.

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

Because that would require that each domain exports its category. 
Remember, Aldor does not have reflection. You get D and currently the 
only way to ask something about the type of D is

   D has CATX

Of course that is not useful since you'd have to know the exports of D 
at the time you write the program. That's much too early.

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

As explained above, Expression D is NOT what you want.

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

Oh, please don't quote Axiom or any other system, I know they are 
relaxed and do what you expect. But look carefully at what you have 
written above, translate that into C, then you see that you have never 
given a1 a value, so the memory location is probably the nil pointer.

I quite like the distinction in the abstract of

http://portal.axiom-developer.org/refs/articles/TheUnknownInComputerAlgebra.dvi

Above a1,a2,a3,a4, and m are "programming variables" and interestingly 
there is actually no "mathematical symbol" specified above. The axiom 
interpreter now is smart and treats (1) as a definition of symbols that 
are called by the same name.

You see the difference if you type

)clear all
a1: Expression Integer := B

> | If that prints something reasonable
> | then it tells me that the compiler knows about a special domain
> | constructor, namely Expression.

> yes.

Maybe I was not clear enough. I meant, that then the compiler has the 
Expression domain built-in. That would be something that I would not 
really like. The compiler and the interpreter should not know about 
mathematics. You can easily implement Expression as a library package 
and that is where it belongs.

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

OK.

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

I am really curious, what model you have. What should

properties()$Integer

return?

> | But that
> | is not a nice thing to take into account for the compiler.
>
> Why?  

I meant that the documentation is not formal enough for a compiler.

> > From my point of view, the type of an operation is just as important
> as its algebraic properties.

Oh, yes, I completely agree. Axiom should have axioms. ;-)

> | It would be
> | much better if Aldor allowed to state associativity in a formal manner.
>
> SPAD does.  See properties()

Sorry, if you mean that, that is not formal enough for me. You just 
declare commutative("*") and you are done. If you start with the Peano 
Axioms then commutativity is not a declaration it requires a proof. So 
it's a theorem. What I would like to have is to state the theorem and 
hand it to a prover (who then spits out that * is commutative).

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

Good to hear that we are on the same side.

Ralf