[Axiom-developer] RE: [Aldor-l] Type: Type

[Page, Bill]

On Tuesday, August 29, 2006 6:03 AM Gabriel Dos Reis wrote:
>>> At the logical level, as I have observed some time ago, there
>>> is an inconsistency problem with Type:Type.  I'm wondering how
>>> Aldor gets away with that.  Many languages (mostly functional)
>>> use stratified types.

On Tue, Aug 29, 2006 at 12:42:04PM +0200, Ralf Hemmecke wrote:
>> Can you construct a paradox that demonstrates the problem in
>> terms of Aldor code? To me it looks like the class (not set)
>> of all classes. Would there be a problem in class theory?

On Tuesday, August 29, 2006 8:52 AM Stephen Watt wrote:
> 
> You are correct that there is a potential inconsistency.
> 
> We avoid Russel's paradox by limiting the operations for
> constructing and testing membership in type categories.
> ...

I think the fact that Aldor defines the type of Type as Type
is very interesting from a theoretical point of view and that
it is not correct to suggest that it implies any inconsistency
or even necessarily any fundamental limitation.

In mathematics it is often necessary to deal formally with
"very large" objects, for example, to be able to reason and
compute with things like streams and formal series or for that
matter even objects such as exact real numbers. These things
do not have simple finite representations inside the computer
yet we do have means to manipulate such objects in the Aldor
and Axiom libaries. Even larger objects such as categories and
the category of all categories can be effectively represented.

Non-well-founded set theory deals specifically with this kind
of situation. (Note: The term "non-well-founded" should not be
interpreted pejoratively, in the same way "imaginary" does not
imply any algebraic defect in reference to a number.)

http://en.wikipedia.org/wiki/Non-well-founded_set_theory

I am particularly fond of the book by Barwise and Moss:
Vicious Circles: on the mathematics of circular phenomena,
CSLI Lecture Notes, 1996.

An earlier but very important reference is the book by
Peter Aczel, Non-Well-Founded Sets. Center for the Study of
Language and Information, CSLI Lecture Notes no. 14, 1988.

http://standish.stanford.edu/pdf/00000056.pdf

One of the ways of axiomatizing non-well-founded sets is via
"accessible pointed graphs". It seems to me that these graphs
also provide an excellent model for Types in Aldor and Axiom.

This is particularly evident in the Axiom library where there
are many inherent circular dependencies. Given the presence of
circulary dependencies and the potential for mutual recursion,
fixed point methods seem especially appropropriate for compiling
the Axiom library. It seems that the SPAD language leaves no
alternative to this process, but Aldor is able to compile some
mutually recursive definitions when they occur in the same source
file. And post-facto extension makes many (most?) cases of mutual
recursion over larger groups of library modules unnecessary. It
remains to be determined whether this is sufficient to implement
Axiom's library without any essential compromises.

http://wiki.axiom-developer.org/MutualRecursion

Further, it seems to me that in principle the concept of
bi-simulation introduced in the theory of non-well-founded sets
might provide an effective definition of equivalence for Aldor's
types.

Regards,
Bill Page.