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

[Gabriel Dos Reis]

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

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

| So that is saying, for each operation you have to figure out the right
| return type.

Maybe I'm dense here, but I still don't get what you're saying.

[...]

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

Yes.

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

Kind of.

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

| You get D and
| currently the only way to ask something about the type of D is
| 
|     D has CATX

yes, and that is quite limited, I know.  But, we are discussing a
system where we would like to express directly abstractions.  I don't
consider the currently crippled way of expressing things a sufficient
reason that answer my request above.

[...]

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

So?  If they do what I expect, then what is the problem?

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

[...]

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

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. 

[...]

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

Currently properties() take basic operators -- see the doc.

In in the system I see I would like properties('+ $ Integer) to report
all  registered properties of + from Integer.  A sort of typeful
version of Mathematica's Attributes[].

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

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.

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

yes, just as you declare axioms for your mathematical structures.  You
certainly don't want people to prove their axioms?

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

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.

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

| What I would like to have is to state the theorem and
| hand it to a prover (who then spits out that * is commutative).

That is good for one use of the system.  For another use, I don't
really want to go through that even I can have the system just look up
and does the job.

This is not an alien story to mathematician.  Start by assuming
something, and progress.  Latter you can prove that something from
more "primitive" blocks.  But, the real practice rarely is starts from
"primitives" and head directly to the final bits.

-- Gaby