axiom-developer
[Top][All Lists]

## [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

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

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

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
http://www.cs.nott.ac.uk/~pni

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.

http://www.cs.nott.ac.uk/~pni/Papers/index.html

>
> 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
functor

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

Regards,
Bill Page.

```