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

[Ralf Hemmecke]

On 09/18/2006 01:00 PM, Gabriel Dos Reis wrote:
> Ralf Hemmecke <address@hidden> writes:
>
> [...]
>
> | > | 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). 
>
> I really meant *lift*, in the following sense:
>
>      Integer × Integer  ---> Variable Integer × Variable Integer
>              |                                |
>       binOp  |                                | lift(binOp)
>              v                                v
>           Integer    ------------>    Variable Integer  
>                           
>
> (the horizontal arrows are to be elaborated).

OK, I want it exactly so. But now you are saying yourself that the type 
of x+y from above should be Variable(Integer) and not the FreeMonoid 
thing. ;-)

> | In Integer
> | you would have
> | 
> | +: (%, %) -> %;
> | 
> | in Variable(Integer) you'd have
> | 
> | +: (%, %) -> FreeMonoid %;
>
> I certainly want to say (x+y) + (s+t), so I think I really want to have
>
>      + : ($, $) -> $
>
> in Variable Integer -- or FreeMonoid $, whatever it is called.

Yep, exactly what I said. In Variable(D), Category of D in and Category 
of D out. So the type of Variable (or Indefinite) would be... hmm I need 
an extra argument... (aaaahhh, I had that yesterday...)

Indefinite(C: Catagory)(D: C): C == add {
    Rep == Union(d: D, ???)
    ...
}

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

> So?

> | Remember, Aldor does not have reflection. 

> If you don't want me to quote Axiom or other systems to you, why are
> you quoting Aldor to me?

I cannot program with reflections in Axiom either. ;-)

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

> | 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.
>
> That does not make any sense to me.  How do you declare a symbolic
> variable in C?

How do you declare a symbolic variable in SPAD? As a demonstration, a 
short program

---BEGIN aaa.spad
)abbrev package RHXPKG RHxPkg

RHxPkg(): with
  foo: Integer -> Expression Integer
 == add
  foo(n: Integer): Expression Integer ==
    k: Expression(Integer) -- := "x"::Symbol :: Expression(Integer)
    n*k
---END aaa.spad

The two minus signs inside the code are delibarate!
Start Axiom, say
)compile aaa.spad
foo(3)
and be surprised.

> | 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. 
>
> They have to know about *something*.  That something would hardly be
> sport games.  
>
> I suspect you instead wanted them to know as minimum as possible of
> mathematics. 

Yes.

> | I meant that the documentation is not formal enough for a compiler.
>
> yes, but you can't completly remove documentation.  All you can wish
> is to move as much as possible from documentation to something the
> compiler understand.

Of course. I stick to the LP paradigm. I am not a computer and computers 
are my slaves. If I just tell them to prove some stupid theorem for me 
they should do it. ;-)

> | If you start with the Peano
> | Axioms then commutativity is not a declaration it requires a proof. 

> If I start there, then probably.  But what if I do not?

Well, I know we don't start always from zero, but we should always have 
a knowledge base in the background and your definitions and theorems are 
based on that knowledge base. If the commutativity proof is inside the 
base then fine, otherwise you are not doing mathematics.

> If you want to take it that way, do you really want Axiom not to use
> the hardware for interger arithmetic but, instead go backt o Church
> numerals?  
>
> I don't.

Neither do I, but state the basic Axioms (which would be hardware 
integers or GMP) and then go from there. So commutativity in that case 
would be an axiom.

> | So it's a theorem.

> A theorem in one system, is just an axiom in another one.
> Where you start greatly depends on needs and contexts.

Right.

Ralf