[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Page, Bill
Subject: [Axiom-developer] RE: FW: data structure vs. mathematical structure
Date: Wed, 15 Nov 2006 05:36:41 -0500

Ralf Hemmecke <address@hidden> writes:
> [...]
> | ++ A set over a domain D models the usual mathematical notion of
> | ++ a finite set of elements from D.
> | 
> | Although
> | 
> | i: Integer
> | 
> | and
> | 
> | s: FinitePowerSet T
> | 
> | would be in perfect analogy if one read ":" as "element of", then
> | to go on "l: List T" would mean "List" is the container of all
> | finite sequences (with some information about their representation
> | (linked list)).

On Tuesday, November 14, 2006 8:30 PM Gaby wrote:
> 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

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.

There is also a recent paper by Pablo Nogueira

  When is an Abstract Data Type a Functor? (31 Oct 06)
  7th Symposium on Trends in Functional Programming (TFP'06)

It contains a lot of references to Haskell and some category theory
but most of what it says about ADTs can also be applied to Axiom.

See also

> However, the existence of 1.. in Axiom would suggest that actually
> some people think of List as the greatest fixed point.

I don't think so.

In Axiom 1.. is called a UniversalSegment or a "Segment which may
be half open". Open segments can be expanded as Streams.

(1) -> expand(1..)

   (1)  [1,2,3,4,5,6,7,8,9,10,...]
                                             Type: Stream Integer

Formally Streams are defined as the greatest fixed point of the

   X |-> T x X

Streams are like Lists but can be infinite. Axiom has both lists and
streams. E.g.

(2) -> generate(x+->nextItem(x),0)$Stream(INT)

   (2)  [0,1,- 1,2,- 2,3,- 3,4,- 4,5,...]
                                             Type: Stream Integer

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]