[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structu

From: Ralf Hemmecke
Subject: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures
Date: Fri, 10 Mar 2006 13:29:47 +0100
User-agent: Thunderbird 1.5 (X11/20051201)

Unfortunately, I've sent this mail only to Martin, so here it comes to axiom-developer together with an explanation of why there is this strange output.

(Well, that is my interpretation. I might be wrong so if anybody with more inside into the internals is on the list, feel free to correct me.)

Here you go...
On 03/09/2006 05:08 PM, Martin Rubey wrote:
> I am satisfied now:

Believe me, you are not.

Unfortunately, my Axiom now gives me the error message

(1) -> Integer has MyMonoid(Integer, *)

   >> System error:
Cannot open the file /home/hemmecke/software/Axiom/mnt/linux/aldor/lib/runtime.o.

,.. so I demonstrate it with pure Aldor.

Basically, if you replace "ArithmeticType" by "Ring" it should work with
  #include "axiom"
and inside Axiom.

#include "aldor"

MyMonoid(T: Type, m: (T, T) -> T): Category == with {
   square: T-> T;
   default {square(t: T): T == m(t, t)}

MyInteger: ArithmeticType == Integer add;
extend MyInteger: MyMonoid(MyInteger, *$MyInteger) == add;
extend Integer: MyMonoid(Integer, *$Integer) == add;
-- end
#include "aldor"
#include "aldorio"
#library MyMon ""
import from MyMon;
macro {
    Z == Integer;
    M == MyInteger;
main(): () == {
  stdout << "1: " << (Z has MyMonoid(Z, *$Z)) << newline;
  stdout << "2: " << (Z has MyMonoid(Z, +$Z)) << newline;
  stdout << "3: " << (M has MyMonoid(M, *$M)) << newline;
  stdout << "4: " << (M has MyMonoid(M, +$M)) << newline;

Compile with

aldor -fo -fao
aldor -grun -laldor mymonoid.o

and try to explain the output.

1: T
2: T
3: T
4: T

It's clear, isn't it?


OK, and now the explanation. One would like the output (T, F, T, F), rigth?

Now look at MyInteger. It has type

with {
  ArithmeticType; -- includes +, *, 0, 1
  MyMonoid(MyInteger, *$MyInteger);

Well, but MyMonoid is a **function**. So the type is (nearly)
with {
  square: MyInteger -> MyInteger;
  default {square(t: MyInteger): T == (*$MyInteger)(t, t)}

You see, the * is hidden behind the == sign. The actual exports are that of ArithmeticType together with "square". It should be clear that then
2 and 4 from above also return true.

HOWEVER, remove the line

  extend Integer: MyMonoid(Integer, *$Integer) == add;

and try to compile "aldor -fasy". Then look at the generated "mymonoid.asy". Look at the exports of |MyInteger|. Under |domExports| right at the bottom of the file, we find

          (|Apply| |MyMonoid| |MyInteger| (|Qualify| * |MyInteger|))
          ((|default| . 1)
            (|symeNameCode| . 51482908)
            (|symeTypeCode| . 366734318)))

That's interesting. The compiler would have a way to tell
that "MyInteger has MyMonoid(MyInteger, +$MyInteger)" is false.

Can someone explain that compiler design?

Well, mathematically thinking, I would say that (T, T, T, T) is OK, since "MyMonoid(Z, +$Z)" stands for the value that MyMonoid gives when applied to the arguments Z and +. There would be no way to guess the arguments from the value.

Well, this discussion is getting more and more into the internals...
I hope we all learn from that.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]