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. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
