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

[Bill Page]

Ralf,

> On September 18, 2006 12:02 PM Bill Page wrote:
> ...
> > What you call "delayed evaluation" (in a computer science sense)
> > has something to do with universal algebra in a a mathematical
> > sense. We need a mathematics (algebra) "large enough" to express
> > this notion.
> 

On September 18, 2006 4:56 PM Ralf Hemmecke wrote:
> Right. Let's make it clearer. Suppose we just take one operation.
> For simplicity let's take +. Let's take the Integers Z as a 
> carrier set and define the universal algebra U = (Z, +) where
> + works on Z as usual. Let us introduce just one indefinite integer
> x. That means we form (Z', +') where Z' is a superset of Z and +'
> restricted to Z is +. Z' is the term algebra constructed from
> Z union {x}  and the function symbol +' where it is understood
> that u+'v is always replace by the actual integer sum u and v if
> they are both elements of Z.
> 
> If you want more indefinite integers, then iterate that process.
> 
> Who would be satisfied with such a way of modelling indefinite
> integers and who would not?

I am very well satisfied with what you wrote above. :-)

> ... 
> > In Axiom I can write:
> > 
> > (1) -> a1:POLY INT
> >        Type: Void
> > ... 
> > Should we say that 'a1' represents an indefinite integer? 
> > Tentatively, I think so.
> 
> Well, I would agree, if the interpreter knows how to deal with
> such "programming variables" that have no values, but neither
> SPAD nor Aldor understand that.

I disagree with the term "programming variable" and also that
SPAD and Aldor do not understand this. And I now also disagree
with my tentative conclusion above: 'a1' is *not* a very good
model for an indefinite integer.

> 
> Have you ever typed
> 
> foo(n: Integer): Expression Integer ==
>   (k: Expression(Integer); n*k)
> foo 1
> 
> into Axiom? (Save your session before doing it.)
>

What I get is "memory may be damaged". This is quite understandable
since k is local to the function and you are trying to use it
as part of an Expression that is returned to the main line. Try this
instead:

(1) -> k: POLY(Integer)
       Type: Void
(2) -> foo(n: Integer): POLY Integer == (n*k)
   Function declaration foo : Integer -> Polynomial Integer has been
      added to workspace.
       Type: Void
(3) -> foo 1
   Compiling function foo with type Integer -> Polynomial Integer

   (3)  k
        Type: Polynomial Integer
 
> >> But Expression is not what solves the "indefinite" problem.
> > 
> > You are right. Expression is too general. Not all objects in
> > 'Expression Integer' evaluate to Integer.
> 
> No, that is not the problem.
> ...

You are right, most of the rest of what I wrote in that email
is wrong. :(

I think the only thing I can salvage from my thoughts so far in
this thread is that in Axiom "indefinite integers" need to be
members of some domain and that domain is not so different from
'Polynomial Integer' but there needs to be some more specific
structure.

Right now I am thinking:

(1) -> a:MPOLY([a],INT)

looks like the kind of universal algebra that you describe above.
Clear MPOLY([a],INT) is a superset of INT and +$MPOLY([a],INT)
extends +$INT in an appropriate way.

Consider:

(2) -> a1:MPOLY([a1,a2],INT)
       Type: Void

(3) -> a2:MPOLY([a1,a2],INT)
       Type: Void

for example as a possible representation of such a domain involving
two indefinite integers.



Regards,
Bill Page.