Re: [Axiom-developer] Aldor and Lisp

[Gabriel Dos Reis]

"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 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