[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Question concerning types...
From: 
Ralf Hemmecke 
Subject: 
Re: [Axiomdeveloper] Question concerning types... 
Date: 
Mon, 18 Sep 2006 14:03:49 +0200 
Useragent: 
Thunderbird 1.5.0.5 (X11/20060719) 
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 builtin. 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
 RE: [Axiomdeveloper] Question concerning types..., (continued)
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types...,
Ralf Hemmecke <=
 [Axiomdeveloper] equal or unequal (was: Question concerning types...), Ralf Hemmecke, 2006/09/18
 [Axiomdeveloper] Re: equal or unequal (was: Question concerning types...), Gabriel Dos Reis, 2006/09/18
 [Axiomdeveloper] Re: equal or unequal, Ralf Hemmecke, 2006/09/18
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Bertfried Fauser, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18