[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiomdeveloper] Re: FW: data structure vs. mathematical structure
From: 
Gabriel Dos Reis 
Subject: 
[Axiomdeveloper] Re: FW: data structure vs. mathematical structure 
Date: 
15 Nov 2006 13:59:18 +0100 
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?
 > LibraryCentric 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 Axiomspeak) for free.
 The following code snipped is from AldorCombinat 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 Aldorcombinat
 available for Axiom, but for the underlying compilation we still need
 the Aldor compiler. So, Gaby, I consider Aldorcombinat a testcase for
 the compilerimprovements branch. ;)
OK, I don't feel it like a pressure :) :)
 Gaby
 RE: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), (continued)
 RE: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Bill Page, 2006/11/13
 Re: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Gabriel Dos Reis, 2006/11/14
 RE: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Bill Page, 2006/11/14
 Re: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Gabriel Dos Reis, 2006/11/14
 RE: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Page, Bill, 2006/11/14
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/14
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/14
 [Axiomdeveloper] RE: FW: data structure vs. mathematical structure, Page, Bill, 2006/11/15
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/15
 Re: [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Martin Rubey, 2006/11/15
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure,
Gabriel Dos Reis <=
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/15
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/15
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
 [Axiomdeveloper] RE: FW: data structure vs. mathematical structure, Page, Bill, 2006/11/15
 [Axiomdeveloper] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
 Re: [Axiomdeveloper] RE: FW: data structure vs. mathematical structure, Martin Rubey, 2006/11/15
 Re: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Gabriel Dos Reis, 2006/11/14
 Re: FW: data structure vs. mathematical structure (was: [Axiomdeveloper] Graph theory), Vanuxem Grégory, 2006/11/14