"Page, Bill" <[EMAIL PROTECTED]> writes: | On Wednesday, October 19, 2005 1:09 AM Gaby wrote: | > | > My current work on designing and implementing a general, | > efficient, scalable, complete representation of ISO C++ (with | > concepts) in C++ has led me to look at the materials on proof | > techniques in Axiom. I've read claims that Type:Type is | > inconsistent with types-as-propositions stance. I'm curious | > to learn how the type/proof techniques in Aldor would get | > away with that. | > | | I think this is a very interesting question. It relates also | to an email exchange a few weeks ago between Peter Broadbery, | Ralf Hemmecke, Tim Daly, me and a few others concerning the | structure of the upper levels of Axiom's type system. | | http://lists.gnu.org/archive/html/axiom-developer/2005-09/msg00225.html | | I think that our conclusion was (at least it was my view :) that | Axiom's concept of Category as the type of Domain and Type as a | Category is not implemented consistently in the current system.
Thank you very much for the links! Obvsiouly, I have not been paying enough attention to the axiom mailing list traffic :-( [...] | Now specifically about the idea that "Type is a Type" might | be inconsistent with types-as-propositions: I think that this | is true only in the most restricted definition of what one | means by a proposition. Certainly under this definition Type | is too "large" to be a Set. But this does not mean that we | cannot reason about it's properties using other formal methods, | for example by means of equational logic in purely algebraic/ | co-algebraic terms. There is quite a large literature about | equational proof methods. | | Lately I have been reading the book "Vicious Circles: On the | Mathematics of Non-Well-founded Phenomena" by Barwise and Moss. | It seems clear that set theory based on the anti-foundation | axiom (AFA) should, in principle provide formal proof methods | for dealing with objects such as Aldor's Type. But I do not | know of any specific research in this area. In addition, the | book discusses the generalization of AFA to greatest fixed | points, systems of equations, co-algebras and co-recursion | which provide formal methods of reasoning about types such as | streams, generators and iterators. Funny we arrived to the same sources through totally different roads :-) After we designed the IPR and decided that a type is an expression, therefore has a type (which is itself), I was worried about its soundness -- IPR is intended to support program static analysis and semantics-based transformations where symbolic manipulations are keys -- and arrived to the non-well-founded literature. I've seen the reference to "Vicious Circles" several times but did not get to read it. I guess now is a good time. Thanks for the wrapup. | It seems plausible to me to suppose that a large part of the | mathematical expressiveness of the Axiom and Aldor languages | is due to the apparent non-well-foundedness of it's type | system. In this sense non-well-foundedness is a good thing: | it makes it seem more likely that Type is "large enough" to | contain to "all of mathematics" (whatever we might want that | to mean :). | | I hope some of the contents of this email are useful to you | and I look forward to hearing your views about Type:Type. Sure your message is helpful and I will certainly send more comments once I've made enough progress with the "problem" that appears to be common to both Axiom/Aldor and IPR. Thanks! -- Gaby _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
