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

[Page, Bill]

On Wednesday, November 15, 2006 7:39 PM Ralf Hemmecke wrote:
> 
> On 11/16/2006 01:20 AM, Gabriel Dos Reis wrote:
> > | > The definition you gave is it: least fixed point of
> > | >     X |-> 1 + T × X × X
> > | 
> > | Hmmm, good question. In Aldor-combinat (AC) we deal with 
> > | combinatorial species. They encode actual structures. The
> > | corresponding generating series G(x) for binary trees given
> > | by your X above has to fulfil the equation
> > | 
> > | G(x) = 1 + x * G(x) * G(x)                           (+)
> > ... 
> > | Assuming that I understand a bit of the theory of species,
> > | then there is only *one* solution to
> > | 
> > |       X = 1 + T * X * X.
> > | 
> > | We are not yet dealing with "virtual species" which would
> > | allow negative coefficients in the generating series.
> > 
> > I realize my sentence could be ambiguous:  I meant "least 
> > fixed point in the category of continuous partial orders
> > (CPO)."
> 
> Well, it seems you have to be even more precise. I still
> cannot understand that. You mean X, 1, T are continuous
> partial orders? And what does then + and × stand for?
> 

It is indeed a remarkable achievement of the level of abstraction
that these formulas are (nearly) identical but refer to seemingly
very different things!

>From a categorical perspective, the + and × above stand for
abstract direct sum and direct product like the disjoint union
and cartesian product of intuitive set theory. Or you can read
the same equation like a production rule in a grammar (universal
algebra) and then + denotes an altenative construction and ×
denotes a pair (or triple as in the case above). The X denotes
a "production". And the general abstract solution is represented
by a particular structure preserving operation called a functor
which in the example above can be thought of as mapping types
into more complex type structures - lists and binary trees -
this is also called a "functor" or type constructor in Axiom
and Aldor.

>From the point of view of combinatorics (counting structures)
these operations behave just like the usual arithmetic ones,
so we also have the interpretation to which you referred as
the solution of a numerical quadratic equation.

The reference to complete partial orders is a way to define an
ordering or "size" of the solutions of the equation so that it
makes sense to speak of the (unique) "least" or "greatest"
solution.

http://en.wikipedia.org/wiki/Complete_partial_order

(Depending on the application the adjective "continuous"
might also be applicable.)

There are other ways to achieve effectively the same thing
in category theory via universal constructions such as limits
and co-limits. The most important thing is to be able to
define abstractly the essential characteristics of the + and
× operations.

>From my point of view, the best way to understand least fixed
points is to also try to understand greatest fixed points at
the same time. As I mentioned in a previous message the Stream
type in Axiom (and some other languages) is related to the
same defining equation as the List functor X = 1 + T * X
except that it is greatest fixed point solution rather than
the least fixed point. It is seems easy (trivial?) to understand
the action of the List type constructor but it is a little more
challenging to understand the Stream constructor. Playing with
Stream in Axiom makes this a little easier.

In particular Streams are possibly infinite types corresponding
to possibily repeating sequences of things of a given Type. For
example

    expand(1..)

is the sequence of PositiveIntegers. And

   repeating [1,2,3]

is a sequence of those three Integers repeated 1,2,3,1,2,3,...
indefinitely. In Axiom such infinite repeating sequences have
a convenient finite representation as a circular list (denoted
by a bar over the list of repeated elements).

Now having thought about Stream as a type constructor solution
of the equation X = 1 + T * X, I would like to ask you what you
think might be the equivalent greatest fixed point solution of

  X = 1 + T * X * X

Recall first that the least fixed point solution corresponds to
the BinaryTree type constructor.

I think I know the answer although I have not seen this written
anyware else, so I want to see if you come to the same conclusion.
:-) Ultimately it is the connection to Azcel and Jon Barwise's
notions of non-wellfounded sets that intrigues me most. 

Please forgive me for going on about this ...

Regards,
Bill Page.