Re: Axiom git
Tim Daly <[email protected]> Mon, 13 Feb 2023 14:42:12 -0500
| Newsgroups | gmane.comp.mathematics.axiom.devel |
|---|---|
| Message-ID | <CAJn5L=Kz=hEeuCQJuO2TX2oAw9KBA18W4_o_mbPYKQPTEPDqJg@mail.gmail.com> |
--000000000000d4e42705f49a0b86 Content-Type: text/plain; charset="UTF-8" Camm, The "next generation" of Axiom has a few goals that is significantly reshaping the whole project. I call the effort SANE (a synonym of rational, judicious, sound, rational). I gave a talk about it at Notre Dame a few years ago (pre-covid). There are two streams of mathematical development that seem to be related but have only James Davenport in common, at least from my survey of the last 25 years of publications. One stream is computer algebra, the other is proof theory (e.g. COQ, LEAN, etc.). The proof people can't trust the computer algebra stream since, while some of the algorithms such as Buchberger's Groebner basis have been proven, most of the computer algebra is ad-hoc. The computer algebra stream seems unaware of the proof work. While truly impressive algorithms have been developed they tend to have the "it works for me" level of test and validation. MERGING proof and computer algebra My current effort merges LEAN [0] and Axiom. There is the usual Axiom hierarchy (category/domain/package) and a parallel hierarchy containing definitions, theorems, and proofs. Each function in Axiom inherits from both. This allows Axiom's group theory scaffold to be placed on proven grounds, usable in the proof of the functions. (Axiom builds a separate subtree containing all of Axiom's functions at the moment). Additionally, the REP representation of the domain is now broken out into a separate chain since the representation has its own associated theorems, again usable in the proof of the functions. Axiom is rather strongly typed but post-IBM development of type theory has moved to dependent types [1]. This allows for much more precise type specifications. DEPENDENT TYPE extensions of Axiom's types One interesting thing about my type theory efforts in Axiom is that a type computation can involve all of lisp and other Axiom algorithms. A dependent type might even be recursive, which raises issues of finding the fixed point to end the recursion. It is a challenge to manage the complexity (but endless fun). That said, since the types express the associated theorems, they become available for proving functions in the domain. More precise type information gives better, shorter, and more focused proof trees. LISP I've been doing the work using CLOS. I've moved the Axiom hierarchy into a CLOS class tree format. The top level of Axiom is now using lisp syntax rather than SPAD. I might put a SPAD language cover over the whole of it. Currently SPAD doesn't have the necessary syntax to handle dependent types or logic. It is hard enough getting things working without worrying about reworking the compiler to create "syntactic sugar". As Axiom has shown, a separate compiler / interpreter has subtle issues. Using lisp as the "top level" has two rather useful effects. First, the interpreter and compiler are the same so the current Axiom issue goes away. Second, all of the lisp tools are available and make sense rather than some random error message from the Axiom algorithm. There is also the issue of "trust". I've been working to push the "trusted code", aka the compiler output "all the way down to the metal". In the instance, that means pushing the generated code down to run on an FPGA hardware base that offers support for the generated code. RISC-V[2] soft core cpu work has made this much easier. RISC-V allows for "extended instructions" which can be dynamically defined to support specific workloads (in this case, Axiom). The FPGA tool chain for small chips works well. Note that Intel (which bought Altera) and AMD (which bought Xilinx) have CPUs which include a native FPGA. Unfortunatly they are only available to data centers. I expect this to change in the future. Ultimately the system is designed to be "trusted" from the metal to the top-level algorithms. I've been experimenting with sending the proof along with the runtime code. Checking a proof is much faster and easier than the initial proof. This allows the proof to run on a separate processor checking the result using the specific values known at runtime. The idea of "proof carrying code" is not new but interesting in this new context. STEELE's book As an aside, I published a hypertex version of Steele's book a few years ago. It used to be on my server until someone attacked and destroyed my server. A copy, with the associated latex sources is online here [3]. Anyway, I've been thinking of building a new version of the book that contains things like "pre-conditions", "post-conditions", and "invariants" for each of the lisp functions. People using lisp could have these available for program validation. OPEN SOURCE Having released Axiom as open source I learned a few lessons. One is that not everyone agrees with and works toward the published project goals. Another is that a community is rather fragile and easily collapsed. A third is that I am not suited for "management" and should not try to lead a project. You'll notice that I've stopped updating the Axiom source tree. I thought FOSS development was a great idea when I started in 1997. The Axiom effort has convinced me otherwise. I've stopped working in "open source". GITHUB If you know the commands to give you write access I'd be happy to enable you. Please let me know how. Again, many thanks for your work. Tim [0] LEAN https://leanprover-community.github.io/ [1] Dependent Types: https://en.wikipedia.org/wiki/Dependent_type [2] RISC-V https://riscv.org/ [3] Hyperlinked Steele's book: https://www.softwarepreservation.org/projects/LISP/common_lisp_family On Mon, Feb 13, 2023 at 9:38 AM Camm Maguire <[email protected]> wrote: > Greetings! > > Tim, is it your intention that github serves as the official repository > henceforward? Are you intending to tag releases here, and/or push > tarballs to the website? Debian axiom is using sources from 20170501, > which were available back then in tar form but seem to be gone now. Are > you planning any further releases? > > It seems your goals are very ambitious. It may be worthwhile making > sure the tree is periodically and incrementally kept up to date and > releasable as you move forward, say once a year or so. If you would > like to grant me access to the tree (github id cammgh), I can volunteer > to maintain the gcl interface if desired. > > Take care, > -- > Camm Maguire [email protected] > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > --000000000000d4e42705f49a0b86 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div>Camm,</div><div><br></div><div>The "next generat= ion" of Axiom has a few goals that is significantly</div><div>reshapin= g the whole project. I call the effort SANE (a synonym of <br></div><div>ra= tional, judicious, sound, rational). I gave a talk about it at Notre</div><= div>Dame a few years ago (pre-covid).<br></div><div><br></div><div>There ar= e two streams of mathematical development that seem to be</div><div>related= but have only James Davenport in common, at least from my <br></div><div>s= urvey of the last 25 years of publications. One stream is computer</div><di= v>algebra, the other is proof theory (e.g. COQ, LEAN, etc.).</div><div><br>= </div><div>The proof people can't trust the computer algebra stream sin= ce, while</div><div>some of the algorithms such as Buchberger's Groebne= r basis have <br></div><div>been proven, most of the computer algebra is ad= -hoc.</div><div><br></div><div>The computer algebra stream seems unaware of= the proof work.</div><div>While truly impressive algorithms have been deve= loped they tend to</div><div>have the "it works for me" level of = test and validation.</div><div><br></div><div>MERGING proof and computer al= gebra<br></div><div><br></div><div>My current effort merges LEAN [0] and Ax= iom. There is the usual</div><div>Axiom hierarchy (category/domain/package)= and a parallel hierarchy</div><div>containing definitions, theorems, and p= roofs. Each function in Axiom</div><div>inherits from both. This allows Axi= om's group theory scaffold to be</div><div>placed on proven grounds, us= able in the proof of the functions.</div><div>(Axiom builds a separate subt= ree containing all of Axiom's functions <br></div><div>at the moment).<= br></div><div><br></div><div>Additionally, the REP representation of the do= main is now broken out<br></div><div>into a separate chain since the repres= entation has its own associated</div><div>theorems, again usable in the pro= of of the functions.</div><div><br></div><div>Axiom is rather strongly type= d but post-IBM development of type</div><div>theory has moved to dependent = types [1]. This allows for much more</div><div>precise type specifications.= <br></div><div><br></div><div>DEPENDENT TYPE extensions of Axiom's typ= es<br></div><div><br></div><div>One interesting thing about my type theory = efforts in Axiom is that</div><div>a type computation can involve all of li= sp and other Axiom algorithms.</div><div>A dependent type might even be rec= ursive, which raises issues of</div><div>finding the fixed point to end the= recursion. It is a challenge to <br></div><div>manage the complexity (but = endless fun).</div><div><br></div><div>That said, since the types express t= he associated theorems, they</div><div>become available for proving functio= ns in the domain. More precise</div><div>type information gives better, sho= rter, and more focused proof trees.<br></div><div><br></div><div>LISP <br><= /div><div><br></div><div>I've been doing the work using CLOS. I've = moved the Axiom</div><div>hierarchy into a CLOS class tree format. The top = level of Axiom</div><div>is now using lisp syntax rather than SPAD. I might= put a SPAD</div><div>language cover over the whole of it. Currently SPAD d= oesn't</div><div>have the necessary syntax to handle dependent types or= logic.</div><div><br></div><div>It is hard enough getting things working w= ithout worrying about</div><div>reworking the compiler to create "synt= actic sugar". As Axiom has</div><div>shown, a separate compiler / inte= rpreter has subtle issues.<br></div><div><br></div><div>Using lisp as the &= quot;top level" has two rather useful effects. First,</div><div>the in= terpreter and compiler are the same so the current Axiom</div><div>issue go= es away. Second, all of the lisp tools are available and</div><div>make sen= se rather than some random error message from the</div><div>Axiom algorithm= .<br></div><div><br></div><div>There is also the issue of "trust"= . I've been working to push the</div><div>"trusted code", aka= the compiler output "all the way down to the</div><div>metal". I= n the instance, that means pushing the generated code</div><div>down to run= on an FPGA hardware base that offers support for</div><div>the generated c= ode. RISC-V[2] soft core cpu work has made this</div><div>much easier. RISC= -V allows for "extended instructions" which can</div><div>be dyna= mically defined to support specific workloads (in this case, <br></div><div= >Axiom). <br></div><div><br></div><div>The FPGA tool chain for small chips = works well. Note that Intel</div><div>(which bought Altera) and AMD (which = bought Xilinx) have CPUs</div><div>which include a native FPGA. Unfortunatl= y they are only available</div><div>to data centers. I expect this to chang= e in the future.<br></div><div><br></div><div>Ultimately the system is desi= gned to be "trusted" from the metal</div><div>to the top-level al= gorithms. I've been experimenting with sending</div><div>the proof alon= g with the runtime code. Checking a proof is much</div><div>faster and easi= er than the initial proof. This allows the proof to <br></div><div>run on a= separate processor checking the result using the</div><div>specific values= known at runtime. The idea of "proof carrying</div><div>code" is= not new but interesting in this new context.<br></div><div><br></div><div>= <br></div><div>STEELE's book</div><div><br></div><div>As an aside, I pu= blished a hypertex version of Steele's book a</div><div>few years ago. = It used to be on my server until someone attacked</div><div>and destroyed m= y server. A copy, with the associated latex sources</div><div>is online her= e [3].<br></div><div><br></div><div>Anyway, I've been thinking of build= ing a new version of the book that <br></div><div>contains things like &quo= t;pre-conditions", "post-conditions", and "invariants&q= uot; <br></div><div>for each of the lisp functions. People using lisp could= have these <br></div><div>available for program validation.</div><div><br>= </div><div><br></div><div>OPEN SOURCE</div><div><br></div><div>Having relea= sed Axiom as open source I learned a few lessons.</div><div><br></div><div>= One is that not everyone agrees with and works toward the</div><div>publish= ed project goals. Another is that a community is</div><div>rather fragile a= nd easily collapsed. A third is that I am not</div><div>suited for "ma= nagement" and should not try to lead a project.</div><div><br></div><d= iv>You'll notice that I've stopped updating the Axiom source tree.<= /div><div>I thought FOSS development was a great idea when I started</div><= div>in 1997. The Axiom effort has convinced me otherwise.<br></div><div>I&#= 39;ve stopped working in "open source".</div><div><br></div><div>= GITHUB</div><div><br></div><div>If you know the commands to give you write = access I'd be</div><div>happy to enable you. Please let me know how.</d= iv><div><br></div><div>Again, many thanks for your work.<br></div><div><br>= </div><div>Tim</div><div><br></div><div><br></div><div><br></div><div>[0] L= EAN <a href=3D"https://leanprover-community.github.io/">https://leanprover-= community.github.io/</a></div><div><br></div><div>[1] Dependent Types: <a h= ref=3D"https://en.wikipedia.org/wiki/Dependent_type">https://en.wikipedia.o= rg/wiki/Dependent_type</a></div><div><br></div><div>[2] RISC-V <a href=3D"h= ttps://riscv.org/">https://riscv.org/</a></div><div><br></div><div>[3] Hype= rlinked Steele's book: <a href=3D"https://www.softwarepreservation.org/= projects/LISP/common_lisp_family">https://www.softwarepreservation.org/proj= ects/LISP/common_lisp_family</a></div></div><br><div class=3D"gmail_quote">= <div dir=3D"ltr" class=3D"gmail_attr">On Mon, Feb 13, 2023 at 9:38 AM Camm = Maguire <<a href=3D"mailto:[email protected]">[email protected]= g</a>> wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin= :0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"= >Greetings!<br> <br> Tim, is it your intention that github serves as the official repository<br> henceforward?=C2=A0 Are you intending to tag releases here, and/or push<br> tarballs to the website?=C2=A0 Debian axiom is using sources from 20170501,= <br> which were available back then in tar form but seem to be gone now.=C2=A0 A= re<br> you planning any further releases?<br> <br> It seems your goals are very ambitious.=C2=A0 It may be worthwhile making<b= r> sure the tree is periodically and incrementally kept up to date and<br> releasable as you move forward, say once a year or so.=C2=A0 If you would<b= r> like to grant me access to the tree (github id cammgh), I can volunteer<br> to maintain the gcl interface if desired.<br> <br> Take care,<br> -- <br> Camm Maguire=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 <a href=3D"mailto:[email protected]" target=3D"_blank">camm@maguir= efamily.org</a><br> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D<br= > "The earth is but one country, and mankind its citizens."=C2=A0 -= -=C2=A0 Baha'u'llah<br> </blockquote></div> --000000000000d4e42705f49a0b86--