[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 12:14:41 +0200 
Useragent: 
Thunderbird 1.5.0.5 (X11/20060719) 
On 09/17/2006 09:18 PM, Gabriel Dos Reis wrote:
Ralf Hemmecke <address@hidden> writes:
[...]
 Looking at it mathematically (and simplified) then all we do is that
 we take a universal algebra D = (A, F) where A is the carrier set and
 F are the functions on it. Variable(D) is maybe a bad name, but all we
 do is that Variable(D) = (A', F') is a universal algebra where A' is
 the union of the set A, a set X of indeterminates, and all things that
 can be generated from A and X by applying functions from F'. F and F'
 behave identically on A.
yes.
 Mathematically, that's not a big deal. But Aldor domains are actually
 multisorted algebras. That makes the situation a little more
 complicated.
but not impossible.
In this discussion, I'm going to ignore Aldor for a moment and
concentrate on SPAD because I don't have access to Aldor source code
and anything that might transpire out of this discoussion should
probably be recorded as a featurerequest for SPAD with all the
"insights" we might have gained.
That's OK for me. But it is easier for me to speak Aldor, because it has
a reasonable language description. I am not at all fluent in SPAD, so
maybe we need a translator sometimes.
 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). In Integer you would have
+: (%, %) > %;
in Variable(Integer) you'd have
+: (%, %) > FreeMonoid %;
So that is saying, for each operation you have to figure out the right
return type. And since the signatures belong to the argument of the
function "Variable", you'd have to build a universal constructor
("Variable") that does this for arbitrary arguments.
Good luck to figure out the return type foo for Variable(MyInteger) and
MyInteger: IntegerType with {foo: %>%} == Integer add {foo(x:%):%==x}
> I don't like Indefinite(Integer) neither. So, it might very
well be that we're back to our old beloved friend Expression(Integer).
No, definitely not. The difference to Expression Integer is that the
"Integer" in the argument says something about the coefficients in the
internal representation (Remember Axiom stores Expression(D) as a
quotient of multivariate polynomials over D in "kernels" as variables.)
So Expression(D) does NOT say anything about the variables. In fact, I
believe that the argument of Expression is more or less only there for
technical reasons. The domains Expression(Integer) and Expression(Float)
or Expression(AlgebraicNumber) are all different. But an element of
Expression SUP Integer
could as well live in Expression Integer. Expression in Axiom is a way
to remove type information. Good for interactive stuff, but I still
believe that people should be more specific (ie add appropriate types)
when they write libraries.
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. So the
whole expression whould typecheck. It's a kind of TypedExpression
domain. Expression and TypedExpression looks similar to lamda calulus
and typed lambda calculus to me.
 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.
Remember, Aldor does not have reflection. You get D and currently the
only way to ask something about the type of D is
D has CATX
Of course that is not useful since you'd have to know the exports of D
at the time you write the program. That's much too early.
 One must know the type of D
 (a category) so that the return type would be clear.

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

 The ??? should be something that allows arbitrary expressions formed
 from D, the functions in C and some indeterminates X. (I have no idea
 how that would look like. Maybe just delayed evaluation of function
 composition.)
I suspect I'm being dense here. What would be wrong with Expression D?
As explained above, Expression D is NOT what you want.
 >  (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. 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.
I quite like the distinction in the abstract of
http://portal.axiomdeveloper.org/refs/articles/TheUnknownInComputerAlgebra.dvi
Above a1,a2,a3,a4, and m are "programming variables" and interestingly
there is actually no "mathematical symbol" specified above. The axiom
interpreter now is smart and treats (1) as a definition of symbols that
are called by the same name.
You see the difference if you type
)clear all
a1: Expression Integer := B
 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 builtin. That would be something that I would not
really like. The compiler and the interpreter should not know about
mathematics. You can easily implement Expression as a library package
and that is where it belongs.
 Drop "Expression" from above, what
 would be on screen for "stdout << m(1,1)"?
well, it Expression is dropped then we're back to the interpretation
we all agree on: A value of type Quaternion Fraction Integer.
Consequently m(1,1) must hold value of that type.
OK.
 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?
 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.
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. If you start with the Peano
Axioms then commutativity is not a declaration it requires a proof. So
it's a theorem. What I would like to have is to state the theorem and
hand it to a prover (who then spits out that * is commutative).
 > In fact I don't want the interpret to become
 > super smart. Just lift operations.

 I am completely with you. The interpreter should not have any
 mathematical knowledge, just look into a database (basically the Axiom
 libraries) and figure out what could be done. It should be possible to
 change the libraries and work with the same interpreter.
yes.
Good to hear that we are on the same side.
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 <=
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 [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