On Wednesday 13 September 2006 11:56 pm, Page, Bill wrote: > I think that this is so far past our current skill level and > the available resources that there is virtually no chance that > this will ever be anything but a paper exercise.
I think it MIGHT be possible for us to make SPAD support the key feature or two we want from Aldor (type behavior, etc.) but even if we do that, we are still faced with the problem that SPAD as a language in Axiom does not have any really good foundation as a documented language. I guess my question to those of us looking to improve SPAD is this - even if we can change it to support the feature or two we need, how do we document the language? Do we have the resources to make a really formal definition? How do we tie those definitions to something that a theorem prover could use? > If we have to live without Aldor then I think we would be much > better off looking at possibilities such as how to make Ocaml > or Haskell work with Axiom. Ocaml at least is heavily used in > proof systems and has a syntax and object model not too > different from SPAD and Aldor. Bill, do you have experience with Ocaml? Apparently Ocaml and Axiom are not completely unaware of each other as projects: http://caml.inria.fr/pub/ml-archives/caml-list/2005/07/cf19927bddbdfdbb6a062bb9f56262e9.en.html and apparently there has been some earlier discussion of languages + mathematical "fitting": http://listserv.acm.org/scripts/wa.exe?A2=ind0206c&L=oscas&P=481 Since my guess is some of the people on the list now were involved in these earlier discussions, perhaps they can give us an idea of what might be the pros and cons of using Ocaml or Haskell to re-implement our spad code. There are some earlier discussions of Ocaml on the list: http://lists.nongnu.org/archive/html/axiom-developer/2005-10/msg00204.html Possibly relevant to this discussion: there has been somewhere some work with COQ and Axiom: http://www.emis.de/proceedings/MKM2001/hardin.ps This is probably one of the documents we should look at first, but I don't know how to obtain a copy: 1. G. Alexandre. D’Axioma Zermelo. Ph. D. Thesis, University of Paris 6, LIP6, February 1998. To the best of my searching abilities, it's not currently online. I suppose a copy might be ordered from the University? Personally, I am not so afraid of the idea of translating our code, since I believe the effort required to understand and document properly what is there is going to be almost the same amount of effort as a re-write. Hopefully the interp framework is reasonably language independent (after all we can plug in Aldor - which is a separate implementation of a language, even if similar to SPAD - already). Since to make files fully literate we need to not only understand the code but the origins and definitions of the algorithms being implemented, we are looking at a massive effort to spruce up the algebra code no matter which way we go on the programming language side. I suspect (although I could be wrong) that understanding and documenting properly the design considerations and mathematical theory behind the SPAD code will be such a large effort that the language considerations become secondary, except for the question of what language has the most potential for benefiting us at the 30 year horizon. Cheers, CY _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
