[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Aldor and Lisp
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] Aldor and Lisp 
Date: 
20 Oct 2005 07:43:14 +0200 
"Page, Bill" <address@hidden> 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 typesaspropositions 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/axiomdeveloper/200509/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 typesaspropositions: 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/
 coalgebraic terms. There is quite a large literature about
 equational proof methods.

 Lately I have been reading the book "Vicious Circles: On the
 Mathematics of NonWellfounded Phenomena" by Barwise and Moss.
 It seems clear that set theory based on the antifoundation
 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, coalgebras and corecursion
 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
semanticsbased transformations where symbolic manipulations are keys
 and arrived to the nonwellfounded 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 nonwellfoundedness of it's type
 system. In this sense nonwellfoundedness 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
 Re: [Axiomdeveloper] Aldor and Lisp, (continued)
 RE: [Axiomdeveloper] Aldor and Lisp, Page, Bill, 2005/10/19
 RE: [Axiomdeveloper] Aldor and Lisp, Page, Bill, 2005/10/19
 RE: [Axiomdeveloper] Aldor and Lisp, Page, Bill, 2005/10/19
 RE: [Axiomdeveloper] Aldor and Lisp, Page, Bill, 2005/10/19
 RE: [Axiomdeveloper] Aldor and Lisp, Page, Bill, 2005/10/19
 Re: [Axiomdeveloper] Aldor and Lisp,
Gabriel Dos Reis <=
 RE: [Axiomdeveloper] Aldor and Lisp, Weiss, Juergen, 2005/10/21
 RE: [Axiomdeveloper] Aldor and Lisp, Weiss, Juergen, 2005/10/21