[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
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.
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)
http://www.cs.nott.ac.uk/~pni/Papers/adt-functors.pdf
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
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.
- Re: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Gabriel Dos Reis, 2006/11/13
- FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Bill Page, 2006/11/13
- Re: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Gabriel Dos Reis, 2006/11/13
- RE: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Bill Page, 2006/11/13
- Re: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Gabriel Dos Reis, 2006/11/14
- RE: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Bill Page, 2006/11/14
- Re: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Gabriel Dos Reis, 2006/11/14
- RE: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory), Page, Bill, 2006/11/14
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/14
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/14
- [Axiom-developer] RE: FW: data structure vs. mathematical structure,
Page, Bill <=
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/15
- Re: [Axiom-developer] Re: FW: data structure vs. mathematical structure, Martin Rubey, 2006/11/15
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/15
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Ralf Hemmecke, 2006/11/15
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
- [Axiom-developer] RE: FW: data structure vs. mathematical structure, Page, Bill, 2006/11/15
- [Axiom-developer] Re: FW: data structure vs. mathematical structure, Gabriel Dos Reis, 2006/11/15
- Re: [Axiom-developer] RE: FW: data structure vs. mathematical structure, Martin Rubey, 2006/11/15