[Axiom-developer] Re: FW: data structure vs. mathematical structure

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| >> And that would match the usual definition of List as the least fixed
| >> point of the functor
| >>
| >>      X |-> 1 + X
| >>
| >> in CPO.
| > In case anyone is wondering what Gaby is talking about, I think the
| > following paper by Dos Reis and Jarvi:
| >   What is Generic Programming?
| >   Library-Centric Software Design LCSD'05
| > http://lcsd05.cs.tamu.edu/papers/dos_reis_et_al.pdf
| > provides a good introduction. It defines a List as the least fixed
| > point of
| >       X |-> 1 + T x X
| > Hopefully a future paper will deal more specifically with Axiom. :-)
| > In Axiom List could be defined something like this
| >   List(T:Type):ListAggregate == add
| >     Rep == Union(nil,Record(first:T,rest:%))
| >     ...
| > (perhaps it is in Aldor?) but in fact the actual definition refers
| > directly to the underlying Lisp architecture.
| 
| I had no need to define List this way, but what about binary trees?

The definition you gave is it: least fixed point of

    X |-> 1 + T × X × X


The interesting bit about those inductive definition is that they come
with "fold" (reduce in Axiom-speak) for free.

| The following code snipped is from Aldor-Combinat and it is running code.
| 
| ---BEGIN test/species.as.nw
| [snip]
| 
| testRecursive1(): () == {
|          macro {
|                  I == EmptySetSpecies;
|                  X == SingletonSpecies;
|                  + == Plus;
|                  * == Times;
|          }
| 
|          A(L: LabelType): CombinatorialSpecies L == (I + X*A*A)(L) add;
| 
|          import from Integer, Array Integer;
|          checkExpOrd(
|              A,
|              [1, 1, 4, 30, 336, 5040],
|              [1, 1, 2, 5, 14, 42]
|          );
| }
| 
| [snap]
| ---END test/species.as.nw
| 
| If you want List the line should be simply ...
| 
|    MyList(L: LabelType): CombinatorialSpecies L == (I + X*MyList)(L) add;
| 
| Well, but in LibAldor List is not defined as a real Union. It rather
| relies on the fact that an actual record can never be the nil pointer.
| 
| Oh, by the way, the above recursive definition of binary trees not
| only defines the data structure but also the exponential and ordinary
| generating series. So one could ask how many trees are there with 7
| nodes (labelled or unlabelled). I fact, it should also be possible, to
| generate all these trees.

Yes!

| 
| Recently, Martin Rubey has done some work to make Aldor-combinat
| available for Axiom, but for the underlying compilation we still need
| the Aldor compiler. So, Gaby, I consider Aldor-combinat a testcase for
| the compiler-improvements branch. ;-)

OK, I don't feel it like a pressure :-) :-)

-- Gaby