Adding two square matrices of different dimension should result in an error. Axiom returns something that looks more like a tensor product.

The implementation of + for SquareMatrix? is inherited from Matrix (src/algebra/matrix.spad.pamphlet). Matrix inherits + from the default implementation in MatrixCategory? (src/algebra/matcat.spad.pamphlet). There it says:

     "+": (%,%) -> %
       ++ \spad{x + y} is the sum of the matrices x and y.
       ++ Error: if the dimensions are incompatible.

and is implemented by default through:

     x + y ==
       ((r := nrows x) ^= nrows y) or ((c := ncols x) ^= ncols y) =>
         error "can't add matrices of different dimensions"
       ans := new(r,c,0)
       for i in minr(x)..maxr(x) repeat
         for j in minc(x)..maxc(x) repeat
           qsetelt_!(ans,i,j,qelt(x,i,j) + qelt(y,i,j))
       ans

I have no idea why the following code returns something of type SquareMatrix?(2,SquareMatrix?(3,Integer)).

(1) -> )set message bottomup on

   Your user access level is compiler and this set option is therefore 
      not available. See the )set userlevel command for more 
      information.

S d ==> SquareMatrix(d,Integer)

a2: S(2) := 1

(1)

a3: S(3) := 1

(2)

a2 + a3

(3)

It seems the Axiom interpreter is trying really hard to figure out what you might mean by this sum! The bottomup output shows the "mode selection" that it eventually arrives at.

I don't know whether I should consider that behaviour of Axiom as a bug or a feature.

If one puts

macro S d == SquareMatrix(d,Integer)
abc(): OutputForm ==
        a2: S(2) := 1
        a3: S(3) := 1
        (a2 + a3)::OutputForm

into a file aaa.input and then says

)read aaa
abc()

one gets exactly the same result of type SquareMatrix?(2,SquareMatrix?(3,Integer)) as above. Clearly, the same code, when put into aaa.spad does not even compile via

)co aaa

The danger is the following (which is maybe not clearly demonstrated by the code above): If somebody writes some prototype of a function into an .input file and later wants to transform the code into a .spad form, s/he cannot expect that the result is the same. If the code does compile the semantics is still different since for the .input part the interpreter might add some knowledge.

That problem is certainly known to people who have used Axiom extensively, but it will come as a surprise if one is relatively new to Axiom.

Category: Axiom Library => Axiom Interpreter Status: open => closed

It is true that Axioms interpreter and compiler apply (slightly) different semantics. However, it seems to me that if code compiles with spad, then it should return the same result when interpreted.

I'm quite sure that this problem is inevitable given that we want the interpreter to guess types...

Martin

I agree with Martin that we should expect that (most) SPAD functions will work when written as function definitions in the Axiom interpreter but usually not the other way around. Although the distinction between interpreter and compiler is a bit ambiguous because functions are usually also compiled to lisp in the Axiom interpret, where possible. The Axiom interpreter however makes assumptions about types, performs "mode matching" and does automatic coercions in an attempt to releave the user of having to specify such details. This is not part of SPAD or Aldor semantics.

This "mode matching" mechanism in the Axiom interpreter is what gives the perhaps unexpected result above. I think it goes something like this: In trying to resolve the meaning of the + operator, mode matching searches for coercions of the operands such that the signature of some known (exposed) function matches the resulting signatures of the operands and the type of the desired result (if specified). It then applies the coercions and function of the first match it finds.

I think this behaviour is fundamental to the design of the Axiom interpreter and cannot/should not be changed. However in a sense it is/was only an experiment. There does not seem to be any sound and complete theory of how it should work in practice. (I think there is a paper about the theory of automatic coercions in the reference library ) In particular, it is difficult to predict in advance the affect for providing the interpret with certain coercion paths since the mode matching search can become quite complex - as the example above illustrates. But it is also essential for basic use of the interpreter such as:

x+1

(4)

where we see the interpreter does behave in a simple and expected manner.

So in short: I think we need a theory, and then we need to review and edit Axiom's current system of coercions to try to ensure that the Axiom interpreter's behaviour is more intuitive for new users.

As an interim measure, it might be nice if we had a more user-friendly way to display the results of the mode matching than the obscure result of )set message bottomup on.