Re: Axiom musings...
Tim Daly <[email protected]> Sat, 13 Nov 2021 17:28:28 -0500
| Newsgroups | gmane.comp.mathematics.axiom.devel |
|---|---|
| Message-ID | <CAJn5L=Ln-Eh5errAZ5_Tn1CikdpFUgkCmWZff4TOg2Sd5_eCOw@mail.gmail.com> |
--00000000000001b29105d0b319e8 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Full support for general, first-class dependent types requires some changes to the Axiom design. That implies some language design questions. Given that mathematics is such a general subject with a lot of "local" notation and ideas (witness logical judgment notation) careful thought is needed to design a language that is able to handle a wide range. Normally language design is a two-level process. The language designer creates a language and then an implementation. Various design choices affect the final language. There is "The Metaobject Protocol" (MOP) https://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kiczales/dp/026261074= 4 which encourages a three-level process. The language designer works at a Metalevel to design a family of languages, then the language specializations, then the implementation. A MOP design allows the language user to optimize the language to their problem. A simple paper on the subject is "Metaobject Protocols" https://users.cs.duke.edu/~vahdat/ps/mop.pdf Tim On Mon, Oct 25, 2021 at 7:42 PM Tim Daly <[email protected]> wrote: > I have a separate thread of research on Self-Replicating Systems > (ref: Kinematics of Self Reproducing Machines > http://www.molecularassembler.com/KSRM.htm) > > which led to watching "Strange Dreams of Stranger Loops" by Will Byrd > https://www.youtube.com/watch?v=3DAffW-7ika0E > > Will referenced a PhD Thesis by Jon Doyle > "A Model for Deliberation, Action, and Introspection" > > I also read the thesis by J.C.G. Sturdy > "A Lisp through the Looking Glass" > > Self-replication requires the ability to manipulate your own > representation in such a way that changes to that representation > will change behavior. > > This leads to two thoughts in the SANE research. > > First, "Declarative Representation". That is, most of the things > about the representation should be declarative rather than > procedural. Applying this idea as much as possible makes it > easier to understand and manipulate. > > Second, "Explicit Call Stack". Function calls form an implicit > call stack. This can usually be displayed in a running lisp system. > However, having the call stack explicitly available would mean > that a system could "introspect" at the first-class level. > > These two ideas would make it easy, for example, to let the > system "show the work". One of the normal complaints is that > a system presents an answer but there is no way to know how > that answer was derived. These two ideas make it possible to > understand, display, and even post-answer manipulate > the intermediate steps. > > Having the intermediate steps also allows proofs to be > inserted in a step-by-step fashion. This aids the effort to > have proofs run in parallel with computation at the hardware > level. > > Tim > > > > > > > On Thu, Oct 21, 2021 at 9:50 AM Tim Daly <[email protected]> wrote: > >> So the current struggle involves the categories in Axiom. >> >> The categories and domains constructed using categories >> are dependent types. When are dependent types "equal"? >> Well, hummmm, that depends on the arguments to the >> constructor. >> >> But in order to decide(?) equality we have to evaluate >> the arguments (which themselves can be dependent types). >> Indeed, we may, and in general, we must evaluate the >> arguments at compile time (well, "construction time" as >> there isn't really a compiler / interpreter separation anymore.) >> >> That raises the question of what "equality" means. This >> is not simply a "set equality" relation. It falls into the >> infinite-groupoid of homotopy type theory. In general >> it appears that deciding category / domain equivalence >> might force us to climb the type hierarchy. >> >> Beyond that, there is the question of "which proof" >> applies to the resulting object. Proofs depend on their >> assumptions which might be different for different >> constructions. As yet I have no clue how to "index" >> proofs based on their assumptions, nor how to >> connect these assumptions to the groupoid structure. >> >> My brain hurts. >> >> Tim >> >> >> On Mon, Oct 18, 2021 at 2:00 AM Tim Daly <[email protected]> wrote: >> >>> "Birthing Computational Mathematics" >>> >>> The Axiom SANE project is difficult at a very fundamental >>> level. The title "SANE" was chosen due to the various >>> words found in a thesuarus... "rational", "coherent", >>> "judicious" and "sound". >>> >>> These are very high level, amorphous ideas. But so is >>> the design of SANE. Breaking away from tradition in >>> computer algebra, type theory, and proof assistants >>> is very difficult. Ideas tend to fall into standard jargon >>> which limits both the frame of thinking (e.g. dependent >>> types) and the content (e.g. notation). >>> >>> Questioning both frame and content is very difficult. >>> It is hard to even recognize when they are accepted >>> "by default" rather than "by choice". What does the idea >>> "power tools" mean in a primitive, hand labor culture? >>> >>> Christopher Alexander [0] addresses this problem in >>> a lot of his writing. Specifically, in his book "Notes on >>> the Synthesis of Form", in his chapter 5 "The Selfconsious >>> Process", he addresses this problem directly. This is a >>> "must read" book. >>> >>> Unlike building design and contruction, however, there >>> are almost no constraints to use as guides. Alexander >>> quotes Plato's Phaedrus: >>> >>> "First, the taking in of scattered particulars under >>> one Idea, so that everyone understands what is being >>> talked about ... Second, the separation of the Idea >>> into parts, by dividing it at the joints, as nature >>> directs, not breaking any limb in half as a bad >>> carver might." >>> >>> Lisp, which has been called "clay for the mind" can >>> build virtually anything that can be thought. The >>> "joints" are also "of one's choosing" so one is >>> both carver and "nature". >>> >>> Clearly the problem is no longer "the tools". >>> *I* am the problem constraining the solution. >>> Birthing this "new thing" is slow, difficult, and >>> uncertain at best. >>> >>> Tim >>> >>> [0] Alexander, Christopher "Notes on the Synthesis >>> of Form" Harvard University Press 1964 >>> ISBN 0-674-62751-2 >>> >>> >>> On Sun, Oct 10, 2021 at 4:40 PM Tim Daly <[email protected]> wrote: >>> >>>> Re: writing a paper... I'm not connected to Academia >>>> so anything I'd write would never make it into print. >>>> >>>> "Language level parsing" is still a long way off. The talk >>>> by Guy Steele [2] highlights some of the problems we >>>> currently face using mathematical metanotation. >>>> >>>> For example, a professor I know at CCNY (City College >>>> of New York) didn't understand Platzer's "funny >>>> fraction notation" (proof judgements) despite being >>>> an expert in Platzer's differential equations area. >>>> >>>> Notation matters and is not widely common. >>>> >>>> I spoke to Professor Black (in LTI) about using natural >>>> language in the limited task of a human-robot cooperation >>>> in changing a car tire. I looked at the current machine >>>> learning efforts. They are no where near anything but >>>> toy systems, taking too long to train and are too fragile. >>>> >>>> Instead I ended up using a combination of AIML [3] >>>> (Artificial Intelligence Markup Language), the ALICE >>>> Chatbot [4], Forgy's OPS5 rule based program [5], >>>> and Fahlman's SCONE [6] knowledge base. It was >>>> much less fragile in my limited domain problem. >>>> >>>> I have no idea how to extend any system to deal with >>>> even undergraduate mathematics parsing. >>>> >>>> Nor do I have any idea how I would embed LEAN >>>> knowledge into a SCONE database, although I >>>> think the combination would be useful and interesting. >>>> >>>> I do believe that, in the limited area of computational >>>> mathematics, we are capable of building robust, proven >>>> systems that are quite general and extensible. As you >>>> might have guessed I've given it a lot of thought over >>>> the years :-) >>>> >>>> A mathematical language seems to need >6 components >>>> >>>> 1) We need some sort of a specification language, possibly >>>> somewhat 'propositional' that introduces the assumptions >>>> you mentioned (ref. your discussion of numbers being >>>> abstract and ref. your discussion of relevant choice of >>>> assumptions related to a problem). >>>> >>>> This is starting to show up in the hardware area (e.g. >>>> Lamport's TLC[0]) >>>> >>>> Of course, specifications relate to proving programs >>>> and, as you recall, I got a cold reception from the >>>> LEAN community about using LEAN for program proofs. >>>> >>>> 2) We need "scaffolding". That is, we need a theory >>>> that can be reduced to some implementable form >>>> that provides concept-level structure. >>>> >>>> Axiom uses group theory for this. Axiom's "category" >>>> structure has "Category" things like Ring. Claiming >>>> to be a Ring brings in a lot of "Signatures" of functions >>>> you have to implement to properly be a Ring. >>>> >>>> Scaffolding provides a firm mathematical basis for >>>> design. It provides a link between the concept of a >>>> Ring and the expectations you can assume when >>>> you claim your "Domain" "is a Ring". Category >>>> theory might provide similar structural scaffolding >>>> (eventually... I'm still working on that thought garden) >>>> >>>> LEAN ought to have a textbook(s?) that structures >>>> the world around some form of mathematics. It isn't >>>> sufficient to say "undergraduate math" is the goal. >>>> There needs to be some coherent organization so >>>> people can bring ideas like Group Theory to the >>>> organization. Which brings me to ... >>>> >>>> 3) We need "spreading". That is, we need to take >>>> the various definitions and theorems in LEAN and >>>> place them in their proper place in the scaffold. >>>> >>>> For example, the Ring category needs the definitions >>>> and theorems for a Ring included in the code for the >>>> Ring category. Similarly, the Commutative category >>>> needs the definitions and theorems that underlie >>>> "commutative" included in the code. >>>> >>>> That way, when you claim to be a "Commutative Ring" >>>> you get both sets of definitions and theorems. That is, >>>> the inheritance mechanism will collect up all of the >>>> definitions and theorems and make them available >>>> for proofs. >>>> >>>> I am looking at LEAN's definitions and theorems with >>>> an eye to "spreading" them into the group scaffold of >>>> Axiom. >>>> >>>> 4) We need "carriers" (Axiom calls them representations, >>>> aka "REP"). REPs allow data structures to be defined >>>> independent of the implementation. >>>> >>>> For example, Axiom can construct Polynomials that >>>> have their coefficients in various forms of representation. >>>> You can define "dense" (all coefficients in a list), >>>> "sparse" (only non-zero coefficients), "recursive", etc. >>>> >>>> A "dense polynomial" and a "sparse polynomial" work >>>> exactly the same way as far as the user is concerned. >>>> They both implement the same set of functions. There >>>> is only a difference of representation for efficiency and >>>> this only affects the implementation of the functions, >>>> not their use. >>>> >>>> Axiom "got this wrong" because it didn't sufficiently >>>> separate the REP from the "Domain". I plan to fix this. >>>> >>>> LEAN ought to have a "data structures" subtree that >>>> has all of the definitions and axioms for all of the >>>> existing data structures (e.g. Red-Black trees). This >>>> would be a good undergraduate project. >>>> >>>> 5) We need "Domains" (in Axiom speak). That is, we >>>> need a box that holds all of the functions that implement >>>> a "Domain". For example, a "Polynomial Domain" would >>>> hold all of the functions for manipulating polynomials >>>> (e.g polynomial multiplication). The "Domain" box >>>> is a dependent type that: >>>> >>>> A) has an argument list of "Categories" that this "Domain" >>>> box inherits. Thus, the "Integer Domain" inherits >>>> the definitions and axioms from "Commutative" >>>> >>>> Functions in the "Domain" box can now assume >>>> and use the properties of being commutative. Proofs >>>> of functions in this domain can use the definitions >>>> and proofs about being commutative. >>>> >>>> B) contains an argument that specifies the "REP" >>>> (aka, the carrier). That way you get all of the >>>> functions associated with the data structure >>>> available for use in the implementation. >>>> >>>> Functions in the Domain box can use all of >>>> the definitions and axioms about the representation >>>> (e.g. NonNegativeIntegers are always positive) >>>> >>>> C) contains local "spread" definitions and axioms >>>> that can be used in function proofs. >>>> >>>> For example, a "Square Matrix" domain would >>>> have local axioms that state that the matrix is >>>> always square. Thus, functions in that box could >>>> use these additional definitions and axioms in >>>> function proofs. >>>> >>>> D) contains local state. A "Square Matrix" domain >>>> would be constructed as a dependent type that >>>> specified the size of the square (e.g. a 2x2 >>>> matrix would have '2' as a dependent parameter. >>>> >>>> E) contains implementations of inherited functions. >>>> >>>> A "Category" could have a signature for a GCD >>>> function and the "Category" could have a default >>>> implementation. However, the "Domain" could >>>> have a locally more efficient implementation which >>>> overrides the inherited implementation. >>>> >>>> Axiom has about 20 GCD implementations that >>>> differ locally from the default in the category. They >>>> use properties known locally to be more efficient. >>>> >>>> F) contains local function signatures. >>>> >>>> A "Domain" gives the user more and more unique >>>> functions. The signature have associated >>>> "pre- and post- conditions" that can be used >>>> as assumptions in the function proofs. >>>> >>>> Some of the user-available functions are only >>>> visible if the dependent type would allow them >>>> to exist. For example, a general Matrix domain >>>> would have fewer user functions that a Square >>>> Matrix domain. >>>> >>>> In addition, local "helper" functions need their >>>> own signatures that are not user visible. >>>> >>>> G) the function implementation for each signature. >>>> >>>> This is obviously where all the magic happens >>>> >>>> H) the proof of each function. >>>> >>>> This is where I'm using LEAN. >>>> >>>> Every function has a proof. That proof can use >>>> all of the definitions and axioms inherited from >>>> the "Category", "Representation", the "Domain >>>> Local", and the signature pre- and post- >>>> conditions. >>>> >>>> I) literature links. Algorithms must contain a link >>>> to at least one literature reference. Of course, >>>> since everything I do is a Literate Program >>>> this is obviously required. Knuth said so :-) >>>> >>>> >>>> LEAN ought to have "books" or "pamphlets" that >>>> bring together all of this information for a domain >>>> such as Square Matrices. That way a user can >>>> find all of the related ideas, available functions, >>>> and their corresponding proofs in one place. >>>> >>>> 6) User level presentation. >>>> >>>> This is where the systems can differ significantly. >>>> Axiom and LEAN both have GCD but they use >>>> that for different purposes. >>>> >>>> I'm trying to connect LEAN's GCD and Axiom's GCD >>>> so there is a "computational mathematics" idea that >>>> allows the user to connect proofs and implementations. >>>> >>>> 7) Trust >>>> >>>> Unlike everything else, computational mathematics >>>> can have proven code that gives various guarantees. >>>> >>>> I have been working on this aspect for a while. >>>> I refer to it as trust "down to the metal" The idea is >>>> that a proof of the GCD function and the implementation >>>> of the GCD function get packaged into the ELF format. >>>> (proof carrying code). When the GCD algorithm executes >>>> on the CPU, the GCD proof is run through the LEAN >>>> proof checker on an FPGA in parallel. >>>> >>>> (I just recently got a PYNQ Xilinx board [1] with a CPU >>>> and FPGA together. I'm trying to implement the LEAN >>>> proof checker on the FPGA). >>>> >>>> We are on the cusp of a revolution in computational >>>> mathematics. But the two pillars (proof and computer >>>> algebra) need to get know each other. >>>> >>>> Tim >>>> >>>> >>>> >>>> [0] Lamport, Leslie "Chapter on TLA+" >>>> in "Software Specification Methods" >>>> https://www.springer.com/gp/book/9781852333539 >>>> (I no longer have CMU library access or I'd send you >>>> the book PDF) >>>> >>>> [1] https://www.tul.com.tw/productspynq-z2.html >>>> >>>> [2] https://www.youtube.com/watch?v=3DdCuZkaaou0Q >>>> >>>> [3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE" >>>> https://arxiv.org/pdf/1307.3091.pdf >>>> >>>> [4] ALICE Chatbot >>>> http://www.scielo.org.mx/pdf/cys/v19n4/1405-5546-cys-19-04-00625.pdf >>>> >>>> [5] OPS5 User Manual >>>> >>>> https://kilthub.cmu.edu/articles/journal_contribution/OPS5_user_s_manu= al/6608090/1 >>>> >>>> [6] Scott Fahlman "SCONE" >>>> http://www.cs.cmu.edu/~sef/scone/ >>>> >>>> On 9/27/21, Tim Daly <[email protected]> wrote: >>>> > I have tried to maintain a list of names of people who have >>>> > helped Axiom, going all the way back to the pre-Scratchpad >>>> > days. The names are listed at the beginning of each book. >>>> > I also maintain a bibliography of publications I've read or >>>> > that have had an indirect influence on Axiom. >>>> > >>>> > Credit is "the coin of the realm". It is easy to share and wrong >>>> > to ignore. It is especially damaging to those in Academia who >>>> > are affected by credit and citations in publications. >>>> > >>>> > Apparently I'm not the only person who feels that way. The ACM >>>> > Turing award seems to have ignored a lot of work: >>>> > >>>> > Scientific Integrity, the 2021 Turing Lecture, and the 2018 Turing >>>> > Award for Deep Learning >>>> > >>>> https://people.idsia.ch/~juergen/scientific-integrity-turing-award-dee= p-learning.html >>>> > >>>> > I worked on an AI problem at IBM Research called Ketazolam. >>>> > (https://en.wikipedia.org/wiki/Ketazolam). The idea was to recognize >>>> > and associated 3D chemical drawings with their drug counterparts. >>>> > I used Rumelhart, and McClelland's books. These books contained >>>> > quite a few ideas that seem to be "new and innovative" among the >>>> > machine learning crowd... but the books are from 1987. I don't belie= ve >>>> > I've seen these books mentioned in any recent bibliography. >>>> > >>>> https://mitpress.mit.edu/books/parallel-distributed-processing-volume-= 1 >>>> > >>>> > >>>> > >>>> > >>>> > On 9/27/21, Tim Daly <[email protected]> wrote: >>>> >> Greg Wilson asked "How Reliable is Scientific Software?" >>>> >> >>>> https://neverworkintheory.org/2021/09/25/how-reliable-is-scientific-so= ftware.html >>>> >> >>>> >> which is a really interesting read. For example" >>>> >> >>>> >> [Hatton1994], is now a quarter of a century old, but its conclusio= ns >>>> >> are still fresh. The authors fed the same data into nine commercial >>>> >> geophysical software packages and compared the results; they found >>>> >> that, "numerical disagreement grows at around the rate of 1% in >>>> >> average absolute difference per 4000 fines of implemented code, and= , >>>> >> even worse, the nature of the disagreement is nonrandom" (i.e., the >>>> >> authors of different packages make similar mistakes). >>>> >> >>>> >> >>>> >> On 9/26/21, Tim Daly <[email protected]> wrote: >>>> >>> I should note that the lastest board I've just unboxed >>>> >>> (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD). >>>> >>> >>>> >>> What makes it interesting is that it contains 2 hard >>>> >>> core processors and an FPGA, connected by 9 paths >>>> >>> for communication. The processors can be run >>>> >>> independently so there is the possibility of a parallel >>>> >>> version of some Axiom algorithms (assuming I had >>>> >>> the time, which I don't). >>>> >>> >>>> >>> Previously either the hard (physical) processor was >>>> >>> separate from the FPGA with minimal communication >>>> >>> or the soft core processor had to be created in the FPGA >>>> >>> and was much slower. >>>> >>> >>>> >>> Now the two have been combined in a single chip. >>>> >>> That means that my effort to run a proof checker on >>>> >>> the FPGA and the algorithm on the CPU just got to >>>> >>> the point where coordination is much easier. >>>> >>> >>>> >>> Now all I have to do is figure out how to program this >>>> >>> beast. >>>> >>> >>>> >>> There is no such thing as a simple job. >>>> >>> >>>> >>> Tim >>>> >>> >>>> >>> >>>> >>> On 9/26/21, Tim Daly <[email protected]> wrote: >>>> >>>> I'm familiar with most of the traditional approaches >>>> >>>> like Theorema. The bibliography contains most of the >>>> >>>> more interesting sources. [0] >>>> >>>> >>>> >>>> There is a difference between traditional approaches to >>>> >>>> connecting computer algebra and proofs and my approach. >>>> >>>> >>>> >>>> Proving an algorithm, like the GCD, in Axiom is hard. >>>> >>>> There are many GCDs (e.g. NNI vs POLY) and there >>>> >>>> are theorems and proofs passed at runtime in the >>>> >>>> arguments of the newly constructed domains. This >>>> >>>> involves a lot of dependent type theory and issues of >>>> >>>> compile time / runtime argument evaluation. The issues >>>> >>>> that arise are difficult and still being debated in the type >>>> >>>> theory community. >>>> >>>> >>>> >>>> I am putting the definitions, theorems, and proofs (DTP) >>>> >>>> directly into the category/domain hierarchy. Each category >>>> >>>> will have the DTP specific to it. That way a commutative >>>> >>>> domain will inherit a commutative theorem and a >>>> >>>> non-commutative domain will not. >>>> >>>> >>>> >>>> Each domain will have additional DTPs associated with >>>> >>>> the domain (e.g. NNI vs Integer) as well as any DTPs >>>> >>>> it inherits from the category hierarchy. Functions in the >>>> >>>> domain will have associated DTPs. >>>> >>>> >>>> >>>> A function to be proven will then inherit all of the relevant >>>> >>>> DTPs. The proof will be attached to the function and >>>> >>>> both will be sent to the hardware (proof-carrying code). >>>> >>>> >>>> >>>> The proof checker, running on a field programmable >>>> >>>> gate array (FPGA), will be checked at runtime in >>>> >>>> parallel with the algorithm running on the CPU >>>> >>>> (aka "trust down to the metal"). (Note that Intel >>>> >>>> and AMD have built CPU/FPGA combined chips, >>>> >>>> currently only available in the cloud.) >>>> >>>> >>>> >>>> >>>> >>>> >>>> >>>> I am (slowly) making progress on the research. >>>> >>>> >>>> >>>> I have the hardware and nearly have the proof >>>> >>>> checker from LEAN running on my FPGA. >>>> >>>> >>>> >>>> I'm in the process of spreading the DTPs from >>>> >>>> LEAN across the category/domain hierarchy. >>>> >>>> >>>> >>>> The current Axiom build extracts all of the functions >>>> >>>> but does not yet have the DTPs. >>>> >>>> >>>> >>>> I have to restructure the system, including the compiler >>>> >>>> and interpreter to parse and inherit the DTPs. I >>>> >>>> have some of that code but only some of the code >>>> >>>> has been pushed to the repository (volume 15) but >>>> >>>> that is rather trivial, out of date, and incomplete. >>>> >>>> >>>> >>>> I'm clearly not smart enough to prove the Risch >>>> >>>> algorithm and its associated machinery but the needed >>>> >>>> definitions and theorems will be available to someone >>>> >>>> who wants to try. >>>> >>>> >>>> >>>> [0] https://github.com/daly/PDFS/blob/master/bookvolbib.pdf >>>> >>>> >>>> >>>> >>>> >>>> On 8/19/21, Tim Daly <[email protected]> wrote: >>>> >>>>> =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 >>>> >>>>> >>>> >>>>> REVIEW (Axiom on WSL2 Windows) >>>> >>>>> >>>> >>>>> >>>> >>>>> So the steps to run Axiom from a Windows desktop >>>> >>>>> >>>> >>>>> 1 Windows) install XMing on Windows for X11 server >>>> >>>>> >>>> >>>>> http://www.straightrunning.com/XmingNotes/ >>>> >>>>> >>>> >>>>> 2 WSL2) Install Axiom in WSL2 >>>> >>>>> >>>> >>>>> sudo apt install axiom >>>> >>>>> >>>> >>>>> 3 WSL2) modify /usr/bin/axiom to fix the bug: >>>> >>>>> (someone changed the axiom startup script. >>>> >>>>> It won't work on WSL2. I don't know who or >>>> >>>>> how to get it fixed). >>>> >>>>> >>>> >>>>> sudo emacs /usr/bin/axiom >>>> >>>>> >>>> >>>>> (split the line into 3 and add quote marks) >>>> >>>>> >>>> >>>>> export SPADDEFAULT=3D/usr/local/axiom/mnt/linux >>>> >>>>> export AXIOM=3D/usr/lib/axiom-20170501 >>>> >>>>> export "PATH=3D/usr/lib/axiom-20170501/bin:$PATH" >>>> >>>>> >>>> >>>>> 4 WSL2) create a .axiom.input file to include startup cmds: >>>> >>>>> >>>> >>>>> emacs .axiom.input >>>> >>>>> >>>> >>>>> )cd "/mnt/c/yourpath" >>>> >>>>> )sys pwd >>>> >>>>> >>>> >>>>> 5 WSL2) create a "myaxiom" command that sets the >>>> >>>>> DISPLAY variable and starts axiom >>>> >>>>> >>>> >>>>> emacs myaxiom >>>> >>>>> >>>> >>>>> #! /bin/bash >>>> >>>>> export DISPLAY=3D:0.0 >>>> >>>>> axiom >>>> >>>>> >>>> >>>>> 6 WSL2) put it in the /usr/bin directory >>>> >>>>> >>>> >>>>> chmod +x myaxiom >>>> >>>>> sudo cp myaxiom /usr/bin/myaxiom >>>> >>>>> >>>> >>>>> 7 WINDOWS) start the X11 server >>>> >>>>> >>>> >>>>> (XMing XLaunch Icon on your desktop) >>>> >>>>> >>>> >>>>> 8 WINDOWS) run myaxiom from PowerShell >>>> >>>>> (this should start axiom with graphics available) >>>> >>>>> >>>> >>>>> wsl myaxiom >>>> >>>>> >>>> >>>>> 8 WINDOWS) make a PowerShell desktop >>>> >>>>> >>>> >>>>> >>>> https://superuser.com/questions/886951/run-powershell-script-when-you-= open-powershell >>>> >>>>> >>>> >>>>> Tim >>>> >>>>> >>>> >>>>> On 8/13/21, Tim Daly <[email protected]> wrote: >>>> >>>>>> A great deal of thought is directed toward making the SANE >>>> version >>>> >>>>>> of Axiom as flexible as possible, decoupling mechanism from >>>> theory. >>>> >>>>>> >>>> >>>>>> An interesting publication by Brian Cantwell Smith [0], >>>> "Reflection >>>> >>>>>> and Semantics in LISP" seems to contain interesting ideas relat= ed >>>> >>>>>> to our goal. Of particular interest is the ability to reason >>>> about >>>> >>>>>> and >>>> >>>>>> perform self-referential manipulations. In a dependently-typed >>>> >>>>>> system it seems interesting to be able "adapt" code to handle >>>> >>>>>> run-time computed arguments to dependent functions. The abstrac= t: >>>> >>>>>> >>>> >>>>>> "We show how a computational system can be constructed to >>>> >>>>>> "reason", >>>> >>>>>> effectively >>>> >>>>>> and consequentially, about its own inferential processes. Th= e >>>> >>>>>> analysis proceeds in two >>>> >>>>>> parts. First, we consider the general question of >>>> computational >>>> >>>>>> semantics, rejecting >>>> >>>>>> traditional approaches, and arguing that the declarative and >>>> >>>>>> procedural aspects of >>>> >>>>>> computational symbols (what they stand for, and what behavio= ur >>>> >>>>>> they >>>> >>>>>> engender) should be >>>> >>>>>> analysed independently, in order that they may be coherently >>>> >>>>>> related. Second, we >>>> >>>>>> investigate self-referential behavior in computational >>>> processes, >>>> >>>>>> and show how to embed an >>>> >>>>>> effective procedural model of a computational calculus withi= n >>>> that >>>> >>>>>> calculus (a model not >>>> >>>>>> unlike a meta-circular interpreter, but connected to the >>>> >>>>>> fundamental operations of the >>>> >>>>>> machine in such a way as to provide, at any point in a >>>> >>>>>> computation, >>>> >>>>>> fully articulated >>>> >>>>>> descriptions of the state of that computation, for inspectio= n >>>> and >>>> >>>>>> possible modification). In >>>> >>>>>> terms of the theories that result from these investigations, >>>> we >>>> >>>>>> present a general architecture >>>> >>>>>> for procedurally reflective processes, able to shift smoothl= y >>>> >>>>>> between dealing with a given >>>> >>>>>> subject domain, and dealing with their own reasoning process= es >>>> >>>>>> over >>>> >>>>>> that domain. >>>> >>>>>> >>>> >>>>>> An instance of the general solution is worked out in the >>>> context >>>> >>>>>> of >>>> >>>>>> an applicative >>>> >>>>>> language. Specifically, we present three successive dialects >>>> of >>>> >>>>>> LISP: 1-LISP, a distillation of >>>> >>>>>> current practice, for comparison purposes; 2-LISP, a dialect >>>> >>>>>> constructed in terms of our >>>> >>>>>> rationalised semantics, in which the concept of evaluation i= s >>>> >>>>>> rejected in favour of >>>> >>>>>> independent notions of simplification and reference, and in >>>> which >>>> >>>>>> the respective categories >>>> >>>>>> of notation, structure, semantics, and behaviour are strictl= y >>>> >>>>>> aligned; and 3-LISP, an >>>> >>>>>> extension of 2-LISP endowed with reflective powers." >>>> >>>>>> >>>> >>>>>> Axiom SANE builds dependent types on the fly. The ability to >>>> access >>>> >>>>>> both the refection >>>> >>>>>> of the tower of algebra and the reflection of the tower of >>>> proofs at >>>> >>>>>> the time of construction >>>> >>>>>> makes the construction of a new domain or specific algorithm >>>> easier >>>> >>>>>> and more general. >>>> >>>>>> >>>> >>>>>> This is of particular interest because one of the efforts is to >>>> build >>>> >>>>>> "all the way down to the >>>> >>>>>> metal". If each layer is constructed on top of previous proven >>>> layers >>>> >>>>>> and the new layer >>>> >>>>>> can "reach below" to lower layers then the tower of layers can = be >>>> >>>>>> built without duplication. >>>> >>>>>> >>>> >>>>>> Tim >>>> >>>>>> >>>> >>>>>> [0], Smith, Brian Cantwell "Reflection and Semantics in LISP" >>>> >>>>>> POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN >>>> >>>>>> ymposium on Principles of programming languagesJanuary 1 >>>> >>>>>> 984 Pages 23=E2=80=9335https://doi.org/10.1145/800017.800513 >>>> >>>>>> >>>> >>>>>> On 6/29/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>> Having spent time playing with hardware it is perfectly clear >>>> that >>>> >>>>>>> future computational mathematics efforts need to adapt to usin= g >>>> >>>>>>> parallel processing. >>>> >>>>>>> >>>> >>>>>>> I've spent a fair bit of time thinking about structuring Axiom >>>> to >>>> >>>>>>> be parallel. Most past efforts have tried to focus on making a >>>> >>>>>>> particular algorithm parallel, such as a matrix multiply. >>>> >>>>>>> >>>> >>>>>>> But I think that it might be more effective to make each domai= n >>>> >>>>>>> run in parallel. A computation crosses multiple domains so a >>>> >>>>>>> particular computation could involve multiple parallel copies. >>>> >>>>>>> >>>> >>>>>>> For example, computing the Cylindrical Algebraic Decomposition >>>> >>>>>>> could recursively decompose the plane. Indeed, any >>>> tree-recursive >>>> >>>>>>> algorithm could be run in parallel "in the large" by creating >>>> new >>>> >>>>>>> running copies of the domain for each sub-problem. >>>> >>>>>>> >>>> >>>>>>> So the question becomes, how does one manage this? >>>> >>>>>>> >>>> >>>>>>> A similar problem occurs in robotics where one could have >>>> multiple >>>> >>>>>>> wheels, arms, propellers, etc. that need to act independently >>>> but >>>> >>>>>>> in coordination. >>>> >>>>>>> >>>> >>>>>>> The robot solution uses ROS2. The three ideas are ROSCORE, >>>> >>>>>>> TOPICS with publish/subscribe, and SERVICES with >>>> request/response. >>>> >>>>>>> These are communication paths defined between processes. >>>> >>>>>>> >>>> >>>>>>> ROS2 has a "roscore" which is basically a phonebook of "topics= ". >>>> >>>>>>> Any process can create or look up the current active topics. e= q: >>>> >>>>>>> >>>> >>>>>>> rosnode list >>>> >>>>>>> >>>> >>>>>>> TOPICS: >>>> >>>>>>> >>>> >>>>>>> Any process can PUBLISH a topic (which is basically a typed da= ta >>>> >>>>>>> structure), e.g the topic /hw with the String data "Hello >>>> World". >>>> >>>>>>> eg: >>>> >>>>>>> >>>> >>>>>>> rostopic pub /hw std_msgs/String "Hello, World" >>>> >>>>>>> >>>> >>>>>>> Any process can SUBSCRIBE to a topic, such as /hw, and get a >>>> >>>>>>> copy of the data. eg: >>>> >>>>>>> >>>> >>>>>>> rostopic echo /hw =3D=3D> "Hello, World" >>>> >>>>>>> >>>> >>>>>>> Publishers talk, subscribers listen. >>>> >>>>>>> >>>> >>>>>>> >>>> >>>>>>> SERVICES: >>>> >>>>>>> >>>> >>>>>>> Any process can make a REQUEST of a SERVICE and get a RESPONSE= . >>>> >>>>>>> This is basically a remote function call. >>>> >>>>>>> >>>> >>>>>>> >>>> >>>>>>> >>>> >>>>>>> Axiom in parallel? >>>> >>>>>>> >>>> >>>>>>> So domains could run, each in its own process. It could provid= e >>>> >>>>>>> services, one for each function. Any other process could reque= st >>>> >>>>>>> a computation and get the result as a response. Domains could >>>> >>>>>>> request services from other domains, either waiting for >>>> responses >>>> >>>>>>> or continuing while the response is being computed. >>>> >>>>>>> >>>> >>>>>>> The output could be sent anywhere, to a terminal, to a browser= , >>>> >>>>>>> to a network, or to another process using the publish/subscrib= e >>>> >>>>>>> protocol, potentially all at the same time since there can be >>>> many >>>> >>>>>>> subscribers to a topic. >>>> >>>>>>> >>>> >>>>>>> Available domains could be dynamically added by announcing >>>> >>>>>>> themselves as new "topics" and could be dynamically looked-up >>>> >>>>>>> at runtime. >>>> >>>>>>> >>>> >>>>>>> This structure allows function-level / domain-level parallelis= m. >>>> >>>>>>> It is very effective in the robot world and I think it might b= e >>>> a >>>> >>>>>>> good structuring mechanism to allow computational mathematics >>>> >>>>>>> to take advantage of multiple processors in a disciplined >>>> fashion. >>>> >>>>>>> >>>> >>>>>>> Axiom has a thousand domains and each could run on its own cor= e. >>>> >>>>>>> >>>> >>>>>>> In addition. notice that each domain is independent of the >>>> others. >>>> >>>>>>> So if we want to use BLAS Fortran code, it could just be anoth= er >>>> >>>>>>> service node. In fact, any "foreign function" could >>>> transparently >>>> >>>>>>> cooperate in a distributed Axiom. >>>> >>>>>>> >>>> >>>>>>> Another key feature is that proofs can be "by node". >>>> >>>>>>> >>>> >>>>>>> Tim >>>> >>>>>>> >>>> >>>>>>> >>>> >>>>>>> >>>> >>>>>>> >>>> >>>>>>> On 6/5/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>> Axiom is based on first-class dependent types. Deciding when >>>> >>>>>>>> two types are equivalent may involve computation. See >>>> >>>>>>>> Christiansen, David Thrane "Checking Dependent Types with >>>> >>>>>>>> Normalization by Evaluation" (2019) >>>> >>>>>>>> >>>> >>>>>>>> This puts an interesting constraint on building types. The >>>> >>>>>>>> constructed types has to export a function to decide if a >>>> >>>>>>>> given type is "equivalent" to itself. >>>> >>>>>>>> >>>> >>>>>>>> The notion of "equivalence" might involve category ideas >>>> >>>>>>>> of natural transformation and univalence. Sigh. >>>> >>>>>>>> >>>> >>>>>>>> That's an interesting design point. >>>> >>>>>>>> >>>> >>>>>>>> Tim >>>> >>>>>>>> >>>> >>>>>>>> >>>> >>>>>>>> On 5/5/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>>> It is interesting that programmer's eyes and expectations >>>> adapt >>>> >>>>>>>>> to the tools they use. For instance, I use emacs and expect = to >>>> >>>>>>>>> work directly in files and multiple buffers. When I try to >>>> use one >>>> >>>>>>>>> of the many IDE tools I find they tend to "get in the way". = I >>>> >>>>>>>>> already >>>> >>>>>>>>> know or can quickly find whatever they try to tell me. If yo= u >>>> use >>>> >>>>>>>>> an >>>> >>>>>>>>> IDE you probably find emacs "too sparse" for programming. >>>> >>>>>>>>> >>>> >>>>>>>>> Recently I've been working in a sparse programming >>>> environment. >>>> >>>>>>>>> I'm exploring the question of running a proof checker in an >>>> FPGA. >>>> >>>>>>>>> The FPGA development tools are painful at best and not >>>> intuitive >>>> >>>>>>>>> since you SEEM to be programming but you're actually >>>> describing >>>> >>>>>>>>> hardware gates, connections, and timing. This is an >>>> environment >>>> >>>>>>>>> where everything happens all-at-once and all-the-time (like >>>> the >>>> >>>>>>>>> circuits in your computer). It is the "assembly language of >>>> >>>>>>>>> circuits". >>>> >>>>>>>>> Naturally, my eyes have adapted to this rather raw level. >>>> >>>>>>>>> >>>> >>>>>>>>> That said, I'm normally doing literate programming all the >>>> time. >>>> >>>>>>>>> My typical file is a document which is a mixture of latex an= d >>>> >>>>>>>>> lisp. >>>> >>>>>>>>> It is something of a shock to return to that world. It is >>>> clear >>>> >>>>>>>>> why >>>> >>>>>>>>> people who program in Python find lisp to be a "sea of >>>> parens". >>>> >>>>>>>>> Yet as a lisp programmer, I don't even see the parens, just >>>> code. >>>> >>>>>>>>> >>>> >>>>>>>>> It takes a few minutes in a literate document to adapt visio= n >>>> to >>>> >>>>>>>>> see the latex / lisp combination as natural. The latex marku= p, >>>> >>>>>>>>> like the lisp parens, eventually just disappears. What remai= ns >>>> >>>>>>>>> is just lisp and natural language text. >>>> >>>>>>>>> >>>> >>>>>>>>> This seems painful at first but eyes quickly adapt. The upsi= de >>>> >>>>>>>>> is that there is always a "finished" document that describes >>>> the >>>> >>>>>>>>> state of the code. The overhead of writing a paragraph to >>>> >>>>>>>>> describe a new function or change a paragraph to describe th= e >>>> >>>>>>>>> changed function is very small. >>>> >>>>>>>>> >>>> >>>>>>>>> Using a Makefile I latex the document to generate a current >>>> PDF >>>> >>>>>>>>> and then I extract, load, and execute the code. This loop >>>> catches >>>> >>>>>>>>> errors in both the latex and the source code. Keeping an ope= n >>>> file >>>> >>>>>>>>> in >>>> >>>>>>>>> my pdf viewer shows all of the changes in the document after >>>> every >>>> >>>>>>>>> run of make. That way I can edit the book as easily as the >>>> code. >>>> >>>>>>>>> >>>> >>>>>>>>> Ultimately I find that writing the book while writing the >>>> code is >>>> >>>>>>>>> more productive. I don't have to remember why I wrote >>>> something >>>> >>>>>>>>> since the explanation is already there. >>>> >>>>>>>>> >>>> >>>>>>>>> We all have our own way of programming and our own tools. >>>> >>>>>>>>> But I find literate programming to be a real advance over ID= E >>>> >>>>>>>>> style programming and "raw code" programming. >>>> >>>>>>>>> >>>> >>>>>>>>> Tim >>>> >>>>>>>>> >>>> >>>>>>>>> >>>> >>>>>>>>> On 2/27/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>>>> The systems I use have the interesting property of >>>> >>>>>>>>>> "Living within the compiler". >>>> >>>>>>>>>> >>>> >>>>>>>>>> Lisp, Forth, Emacs, and other systems that present themselv= es >>>> >>>>>>>>>> through the Read-Eval-Print-Loop (REPL) allow the >>>> >>>>>>>>>> ability to deeply interact with the system, shaping it to >>>> your >>>> >>>>>>>>>> need. >>>> >>>>>>>>>> >>>> >>>>>>>>>> My current thread of study is software architecture. See >>>> >>>>>>>>>> https://www.youtube.com/watch?v=3DW2hagw1VhhI&feature=3Dyou= tu.be >>>> >>>>>>>>>> and https://www.georgefairbanks.com/videos/ >>>> >>>>>>>>>> >>>> >>>>>>>>>> My current thinking on SANE involves the ability to >>>> >>>>>>>>>> dynamically define categories, representations, and functio= ns >>>> >>>>>>>>>> along with "composition functions" that permits choosing a >>>> >>>>>>>>>> combination at the time of use. >>>> >>>>>>>>>> >>>> >>>>>>>>>> You might want a domain for handling polynomials. There are >>>> >>>>>>>>>> a lot of choices, depending on your use case. You might wan= t >>>> >>>>>>>>>> different representations. For example, you might want dens= e, >>>> >>>>>>>>>> sparse, recursive, or "machine compatible fixnums" (e.g. to >>>> >>>>>>>>>> interface with C code). If these don't exist it ought to be >>>> >>>>>>>>>> possible >>>> >>>>>>>>>> to create them. Such "lego-like" building blocks require >>>> careful >>>> >>>>>>>>>> thought about creating "fully factored" objects. >>>> >>>>>>>>>> >>>> >>>>>>>>>> Given that goal, the traditional barrier of "compiler" vs >>>> >>>>>>>>>> "interpreter" >>>> >>>>>>>>>> does not seem useful. It is better to "live within the >>>> compiler" >>>> >>>>>>>>>> which >>>> >>>>>>>>>> gives the ability to define new things "on the fly". >>>> >>>>>>>>>> >>>> >>>>>>>>>> Of course, the SANE compiler is going to want an associated >>>> >>>>>>>>>> proof of the functions you create along with the other part= s >>>> >>>>>>>>>> such as its category hierarchy and representation propertie= s. >>>> >>>>>>>>>> >>>> >>>>>>>>>> There is no such thing as a simple job. :-) >>>> >>>>>>>>>> >>>> >>>>>>>>>> Tim >>>> >>>>>>>>>> >>>> >>>>>>>>>> >>>> >>>>>>>>>> On 2/18/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>>>>> The Axiom SANE compiler / interpreter has a few design >>>> points. >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> 1) It needs to mix interpreted and compiled code in the sa= me >>>> >>>>>>>>>>> function. >>>> >>>>>>>>>>> SANE allows dynamic construction of code as well as dynami= c >>>> type >>>> >>>>>>>>>>> construction at runtime. Both of these can occur in a >>>> runtime >>>> >>>>>>>>>>> object. >>>> >>>>>>>>>>> So there is potentially a mixture of interpreted and >>>> compiled >>>> >>>>>>>>>>> code. >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> 2) It needs to perform type resolution at compile time >>>> without >>>> >>>>>>>>>>> overhead >>>> >>>>>>>>>>> where possible. Since this is not always possible there >>>> needs to >>>> >>>>>>>>>>> be >>>> >>>>>>>>>>> a "prefix thunk" that will perform the resolution. >>>> Trivially, >>>> >>>>>>>>>>> for >>>> >>>>>>>>>>> example, >>>> >>>>>>>>>>> if we have a + function we need to type-resolve the >>>> arguments. >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> However, if we can prove at compile time that the types ar= e >>>> both >>>> >>>>>>>>>>> bounded-NNI and the result is bounded-NNI (i.e. fixnum in >>>> lisp) >>>> >>>>>>>>>>> then we can inline a call to + at runtime. If not, we migh= t >>>> have >>>> >>>>>>>>>>> + applied to NNI and POLY(FLOAT), which requires a thunk t= o >>>> >>>>>>>>>>> resolve types. The thunk could even "specialize and compil= e" >>>> >>>>>>>>>>> the code before executing it. >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> It turns out that the Forth implementation of >>>> >>>>>>>>>>> "threaded-interpreted" >>>> >>>>>>>>>>> languages model provides an efficient and effective way to >>>> do >>>> >>>>>>>>>>> this.[0] >>>> >>>>>>>>>>> Type resolution can be "inserted" in intermediate thunks. >>>> >>>>>>>>>>> The model also supports dynamic overloading and tail >>>> recursion. >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> Combining high-level CLOS code with low-level threading >>>> gives an >>>> >>>>>>>>>>> easy to understand and robust design. >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> Tim >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> [0] Loeliger, R.G. "Threaded Interpretive Languages" (1981= ) >>>> >>>>>>>>>>> ISBN 0-07-038360-X >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> >>>> >>>>>>>>>>> On 2/5/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>>>>>> I've worked hard to make Axiom depend on almost no other >>>> >>>>>>>>>>>> tools so that it would not get caught by "code rot" of >>>> >>>>>>>>>>>> libraries. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> However, I'm also trying to make the new SANE version muc= h >>>> >>>>>>>>>>>> easier to understand and debug.To that end I've been >>>> >>>>>>>>>>>> experimenting >>>> >>>>>>>>>>>> with some ideas. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> It should be possible to view source code, of course. But >>>> the >>>> >>>>>>>>>>>> source >>>> >>>>>>>>>>>> code is not the only, nor possibly the best, >>>> representation of >>>> >>>>>>>>>>>> the >>>> >>>>>>>>>>>> ideas. >>>> >>>>>>>>>>>> In particular, source code gets compiled into data >>>> structures. >>>> >>>>>>>>>>>> In >>>> >>>>>>>>>>>> Axiom >>>> >>>>>>>>>>>> these data structures really are a graph of related >>>> structures. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> For example, looking at the gcd function from NNI, there >>>> is the >>>> >>>>>>>>>>>> representation of the gcd function itself. But there is >>>> also a >>>> >>>>>>>>>>>> structure >>>> >>>>>>>>>>>> that is the REP (and, in the new system, is separate from >>>> the >>>> >>>>>>>>>>>> domain). >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> Further, there are associated specification and proof >>>> >>>>>>>>>>>> structures. >>>> >>>>>>>>>>>> Even >>>> >>>>>>>>>>>> further, the domain inherits the category structures, and >>>> from >>>> >>>>>>>>>>>> those >>>> >>>>>>>>>>>> it >>>> >>>>>>>>>>>> inherits logical axioms and definitions through the proof >>>> >>>>>>>>>>>> structure. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> Clearly the gcd function is a node in a much larger graph >>>> >>>>>>>>>>>> structure. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> When trying to decide why code won't compile it would be >>>> useful >>>> >>>>>>>>>>>> to >>>> >>>>>>>>>>>> be able to see and walk these structures. I've thought >>>> about >>>> >>>>>>>>>>>> using >>>> >>>>>>>>>>>> the >>>> >>>>>>>>>>>> browser but browsers are too weak. Either everything has >>>> to be >>>> >>>>>>>>>>>> "in >>>> >>>>>>>>>>>> a >>>> >>>>>>>>>>>> single tab to show the graph" or "the nodes of the graph >>>> are in >>>> >>>>>>>>>>>> different >>>> >>>>>>>>>>>> tabs". Plus, constructing dynamic graphs that change as t= he >>>> >>>>>>>>>>>> software >>>> >>>>>>>>>>>> changes (e.g. by loading a new spad file or creating a ne= w >>>> >>>>>>>>>>>> function) >>>> >>>>>>>>>>>> represents the huge problem of keeping the browser "in sy= nc >>>> >>>>>>>>>>>> with >>>> >>>>>>>>>>>> the >>>> >>>>>>>>>>>> Axiom workspace". So something more dynamic and embedded = is >>>> >>>>>>>>>>>> needed. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> Axiom source gets compiled into CLOS data structures. Eac= h >>>> of >>>> >>>>>>>>>>>> these >>>> >>>>>>>>>>>> new SANE structures has an associated surface >>>> representation, >>>> >>>>>>>>>>>> so >>>> >>>>>>>>>>>> they >>>> >>>>>>>>>>>> can be presented in user-friendly form. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> Also, since Axiom is literate software, it should be >>>> possible >>>> >>>>>>>>>>>> to >>>> >>>>>>>>>>>> look >>>> >>>>>>>>>>>> at >>>> >>>>>>>>>>>> the code in its literate form with the surrounding >>>> explanation. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> Essentially we'd like to have the ability to "deep dive" >>>> into >>>> >>>>>>>>>>>> the >>>> >>>>>>>>>>>> Axiom >>>> >>>>>>>>>>>> workspace, not only for debugging, but also for >>>> understanding >>>> >>>>>>>>>>>> what >>>> >>>>>>>>>>>> functions are used, where they come from, what they >>>> inherit, >>>> >>>>>>>>>>>> and >>>> >>>>>>>>>>>> how they are used in a computation. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> To that end I'm looking at using McClim, a lisp windowing >>>> >>>>>>>>>>>> system. >>>> >>>>>>>>>>>> Since the McClim windows would be part of the lisp image, >>>> they >>>> >>>>>>>>>>>> have >>>> >>>>>>>>>>>> access to display (and modify) the Axiom workspace at all >>>> >>>>>>>>>>>> times. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> The only hesitation is that McClim uses quicklisp and >>>> drags in >>>> >>>>>>>>>>>> a >>>> >>>>>>>>>>>> lot >>>> >>>>>>>>>>>> of other subsystems. It's all lisp, of course. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> These ideas aren't new. They were available on Symbolics >>>> >>>>>>>>>>>> machines, >>>> >>>>>>>>>>>> a truly productive platform and one I sorely miss. >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> Tim >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>>> On 1/19/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>>>>>>> Also of interest is the talk >>>> >>>>>>>>>>>>> "The Unreasonable Effectiveness of Dynamic Typing for >>>> >>>>>>>>>>>>> Practical >>>> >>>>>>>>>>>>> Programs" >>>> >>>>>>>>>>>>> https://vimeo.com/74354480 >>>> >>>>>>>>>>>>> which questions whether static typing really has any >>>> benefit. >>>> >>>>>>>>>>>>> >>>> >>>>>>>>>>>>> Tim >>>> >>>>>>>>>>>>> >>>> >>>>>>>>>>>>> >>>> >>>>>>>>>>>>> On 1/19/21, Tim Daly <[email protected]> wrote: >>>> >>>>>>>>>>>>>> Peter Naur wrote an article of interest: >>>> >>>>>>>>>>>>>> http://pages.cs.wisc.edu/~remzi/Naur.pdf >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> In particular, it mirrors my notion that Axiom needs >>>> >>>>>>>>>>>>>> to embrace literate programming so that the "theory >>>> >>>>>>>>>>>>>> of the problem" is presented as well as the "theory >>>> >>>>>>>>>>>>>> of the solution". I quote the introduction: >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> This article is, to my mind, the most accurate account >>>> >>>>>>>>>>>>>> of what goes on in designing and coding a program. >>>> >>>>>>>>>>>>>> I refer to it regularly when discussing how much >>>> >>>>>>>>>>>>>> documentation to create, how to pass along tacit >>>> >>>>>>>>>>>>>> knowledge, and the value of the XP's metaphor-setting >>>> >>>>>>>>>>>>>> exercise. It also provides a way to examine a >>>> methodolgy's >>>> >>>>>>>>>>>>>> economic structure. >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> In the article, which follows, note that the quality of >>>> the >>>> >>>>>>>>>>>>>> designing programmer's work is related to the quality o= f >>>> >>>>>>>>>>>>>> the match between his theory of the problem and his >>>> theory >>>> >>>>>>>>>>>>>> of the solution. Note that the quality of a later >>>> >>>>>>>>>>>>>> programmer's >>>> >>>>>>>>>>>>>> work is related to the match between his theories and t= he >>>> >>>>>>>>>>>>>> previous programmer's theories. >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> Using Naur's ideas, the designer's job is not to pass >>>> along >>>> >>>>>>>>>>>>>> "the design" but to pass along "the theories" driving t= he >>>> >>>>>>>>>>>>>> design. >>>> >>>>>>>>>>>>>> The latter goal is more useful and more appropriate. It >>>> also >>>> >>>>>>>>>>>>>> highlights that knowledge of the theory is tacit in the >>>> >>>>>>>>>>>>>> owning, >>>> >>>>>>>>>>>>>> and >>>> >>>>>>>>>>>>>> so passing along the thoery requires passing along both >>>> >>>>>>>>>>>>>> explicit >>>> >>>>>>>>>>>>>> and tacit knowledge. >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>>> Tim >>>> >>>>>>>>>>>>>> >>>> >>>>>>>>>>>>> >>>> >>>>>>>>>>>> >>>> >>>>>>>>>>> >>>> >>>>>>>>>> >>>> >>>>>>>>> >>>> >>>>>>>> >>>> >>>>>>> >>>> >>>>>> >>>> >>>>> >>>> >>>> >>>> >>> >>>> >> >>>> > >>>> >>> --00000000000001b29105d0b319e8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div>Full support for general, first-class dependent types= requires</div><div>some changes to the Axiom design. That implies some lan= guage</div><div>design questions.</div><div><br></div><div>Given that mathe= matics is such a general subject with a lot of</div><div>"local" = notation and ideas (witness logical judgment notation)</div><div>careful th= ought is needed to design a language that is able to</div><div>handle a wid= e range.</div><div><br></div><div>Normally language design is a two-level p= rocess. The language</div><div>designer creates a language and then an impl= ementation. Various</div><div>design choices affect the final language.<br>= </div><div><br></div><div>There is "The Metaobject Protocol" (MOP= )<br></div><div><a href=3D"https://www.amazon.com/Art-Metaobject-Protocol-G= regor-Kiczales/dp/0262610744">https://www.amazon.com/Art-Metaobject-Protoco= l-Gregor-Kiczales/dp/0262610744</a></div><div>which encourages a three-leve= l process. The language designer <br></div><div>works at a Metalevel to des= ign a family of languages, then the</div><div>language specializations, the= n the implementation. A MOP design</div><div>allows the language user to op= timize the language to their problem.</div><div><br></div><div>A simple pap= er on the subject is "Metaobject Protocols"</div><div><a href=3D"= https://users.cs.duke.edu/~vahdat/ps/mop.pdf">https://users.cs.duke.edu/~va= hdat/ps/mop.pdf</a></div><div><br></div><div>Tim</div><div><br></div></div>= <br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Mon= , Oct 25, 2021 at 7:42 PM Tim Daly <<a href=3D"mailto:[email protected]= ">[email protected]</a>> wrote:<br></div><blockquote class=3D"gmail_quo= te" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204= );padding-left:1ex"><div dir=3D"ltr"><div>I have a separate thread of resea= rch on Self-Replicating Systems</div><div>(ref: Kinematics of Self Reproduc= ing Machines</div><div><a href=3D"http://www.molecularassembler.com/KSRM.ht= m" target=3D"_blank">http://www.molecularassembler.com/KSRM.htm</a>)<br></d= iv><div><br></div><div>which led to watching "Strange Dreams of Strang= er Loops" by Will Byrd</div><div><a href=3D"https://www.youtube.com/wa= tch?v=3DAffW-7ika0E" target=3D"_blank">https://www.youtube.com/watch?v=3DAf= fW-7ika0E</a></div><div><br></div><div>Will referenced a PhD Thesis by Jon = Doyle</div><div>"A Model for Deliberation, Action, and Introspection&q= uot;</div><div><br></div><div>I also read the thesis by J.C.G. Sturdy</div>= <div>"A Lisp through the Looking Glass"</div><div><br></div><div>= Self-replication requires the ability to manipulate your own</div><div>repr= esentation in such a way that changes to that representation</div><div>will= change behavior.</div><div><br></div><div>This leads to two thoughts in th= e SANE research.</div><div><br></div><div>First, "Declarative Represen= tation". That is, most of the things</div><div>about the representatio= n should be declarative rather than</div><div>procedural. Applying this ide= a as much as possible makes it</div><div>easier to understand and manipulat= e.<br></div><div><br></div><div>Second, "Explicit Call Stack". Fu= nction calls form an implicit</div><div>call stack. This can usually be dis= played in a running lisp system.</div><div>However, having the call stack e= xplicitly available would mean</div><div>that a system could "introspe= ct" at the first-class level.</div><div><br></div><div>These two ideas= would make it easy, for example, to let the</div><div>system "show th= e work". One of the normal complaints is that</div><div>a system prese= nts an answer but there is no way to know how</div><div>that answer was der= ived. These two ideas make it possible to</div><div>understand, display, an= d even post-answer manipulate</div><div>the intermediate steps.</div><div><= br></div><div>Having the intermediate steps also allows proofs to be</div><= div>inserted in a step-by-step fashion. This aids the effort to</div><div>h= ave proofs run in parallel with computation at the hardware</div><div>level= .<br></div><div><br></div><div>Tim</div><div><br></div><div><br></div><div>= <br></div><div><br></div><div><br> </div></div><br><div class=3D"gmail_quot= e"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Oct 21, 2021 at 9:50 AM Ti= m Daly <<a href=3D"mailto:[email protected]" target=3D"_blank">axiomcas= @gmail.com</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"><div dir=3D"ltr"><div>So the current struggle involves the categ= ories in Axiom.</div><div><br></div><div>The categories and domains constru= cted using categories</div><div>are dependent types. When are dependent typ= es "equal"?</div><div>Well, hummmm, that depends on the arguments= to the</div><div>constructor.</div><div><br></div><div>But in order to dec= ide(?) equality we have to evaluate</div><div>the arguments (which themselv= es can be dependent types).</div><div>Indeed, we may, and in general, we mu= st evaluate the <br></div><div>arguments at compile time (well, "const= ruction time" as</div><div>there isn't really a compiler / interpr= eter separation anymore.)<br></div><div><br></div><div>That raises the ques= tion of what "equality" means. This</div><div>is not simply a &qu= ot;set equality" relation. It falls into the</div><div>infinite-groupo= id of homotopy type theory. In general</div><div>it appears that deciding c= ategory / domain equivalence</div><div>might force us to climb the type hie= rarchy.</div><div><br></div><div>Beyond that, there is the question of &quo= t;which proof"</div><div>applies to the resulting object. Proofs depen= d on their</div><div>assumptions which might be different for different</di= v><div>constructions. As yet I have no clue how to "index"</div><= div>proofs based on their assumptions, nor how to <br></div><div>connect th= ese assumptions to the groupoid structure.</div><div><br></div><div>My brai= n hurts.</div><div><br></div><div>Tim</div><div><br></div></div><br><div cl= ass=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, Oct 18, 2= 021 at 2:00 AM Tim Daly <<a href=3D"mailto:[email protected]" target=3D= "_blank">[email protected]</a>> wrote:<br></div><blockquote class=3D"gm= ail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,= 204,204);padding-left:1ex"><div dir=3D"ltr"><div>"Birthing Computation= al Mathematics"</div><div><br></div><div>The Axiom SANE project is dif= ficult at a very fundamental</div><div>level. The title "SANE" wa= s chosen due to the various</div><div>words found in a thesuarus... "r= ational", "coherent",</div><div>"judicious" and &q= uot;sound".</div><div><br></div><div>These are very high level, amorph= ous ideas. But so is</div><div>the design of SANE. Breaking away from tradi= tion in</div><div>computer algebra, type theory, and proof assistants</div>= <div>is very difficult. Ideas tend to fall into standard jargon</div><div>w= hich limits both the frame of thinking (e.g. dependent</div><div>types) and= the content (e.g. notation).</div><div><br></div><div>Questioning both fra= me and content is very difficult.</div><div>It is hard to even recognize wh= en they are accepted</div><div>"by default" rather than "by = choice". What does the idea<br></div><div>"power tools" mean= in a primitive, hand labor culture?<br></div><div><br></div><div>Christoph= er Alexander [0] addresses this problem in</div><div>a lot of his writing. = Specifically, in his book "Notes on</div><div>the Synthesis of Form&qu= ot;, in his chapter 5 "The Selfconsious</div><div>Process", he ad= dresses this problem directly. This is a</div><div>"must read" bo= ok.<br></div><div><br></div><div>Unlike building design and contruction, ho= wever, there</div><div>are almost no constraints to use as guides. Alexande= r</div><div>quotes Plato's Phaedrus:</div><div><br></div><div>=C2=A0 &q= uot;First, the taking in of scattered particulars under</div><div>=C2=A0=C2= =A0 one Idea, so that everyone understands what is being</div><div>=C2=A0= =C2=A0 talked about ... Second, the separation of the Idea</div><div>=C2=A0= =C2=A0 into parts, by dividing it at the joints, as nature</div><div>=C2=A0= =C2=A0 directs, not breaking any limb in half as a bad <br></div><div>=C2= =A0=C2=A0 carver might."<br></div><div><br></div><div>Lisp, which has = been called "clay for the mind" can</div><div>build virtually any= thing that can be thought. The <br></div><div>"joints" are also &= quot;of one's choosing" so one is</div><div>both carver and "= nature".<br></div><div><br></div><div>Clearly the problem is no longer= "the tools".</div><div>*I* am the problem constraining the solut= ion.</div><div>Birthing this "new thing" is slow, difficult, and<= /div><div>uncertain at best.</div><div><br></div><div>Tim</div><div><br></d= iv><div>[0] Alexander, Christopher "Notes on the Synthesis</div><div>o= f Form" Harvard University Press 1964 <br></div><div>ISBN 0-674-62751-= 2</div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr"= class=3D"gmail_attr">On Sun, Oct 10, 2021 at 4:40 PM Tim Daly <<a href= =3D"mailto:[email protected]" target=3D"_blank">[email protected]</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">Re: writ= ing a paper... I'm not connected to Academia<br> so anything I'd write would never make it into print.<br> <br> "Language level parsing" is still a long way off. The talk<br> by Guy Steele [2] highlights some of the problems we<br> currently face using mathematical metanotation.<br> <br> For example, a professor I know at CCNY (City College<br> of New York) didn't understand Platzer's "funny<br> fraction notation" (proof judgements) despite being<br> an expert in Platzer's differential equations area.<br> <br> Notation matters and is not widely common.<br> <br> I spoke to Professor Black (in LTI) about using natural<br> language in the limited task of a human-robot cooperation<br> in changing a car tire.=C2=A0 I looked at the current machine<br> learning efforts. They are no where near anything but<br> toy systems, taking too long to train and are too fragile.<br> <br> Instead I ended up using a combination of AIML [3]<br> (Artificial Intelligence Markup Language), the ALICE<br> Chatbot [4], Forgy's OPS5 rule based program [5],<br> and Fahlman's SCONE [6] knowledge base. It was<br> much less fragile in my limited domain problem.<br> <br> I have no idea how to extend any system to deal with<br> even undergraduate mathematics parsing.<br> <br> Nor do I have any idea how I would embed LEAN<br> knowledge into a SCONE database, although I<br> think the combination would be useful and interesting.<br> <br> I do believe that, in the limited area of computational<br> mathematics, we are capable of building robust, proven<br> systems that are quite general and extensible. As you<br> might have guessed I've given it a lot of thought over<br> the years :-)<br> <br> A mathematical language seems to need >6 components<br> <br> 1) We need some sort of a specification language, possibly<br> somewhat 'propositional' that introduces the assumptions<br> you mentioned (ref. your discussion of numbers being<br> abstract and ref. your discussion of relevant choice of<br> assumptions related to a problem).<br> <br> This is starting to show up in the hardware area (e.g.<br> Lamport's TLC[0])<br> <br> Of course, specifications relate to proving programs<br> and, as you recall, I got a cold reception from the<br> LEAN community about using LEAN for program proofs.<br> <br> 2) We need "scaffolding". That is, we need a theory<br> that can be reduced to some implementable form<br> that provides concept-level structure.<br> <br> Axiom uses group theory for this. Axiom's "category"<br> structure has "Category" things like Ring. Claiming<br> to be a Ring brings in a lot of "Signatures" of functions<br> you have to implement to properly be a Ring.<br> <br> Scaffolding provides a firm mathematical basis for<br> design. It provides a link between the concept of a<br> Ring and the expectations you can assume when<br> you claim your "Domain" "is a Ring". Category<br> theory might provide similar structural scaffolding<br> (eventually... I'm still working on that thought garden)<br> <br> LEAN ought to have a textbook(s?) that structures<br> the world around some form of mathematics. It isn't<br> sufficient to say "undergraduate math" is the goal.<br> There needs to be some coherent organization so<br> people can bring ideas like Group Theory to the<br> organization. Which brings me to ...<br> <br> 3) We need "spreading". That is, we need to take<br> the various definitions and theorems in LEAN and<br> place them in their proper place in the scaffold.<br> <br> For example, the Ring category needs the definitions<br> and theorems for a Ring included in the code for the<br> Ring category. Similarly, the Commutative category<br> needs the definitions and theorems that underlie<br> "commutative" included in the code.<br> <br> That way, when you claim to be a "Commutative Ring"<br> you get both sets of definitions and theorems. That is,<br> the inheritance mechanism will collect up all of the<br> definitions and theorems and make them available<br> for proofs.<br> <br> I am looking at LEAN's definitions and theorems with<br> an eye to "spreading" them into the group scaffold of<br> Axiom.<br> <br> 4) We need "carriers" (Axiom calls them representations,<br> aka "REP"). REPs allow data structures to be defined<br> independent of the implementation.<br> <br> For example, Axiom can construct Polynomials that<br> have their coefficients in various forms of representation.<br> You can define "dense" (all coefficients in a list),<br> "sparse" (only non-zero coefficients), "recursive", etc= .<br> <br> A "dense polynomial" and a "sparse polynomial" work<br> exactly the same way as far as the user is concerned.<br> They both implement the same set of functions. There<br> is only a difference of representation for efficiency and<br> this only affects the implementation of the functions,<br> not their use.<br> <br> Axiom "got this wrong" because it didn't sufficiently<br> separate the REP from the "Domain". I plan to fix this.<br> <br> LEAN ought to have a "data structures" subtree that<br> has all of the definitions and axioms for all of the<br> existing data structures (e.g. Red-Black trees). This<br> would be a good undergraduate project.<br> <br> 5) We need "Domains" (in Axiom speak). That is, we<br> need a box that holds all of the functions that implement<br> a "Domain". For example, a "Polynomial Domain" would<br= > hold all of the functions for manipulating polynomials<br> (e.g polynomial multiplication). The "Domain" box<br> is a dependent type that:<br> <br> =C2=A0 A) has an argument list of "Categories" that this "Do= main"<br> =C2=A0 =C2=A0 =C2=A0 box inherits. Thus, the "Integer Domain" inh= erits<br> =C2=A0 =C2=A0 =C2=A0 the definitions and axioms from "Commutative"= ;<br> <br> =C2=A0 =C2=A0 =C2=A0Functions in the "Domain" box can now assume<= br> =C2=A0 =C2=A0 =C2=A0and use the properties of being commutative. Proofs<br> =C2=A0 =C2=A0 =C2=A0of functions in this domain can use the definitions<br> =C2=A0 =C2=A0 =C2=A0and proofs about being commutative.<br> <br> =C2=A0 B) contains an argument that specifies the "REP"<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0(aka, the carrier). That way you get all of the<= br> =C2=A0 =C2=A0 =C2=A0 =C2=A0functions associated with the data structure<br> =C2=A0 =C2=A0 =C2=A0 available for use in the implementation.<br> <br> =C2=A0 =C2=A0 =C2=A0 Functions in the Domain box can use all of<br> =C2=A0 =C2=A0 =C2=A0 the definitions and axioms about the representation<br= > =C2=A0 =C2=A0 =C2=A0 (e.g. NonNegativeIntegers are always positive)<br> <br> =C2=A0 C) contains local "spread" definitions and axioms<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0that can be used in function proofs.<br> <br> =C2=A0 =C2=A0 =C2=A0 For example, a "Square Matrix" domain would<= br> =C2=A0 =C2=A0 =C2=A0 have local axioms that state that the matrix is<br> =C2=A0 =C2=A0 =C2=A0 always square. Thus, functions in that box could<br> =C2=A0 =C2=A0 =C2=A0 use these additional definitions and axioms in<br> =C2=A0 =C2=A0 =C2=A0 function proofs.<br> <br> =C2=A0 D) contains local state. A "Square Matrix" domain<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0would be constructed as a dependent type that<br= > =C2=A0 =C2=A0 =C2=A0 =C2=A0specified the size of the square (e.g. a 2x2<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0matrix would have '2' as a dependent par= ameter.<br> <br> =C2=A0 E) contains implementations of inherited functions.<br> <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0A "Category" could have a signature fo= r a GCD<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0function and the "Category" could have= a default<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0implementation. However, the "Domain" = could<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0have a locally more efficient implementation whi= ch<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0overrides the inherited implementation.<br> <br> =C2=A0 =C2=A0 =C2=A0 Axiom has about 20 GCD implementations that<br> =C2=A0 =C2=A0 =C2=A0 differ locally from the default in the category. They<= br> =C2=A0 =C2=A0 =C2=A0 use properties known locally to be more efficient.<br> <br> =C2=A0 F) contains local function signatures.<br> <br> =C2=A0 =C2=A0 =C2=A0 A "Domain" gives the user more and more uniq= ue<br> =C2=A0 =C2=A0 =C2=A0 functions. The signature have associated<br> =C2=A0 =C2=A0 =C2=A0 "pre- and post- conditions" that can be used= <br> =C2=A0 =C2=A0 =C2=A0 as assumptions in the function proofs.<br> <br> =C2=A0 =C2=A0 =C2=A0 Some of the user-available functions are only<br> =C2=A0 =C2=A0 =C2=A0 visible if the dependent type would allow them<br> =C2=A0 =C2=A0 =C2=A0 to exist. For example, a general Matrix domain<br> =C2=A0 =C2=A0 =C2=A0 would have fewer user functions that a Square<br> =C2=A0 =C2=A0 =C2=A0 Matrix domain.<br> <br> =C2=A0 =C2=A0 =C2=A0 In addition, local "helper" functions need t= heir<br> =C2=A0 =C2=A0 =C2=A0 own signatures that are not user visible.<br> <br> =C2=A0 G) the function implementation for each signature.<br> <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0This is obviously where all the magic happens<br= > <br> =C2=A0 H) the proof of each function.<br> <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0This is where I'm using LEAN.<br> <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0Every function has a proof. That proof can use<b= r> =C2=A0 =C2=A0 =C2=A0 =C2=A0all of the definitions and axioms inherited from= <br> =C2=A0 =C2=A0 =C2=A0 =C2=A0the "Category", "Representation&q= uot;, the "Domain<br> =C2=A0 =C2=A0 =C2=A0 =C2=A0Local", and the signature pre- and post-<br= > =C2=A0 =C2=A0 =C2=A0 =C2=A0conditions.<br> <br> =C2=A0 =C2=A0I) literature links. Algorithms must contain a link<br> =C2=A0 =C2=A0 =C2=A0 to at least one literature reference. Of course,<br> =C2=A0 =C2=A0 =C2=A0 since everything I do is a Literate Program<br> =C2=A0 =C2=A0 =C2=A0 this is obviously required. Knuth said so :-)<br> <br> <br> LEAN ought to have "books" or "pamphlets" that<br> bring together all of this information for a domain<br> such as Square Matrices. That way a user can<br> find all of the related ideas, available functions,<br> and their corresponding proofs in one place.<br> <br> 6) User level presentation.<br> <br> =C2=A0 =C2=A0 This is where the systems can differ significantly.<br> =C2=A0 =C2=A0 Axiom and LEAN both have GCD but they use<br> =C2=A0 =C2=A0 that for different purposes.<br> <br> =C2=A0 =C2=A0 I'm trying to connect LEAN's GCD and Axiom's GCD<= br> =C2=A0 =C2=A0 so there is a "computational mathematics" idea that= <br> =C2=A0 =C2=A0 allows the user to connect proofs and implementations.<br> <br> 7) Trust<br> <br> Unlike everything else, computational mathematics<br> can have proven code that gives various guarantees.<br> <br> I have been working on this aspect for a while.<br> I refer to it as trust "down to the metal" The idea is<br> that a proof of the GCD function and the implementation<br> of the GCD function get packaged into the ELF format.<br> (proof carrying code). When the GCD algorithm executes<br> on the CPU, the GCD proof is run through the LEAN<br> proof checker on an FPGA in parallel.<br> <br> (I just recently got a PYNQ Xilinx board [1] with a CPU<br> and FPGA together. I'm trying to implement the LEAN<br> proof checker on the FPGA).<br> <br> We are on the cusp of a revolution in computational<br> mathematics. But the two pillars (proof and computer<br> algebra) need to get know each other.<br> <br> Tim<br> <br> <br> <br> [0] Lamport, Leslie "Chapter on TLA+"<br> in "Software Specification Methods"<br> <a href=3D"https://www.springer.com/gp/book/9781852333539" rel=3D"noreferre= r" target=3D"_blank">https://www.springer.com/gp/book/9781852333539</a><br> (I no longer have CMU library access or I'd send you<br> the book PDF)<br> <br> [1] <a href=3D"https://www.tul.com.tw/productspynq-z2.html" rel=3D"noreferr= er" target=3D"_blank">https://www.tul.com.tw/productspynq-z2.html</a><br> <br> [2] <a href=3D"https://www.youtube.com/watch?v=3DdCuZkaaou0Q" rel=3D"norefe= rrer" target=3D"_blank">https://www.youtube.com/watch?v=3DdCuZkaaou0Q</a><b= r> <br> [3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE"<br> <a href=3D"https://arxiv.org/pdf/1307.3091.pdf" rel=3D"noreferrer" target= =3D"_blank">https://arxiv.org/pdf/1307.3091.pdf</a><br> <br> [4] ALICE Chatbot<br> <a href=3D"http://www.scielo.org.mx/pdf/cys/v19n4/1405-5546-cys-19-04-00625= .pdf" rel=3D"noreferrer" target=3D"_blank">http://www.scielo.org.mx/pdf/cys= /v19n4/1405-5546-cys-19-04-00625.pdf</a><br> <br> [5] OPS5 User Manual<br> <a href=3D"https://kilthub.cmu.edu/articles/journal_contribution/OPS5_user_= s_manual/6608090/1" rel=3D"noreferrer" target=3D"_blank">https://kilthub.cm= u.edu/articles/journal_contribution/OPS5_user_s_manual/6608090/1</a><br> <br> [6] Scott Fahlman "SCONE"<br> <a href=3D"http://www.cs.cmu.edu/~sef/scone/" rel=3D"noreferrer" target=3D"= _blank">http://www.cs.cmu.edu/~sef/scone/</a><br> <br> On 9/27/21, Tim Daly <<a href=3D"mailto:[email protected]" target=3D"_b= lank">[email protected]</a>> wrote:<br> > I have tried to maintain a list of names of people who have<br> > helped Axiom, going all the way back to the pre-Scratchpad<br> > days. The names are listed at the beginning of each book.<br> > I also maintain a bibliography of publications I've read or<br> > that have had an indirect influence on Axiom.<br> ><br> > Credit is "the coin of the realm". It is easy to share and w= rong<br> > to ignore. It is especially damaging to those in Academia who<br> > are affected by credit and citations in publications.<br> ><br> > Apparently I'm not the only person who feels that way. The ACM<br> > Turing award seems to have ignored a lot of work:<br> ><br> > Scientific Integrity, the 2021 Turing Lecture, and the 2018 Turing<br> > Award for Deep Learning<br> > <a href=3D"https://people.idsia.ch/~juergen/scientific-integrity-turin= g-award-deep-learning.html" rel=3D"noreferrer" target=3D"_blank">https://pe= ople.idsia.ch/~juergen/scientific-integrity-turing-award-deep-learning.html= </a><br> ><br> > I worked on an AI problem at IBM Research called Ketazolam.<br> > (<a href=3D"https://en.wikipedia.org/wiki/Ketazolam" rel=3D"noreferrer= " target=3D"_blank">https://en.wikipedia.org/wiki/Ketazolam</a>). The idea = was to recognize<br> > and associated 3D chemical drawings with their drug counterparts.<br> > I used Rumelhart, and McClelland's books. These books contained<br= > > quite a few ideas that seem to be "new and innovative" among= the<br> > machine learning crowd... but the books are from 1987. I don't bel= ieve<br> > I've seen these books mentioned in any recent bibliography.<br> > <a href=3D"https://mitpress.mit.edu/books/parallel-distributed-process= ing-volume-1" rel=3D"noreferrer" target=3D"_blank">https://mitpress.mit.edu= /books/parallel-distributed-processing-volume-1</a><br> ><br> ><br> ><br> ><br> > On 9/27/21, Tim Daly <<a href=3D"mailto:[email protected]" target= =3D"_blank">[email protected]</a>> wrote:<br> >> Greg Wilson asked "How Reliable is Scientific Software?"= <br> >> <a href=3D"https://neverworkintheory.org/2021/09/25/how-reliable-i= s-scientific-software.html" rel=3D"noreferrer" target=3D"_blank">https://ne= verworkintheory.org/2021/09/25/how-reliable-is-scientific-software.html</a>= <br> >><br> >> which is a really interesting read. For example"<br> >><br> >>=C2=A0 [Hatton1994], is now a quarter of a century old, but its con= clusions<br> >> are still fresh. The authors fed the same data into nine commercia= l<br> >> geophysical software packages and compared the results; they found= <br> >> that, "numerical disagreement grows at around the rate of 1% = in<br> >> average absolute difference per 4000 fines of implemented code, an= d,<br> >> even worse, the nature of the disagreement is nonrandom" (i.e= ., the<br> >> authors of different packages make similar mistakes).<br> >><br> >><br> >> On 9/26/21, Tim Daly <<a href=3D"mailto:[email protected]" tar= get=3D"_blank">[email protected]</a>> wrote:<br> >>> I should note that the lastest board I've just unboxed<br> >>> (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).<br> >>><br> >>> What makes it interesting is that it contains 2 hard<br> >>> core processors and an FPGA, connected by 9 paths<br> >>> for communication. The processors can be run<br> >>> independently so there is the possibility of a parallel<br> >>> version of some Axiom algorithms (assuming I had<br> >>> the time, which I don't).<br> >>><br> >>> Previously either the hard (physical) processor was<br> >>> separate from the FPGA with minimal communication<br> >>> or the soft core processor had to be created in the FPGA<br> >>> and was much slower.<br> >>><br> >>> Now the two have been combined in a single chip.<br> >>> That means that my effort to run a proof checker on<br> >>> the FPGA and the algorithm on the CPU just got to<br> >>> the point where coordination is much easier.<br> >>><br> >>> Now all I have to do is figure out how to program this<br> >>> beast.<br> >>><br> >>> There is no such thing as a simple job.<br> >>><br> >>> Tim<br> >>><br> >>><br> >>> On 9/26/21, Tim Daly <<a href=3D"mailto:[email protected]"= target=3D"_blank">[email protected]</a>> wrote:<br> >>>> I'm familiar with most of the traditional approaches<b= r> >>>> like Theorema. The bibliography contains most of the<br> >>>> more interesting sources. [0]<br> >>>><br> >>>> There is a difference between traditional approaches to<br= > >>>> connecting computer algebra and proofs and my approach.<br= > >>>><br> >>>> Proving an algorithm, like the GCD, in Axiom is hard.<br> >>>> There are many GCDs (e.g. NNI vs POLY) and there<br> >>>> are theorems and proofs passed at runtime in the<br> >>>> arguments of the newly constructed domains. This<br> >>>> involves a lot of dependent type theory and issues of<br> >>>> compile time / runtime argument evaluation. The issues<br> >>>> that arise are difficult and still being debated in the ty= pe<br> >>>> theory community.<br> >>>><br> >>>> I am putting the definitions, theorems, and proofs (DTP)<b= r> >>>> directly into the category/domain hierarchy. Each category= <br> >>>> will have the DTP specific to it. That way a commutative<b= r> >>>> domain will inherit a commutative theorem and a<br> >>>> non-commutative domain will not.<br> >>>><br> >>>> Each domain will have additional DTPs associated with<br> >>>> the domain (e.g. NNI vs Integer) as well as any DTPs<br> >>>> it inherits from the category hierarchy. Functions in the<= br> >>>> domain will have associated DTPs.<br> >>>><br> >>>> A function to be proven will then inherit all of the relev= ant<br> >>>> DTPs. The proof will be attached to the function and<br> >>>> both will be sent to the hardware (proof-carrying code).<b= r> >>>><br> >>>> The proof checker, running on a field programmable<br> >>>> gate array (FPGA), will be checked at runtime in<br> >>>> parallel with the algorithm running on the CPU<br> >>>> (aka "trust down to the metal"). (Note that Inte= l<br> >>>> and AMD have built CPU/FPGA combined chips,<br> >>>> currently only available in the cloud.)<br> >>>><br> >>>><br> >>>><br> >>>> I am (slowly) making progress on the research.<br> >>>><br> >>>> I have the hardware and nearly have the proof<br> >>>> checker from LEAN running on my FPGA.<br> >>>><br> >>>> I'm in the process of spreading the DTPs from<br> >>>> LEAN across the category/domain hierarchy.<br> >>>><br> >>>> The current Axiom build extracts all of the functions<br> >>>> but does not yet have the DTPs.<br> >>>><br> >>>> I have to restructure the system, including the compiler<b= r> >>>> and interpreter to parse and inherit the DTPs. I<br> >>>> have some of that code but only some of the code<br> >>>> has been pushed to the repository (volume 15) but<br> >>>> that is rather trivial, out of date, and incomplete.<br> >>>><br> >>>> I'm clearly not smart enough to prove the Risch<br> >>>> algorithm and its associated machinery but the needed<br> >>>> definitions and theorems will be available to someone<br> >>>> who wants to try.<br> >>>><br> >>>> [0] <a href=3D"https://github.com/daly/PDFS/blob/master/bo= okvolbib.pdf" rel=3D"noreferrer" target=3D"_blank">https://github.com/daly/= PDFS/blob/master/bookvolbib.pdf</a><br> >>>><br> >>>><br> >>>> On 8/19/21, Tim Daly <<a href=3D"mailto:axiomcas@gmail.= com" target=3D"_blank">[email protected]</a>> wrote:<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<br> >>>>><br> >>>>> REVIEW (Axiom on WSL2 Windows)<br> >>>>><br> >>>>><br> >>>>> So the steps to run Axiom from a Windows desktop<br> >>>>><br> >>>>> 1 Windows) install XMing on Windows for X11 server<br> >>>>><br> >>>>> <a href=3D"http://www.straightrunning.com/XmingNotes/"= rel=3D"noreferrer" target=3D"_blank">http://www.straightrunning.com/XmingN= otes/</a><br> >>>>><br> >>>>> 2 WSL2) Install Axiom in WSL2<br> >>>>><br> >>>>> sudo apt install axiom<br> >>>>><br> >>>>> 3 WSL2) modify /usr/bin/axiom to fix the bug:<br> >>>>> (someone changed the axiom startup script.<br> >>>>> It won't work on WSL2. I don't know who or<br> >>>>> how to get it fixed).<br> >>>>><br> >>>>> sudo emacs /usr/bin/axiom<br> >>>>><br> >>>>> (split the line into 3 and add quote marks)<br> >>>>><br> >>>>> export SPADDEFAULT=3D/usr/local/axiom/mnt/linux<br> >>>>> export AXIOM=3D/usr/lib/axiom-20170501<br> >>>>> export "PATH=3D/usr/lib/axiom-20170501/bin:$PATH&= quot;<br> >>>>><br> >>>>> 4 WSL2) create a .axiom.input file to include startup = cmds:<br> >>>>><br> >>>>> emacs .axiom.input<br> >>>>><br> >>>>> )cd "/mnt/c/yourpath"<br> >>>>> )sys pwd<br> >>>>><br> >>>>> 5 WSL2) create a "myaxiom" command that sets= the<br> >>>>>=C2=A0 =C2=A0 =C2=A0DISPLAY variable and starts axiom<b= r> >>>>><br> >>>>> emacs myaxiom<br> >>>>><br> >>>>> #! /bin/bash<br> >>>>> export DISPLAY=3D:0.0<br> >>>>> axiom<br> >>>>><br> >>>>> 6 WSL2) put it in the /usr/bin directory<br> >>>>><br> >>>>> chmod +x myaxiom<br> >>>>> sudo cp myaxiom /usr/bin/myaxiom<br> >>>>><br> >>>>> 7 WINDOWS) start the X11 server<br> >>>>><br> >>>>> (XMing XLaunch Icon on your desktop)<br> >>>>><br> >>>>> 8 WINDOWS) run myaxiom from PowerShell<br> >>>>> (this should start axiom with graphics available)<br> >>>>><br> >>>>> wsl myaxiom<br> >>>>><br> >>>>> 8 WINDOWS) make a PowerShell desktop<br> >>>>><br> >>>>> <a href=3D"https://superuser.com/questions/886951/run-= powershell-script-when-you-open-powershell" rel=3D"noreferrer" target=3D"_b= lank">https://superuser.com/questions/886951/run-powershell-script-when-you= -open-powershell</a><br> >>>>><br> >>>>> Tim<br> >>>>><br> >>>>> On 8/13/21, Tim Daly <<a href=3D"mailto:axiomcas@gm= ail.com" target=3D"_blank">[email protected]</a>> wrote:<br> >>>>>> A great deal of thought is directed toward making = the SANE version<br> >>>>>> of Axiom as flexible as possible, decoupling mecha= nism from theory.<br> >>>>>><br> >>>>>> An interesting publication by Brian Cantwell Smith= [0], "Reflection<br> >>>>>> and Semantics in LISP" seems to contain inter= esting ideas related<br> >>>>>> to our goal. Of particular interest is the ability= to reason about<br> >>>>>> and<br> >>>>>> perform self-referential manipulations. In a depen= dently-typed<br> >>>>>> system it seems interesting to be able "adapt= " code to handle<br> >>>>>> run-time computed arguments to dependent functions= . The abstract:<br> >>>>>><br> >>>>>>=C2=A0 =C2=A0 "We show how a computational sys= tem can be constructed to<br> >>>>>> "reason",<br> >>>>>> effectively<br> >>>>>>=C2=A0 =C2=A0 and consequentially, about its own in= ferential processes. The<br> >>>>>> analysis proceeds in two<br> >>>>>>=C2=A0 =C2=A0 parts. First, we consider the general= question of computational<br> >>>>>> semantics, rejecting<br> >>>>>>=C2=A0 =C2=A0 traditional approaches, and arguing t= hat the declarative and<br> >>>>>> procedural aspects of<br> >>>>>>=C2=A0 =C2=A0 computational symbols (what they stan= d for, and what behaviour<br> >>>>>> they<br> >>>>>> engender) should be<br> >>>>>>=C2=A0 =C2=A0 analysed independently, in order that= they may be coherently<br> >>>>>> related. Second, we<br> >>>>>>=C2=A0 =C2=A0 investigate self-referential behavior= in computational processes,<br> >>>>>> and show how to embed an<br> >>>>>>=C2=A0 =C2=A0 effective procedural model of a compu= tational calculus within that<br> >>>>>> calculus (a model not<br> >>>>>>=C2=A0 =C2=A0 unlike a meta-circular interpreter, b= ut connected to the<br> >>>>>> fundamental operations of the<br> >>>>>>=C2=A0 =C2=A0 machine in such a way as to provide, = at any point in a<br> >>>>>> computation,<br> >>>>>> fully articulated<br> >>>>>>=C2=A0 =C2=A0 descriptions of the state of that com= putation, for inspection and<br> >>>>>> possible modification). In<br> >>>>>>=C2=A0 =C2=A0 terms of the theories that result fro= m these investigations, we<br> >>>>>> present a general architecture<br> >>>>>>=C2=A0 =C2=A0 for procedurally reflective processes= , able to shift smoothly<br> >>>>>> between dealing with a given<br> >>>>>>=C2=A0 =C2=A0 subject domain, and dealing with thei= r own reasoning processes<br> >>>>>> over<br> >>>>>> that domain.<br> >>>>>><br> >>>>>>=C2=A0 =C2=A0 An instance of the general solution i= s worked out in the context<br> >>>>>> of<br> >>>>>> an applicative<br> >>>>>>=C2=A0 =C2=A0 language. Specifically, we present th= ree successive dialects of<br> >>>>>> LISP: 1-LISP, a distillation of<br> >>>>>>=C2=A0 =C2=A0 current practice, for comparison purp= oses; 2-LISP, a dialect<br> >>>>>> constructed in terms of our<br> >>>>>>=C2=A0 =C2=A0 rationalised semantics, in which the = concept of evaluation is<br> >>>>>> rejected in favour of<br> >>>>>>=C2=A0 =C2=A0 independent notions of simplification= and reference, and in which<br> >>>>>> the respective categories<br> >>>>>>=C2=A0 =C2=A0 of notation, structure, semantics, an= d behaviour are strictly<br> >>>>>> aligned; and 3-LISP, an<br> >>>>>>=C2=A0 =C2=A0 extension of 2-LISP endowed with refl= ective powers."<br> >>>>>><br> >>>>>> Axiom SANE builds dependent types on the fly. The = ability to access<br> >>>>>> both the refection<br> >>>>>> of the tower of algebra and the reflection of the = tower of proofs at<br> >>>>>> the time of construction<br> >>>>>> makes the construction of a new domain or specific= algorithm easier<br> >>>>>> and more general.<br> >>>>>><br> >>>>>> This is of particular interest because one of the = efforts is to build<br> >>>>>> "all the way down to the<br> >>>>>> metal". If each layer is constructed on top o= f previous proven layers<br> >>>>>> and the new layer<br> >>>>>> can "reach below" to lower layers then t= he tower of layers can be<br> >>>>>> built without duplication.<br> >>>>>><br> >>>>>> Tim<br> >>>>>><br> >>>>>> [0], Smith, Brian Cantwell "Reflection and Se= mantics in LISP"<br> >>>>>> POPL '84: Proceedings of the 11th ACM SIGACT-S= IGPLAN<br> >>>>>> ymposium on Principles of programming languagesJan= uary 1<br> >>>>>> 984 Pages 23=E2=80=9335<a href=3D"https://doi.org/= 10.1145/800017.800513" rel=3D"noreferrer" target=3D"_blank">https://doi.org= /10.1145/800017.800513</a><br> >>>>>><br> >>>>>> On 6/29/21, Tim Daly <<a href=3D"mailto:axiomca= [email protected]" target=3D"_blank">[email protected]</a>> wrote:<br> >>>>>>> Having spent time playing with hardware it is = perfectly clear that<br> >>>>>>> future computational mathematics efforts need = to adapt to using<br> >>>>>>> parallel processing.<br> >>>>>>><br> >>>>>>> I've spent a fair bit of time thinking abo= ut structuring Axiom to<br> >>>>>>> be parallel. Most past efforts have tried to f= ocus on making a<br> >>>>>>> particular algorithm parallel, such as a matri= x multiply.<br> >>>>>>><br> >>>>>>> But I think that it might be more effective to= make each domain<br> >>>>>>> run in parallel. A computation crosses multipl= e domains so a<br> >>>>>>> particular computation could involve multiple = parallel copies.<br> >>>>>>><br> >>>>>>> For example, computing the Cylindrical Algebra= ic Decomposition<br> >>>>>>> could recursively decompose the plane. Indeed,= any tree-recursive<br> >>>>>>> algorithm could be run in parallel "in th= e large" by creating new<br> >>>>>>> running copies of the domain for each sub-prob= lem.<br> >>>>>>><br> >>>>>>> So the question becomes, how does one manage t= his?<br> >>>>>>><br> >>>>>>> A similar problem occurs in robotics where one= could have multiple<br> >>>>>>> wheels, arms, propellers, etc. that need to ac= t independently but<br> >>>>>>> in coordination.<br> >>>>>>><br> >>>>>>> The robot solution uses ROS2. The three ideas = are ROSCORE,<br> >>>>>>> TOPICS with publish/subscribe, and SERVICES wi= th request/response.<br> >>>>>>> These are communication paths defined between = processes.<br> >>>>>>><br> >>>>>>> ROS2 has a "roscore" which is basica= lly a phonebook of "topics".<br> >>>>>>> Any process can create or look up the current = active topics. eq:<br> >>>>>>><br> >>>>>>>=C2=A0 =C2=A0 rosnode list<br> >>>>>>><br> >>>>>>> TOPICS:<br> >>>>>>><br> >>>>>>> Any process can PUBLISH a topic (which is basi= cally a typed data<br> >>>>>>> structure), e.g the topic /hw with the String = data "Hello World".<br> >>>>>>> eg:<br> >>>>>>><br> >>>>>>>=C2=A0 =C2=A0 rostopic pub /hw std_msgs/String = "Hello, World"<br> >>>>>>><br> >>>>>>> Any process can SUBSCRIBE to a topic, such as = /hw, and get a<br> >>>>>>> copy of the data.=C2=A0 eg:<br> >>>>>>><br> >>>>>>>=C2=A0 =C2=A0 rostopic echo /hw=C2=A0 =C2=A0=3D= =3D> "Hello, World"<br> >>>>>>><br> >>>>>>> Publishers talk, subscribers listen.<br> >>>>>>><br> >>>>>>><br> >>>>>>> SERVICES:<br> >>>>>>><br> >>>>>>> Any process can make a REQUEST of a SERVICE an= d get a RESPONSE.<br> >>>>>>> This is basically a remote function call.<br> >>>>>>><br> >>>>>>><br> >>>>>>><br> >>>>>>> Axiom in parallel?<br> >>>>>>><br> >>>>>>> So domains could run, each in its own process.= It could provide<br> >>>>>>> services, one for each function. Any other pro= cess could request<br> >>>>>>> a computation and get the result as a response= . Domains could<br> >>>>>>> request services from other domains, either wa= iting for responses<br> >>>>>>> or continuing while the response is being comp= uted.<br> >>>>>>><br> >>>>>>> The output could be sent anywhere, to a termin= al, to a browser,<br> >>>>>>> to a network, or to another process using the = publish/subscribe<br> >>>>>>> protocol, potentially all at the same time sin= ce there can be many<br> >>>>>>> subscribers to a topic.<br> >>>>>>><br> >>>>>>> Available domains could be dynamically added b= y announcing<br> >>>>>>> themselves as new "topics" and could= be dynamically looked-up<br> >>>>>>> at runtime.<br> >>>>>>><br> >>>>>>> This structure allows function-level / domain-= level parallelism.<br> >>>>>>> It is very effective in the robot world and I = think it might be a<br> >>>>>>> good structuring mechanism to allow computatio= nal mathematics<br> >>>>>>> to take advantage of multiple processors in a = disciplined fashion.<br> >>>>>>><br> >>>>>>> Axiom has a thousand domains and each could ru= n on its own core.<br> >>>>>>><br> >>>>>>> In addition. notice that each domain is indepe= ndent of the others.<br> >>>>>>> So if we want to use BLAS Fortran code, it cou= ld just be another<br> >>>>>>> service node. In fact, any "foreign funct= ion" could transparently<br> >>>>>>> cooperate in a distributed Axiom.<br> >>>>>>><br> >>>>>>> Another key feature is that proofs can be &quo= t;by node".<br> >>>>>>><br> >>>>>>> Tim<br> >>>>>>><br> >>>>>>><br> >>>>>>><br> >>>>>>><br> >>>>>>> On 6/5/21, Tim Daly <<a href=3D"mailto:axio= [email protected]" target=3D"_blank">[email protected]</a>> wrote:<br> >>>>>>>> Axiom is based on first-class dependent ty= pes. Deciding when<br> >>>>>>>> two types are equivalent may involve compu= tation. See<br> >>>>>>>> Christiansen, David Thrane "Checking = Dependent Types with<br> >>>>>>>> Normalization by Evaluation" (2019)<b= r> >>>>>>>><br> >>>>>>>> This puts an interesting constraint on bui= lding types. The<br> >>>>>>>> constructed types has to export a function= to decide if a<br> >>>>>>>> given type is "equivalent" to it= self.<br> >>>>>>>><br> >>>>>>>> The notion of "equivalence" migh= t involve category ideas<br> >>>>>>>> of natural transformation and univalence. = Sigh.<br> >>>>>>>><br> >>>>>>>> That's an interesting design point.<br= > >>>>>>>><br> >>>>>>>> Tim<br> >>>>>>>><br> >>>>>>>><br> >>>>>>>> On 5/5/21, Tim Daly <<a href=3D"mailto:= [email protected]" target=3D"_blank">[email protected]</a>> wrote:<br> >>>>>>>>> It is interesting that programmer'= s eyes and expectations adapt<br> >>>>>>>>> to the tools they use. For instance, I= use emacs and expect to<br> >>>>>>>>> work directly in files and multiple bu= ffers. When I try to use one<br> >>>>>>>>> of the many IDE tools I find they tend= to "get in the way". I<br> >>>>>>>>> already<br> >>>>>>>>> know or can quickly find whatever they= try to tell me. If you use<br> >>>>>>>>> an<br> >>>>>>>>> IDE you probably find emacs "too = sparse" for programming.<br> >>>>>>>>><br> >>>>>>>>> Recently I've been working in a sp= arse programming environment.<br> >>>>>>>>> I'm exploring the question of runn= ing a proof checker in an FPGA.<br> >>>>>>>>> The FPGA development tools are painful= at best and not intuitive<br> >>>>>>>>> since you SEEM to be programming but y= ou're actually describing<br> >>>>>>>>> hardware gates, connections, and timin= g. This is an environment<br> >>>>>>>>> where everything happens all-at-once a= nd all-the-time (like the<br> >>>>>>>>> circuits in your computer). It is the = "assembly language of<br> >>>>>>>>> circuits".<br> >>>>>>>>> Naturally, my eyes have adapted to thi= s rather raw level.<br> >>>>>>>>><br> >>>>>>>>> That said, I'm normally doing lite= rate programming all the time.<br> >>>>>>>>> My typical file is a document which is= a mixture of latex and<br> >>>>>>>>> lisp.<br> >>>>>>>>> It is something of a shock to return t= o that world. It is clear<br> >>>>>>>>> why<br> >>>>>>>>> people who program in Python find lisp= to be a "sea of parens".<br> >>>>>>>>> Yet as a lisp programmer, I don't = even see the parens, just code.<br> >>>>>>>>><br> >>>>>>>>> It takes a few minutes in a literate d= ocument to adapt vision to<br> >>>>>>>>> see the latex / lisp combination as na= tural. The latex markup,<br> >>>>>>>>> like the lisp parens, eventually just = disappears. What remains<br> >>>>>>>>> is just lisp and natural language text= .<br> >>>>>>>>><br> >>>>>>>>> This seems painful at first but eyes q= uickly adapt. The upside<br> >>>>>>>>> is that there is always a "finish= ed" document that describes the<br> >>>>>>>>> state of the code. The overhead of wri= ting a paragraph to<br> >>>>>>>>> describe a new function or change a pa= ragraph to describe the<br> >>>>>>>>> changed function is very small.<br> >>>>>>>>><br> >>>>>>>>> Using a Makefile I latex the document = to generate a current PDF<br> >>>>>>>>> and then I extract, load, and execute = the code. This loop catches<br> >>>>>>>>> errors in both the latex and the sourc= e code. Keeping an open file<br> >>>>>>>>> in<br> >>>>>>>>> my pdf viewer shows all of the changes= in the document after every<br> >>>>>>>>> run of make. That way I can edit the b= ook as easily as the code.<br> >>>>>>>>><br> >>>>>>>>> Ultimately I find that writing the boo= k while writing the code is<br> >>>>>>>>> more productive. I don't have to r= emember why I wrote something<br> >>>>>>>>> since the explanation is already there= .<br> >>>>>>>>><br> >>>>>>>>> We all have our own way of programming= and our own tools.<br> >>>>>>>>> But I find literate programming to be = a real advance over IDE<br> >>>>>>>>> style programming and "raw code&q= uot; programming.<br> >>>>>>>>><br> >>>>>>>>> Tim<br> >>>>>>>>><br> >>>>>>>>><br> >>>>>>>>> On 2/27/21, Tim Daly <<a href=3D"ma= ilto:[email protected]" target=3D"_blank">[email protected]</a>> wrote= :<br> >>>>>>>>>> The systems I use have the interes= ting property of<br> >>>>>>>>>> "Living within the compiler&q= uot;.<br> >>>>>>>>>><br> >>>>>>>>>> Lisp, Forth, Emacs, and other syst= ems that present themselves<br> >>>>>>>>>> through the Read-Eval-Print-Loop (= REPL) allow the<br> >>>>>>>>>> ability to deeply interact with th= e system, shaping it to your<br> >>>>>>>>>> need.<br> >>>>>>>>>><br> >>>>>>>>>> My current thread of study is soft= ware architecture. See<br> >>>>>>>>>> <a href=3D"https://www.youtube.com= /watch?v=3DW2hagw1VhhI&feature=3Dyoutu.be" rel=3D"noreferrer" target=3D= "_blank">https://www.youtube.com/watch?v=3DW2hagw1VhhI&feature=3Dyoutu.= be</a><br> >>>>>>>>>> and <a href=3D"https://www.georgef= airbanks.com/videos/" rel=3D"noreferrer" target=3D"_blank">https://www.geor= gefairbanks.com/videos/</a><br> >>>>>>>>>><br> >>>>>>>>>> My current thinking on SANE involv= es the ability to<br> >>>>>>>>>> dynamically define categories, rep= resentations, and functions<br> >>>>>>>>>> along with "composition funct= ions" that permits choosing a<br> >>>>>>>>>> combination at the time of use.<br= > >>>>>>>>>><br> >>>>>>>>>> You might want a domain for handli= ng polynomials. There are<br> >>>>>>>>>> a lot of choices, depending on you= r use case. You might want<br> >>>>>>>>>> different representations. For exa= mple, you might want dense,<br> >>>>>>>>>> sparse, recursive, or "machin= e compatible fixnums" (e.g. to<br> >>>>>>>>>> interface with C code). If these d= on't exist it ought to be<br> >>>>>>>>>> possible<br> >>>>>>>>>> to create them. Such "lego-li= ke" building blocks require careful<br> >>>>>>>>>> thought about creating "fully= factored" objects.<br> >>>>>>>>>><br> >>>>>>>>>> Given that goal, the traditional b= arrier of "compiler" vs<br> >>>>>>>>>> "interpreter"<br> >>>>>>>>>> does not seem useful. It is better= to "live within the compiler"<br> >>>>>>>>>> which<br> >>>>>>>>>> gives the ability to define new th= ings "on the fly".<br> >>>>>>>>>><br> >>>>>>>>>> Of course, the SANE compiler is go= ing to want an associated<br> >>>>>>>>>> proof of the functions you create = along with the other parts<br> >>>>>>>>>> such as its category hierarchy and= representation properties.<br> >>>>>>>>>><br> >>>>>>>>>> There is no such thing as a simple= job. :-)<br> >>>>>>>>>><br> >>>>>>>>>> Tim<br> >>>>>>>>>><br> >>>>>>>>>><br> >>>>>>>>>> On 2/18/21, Tim Daly <<a href= =3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>>= wrote:<br> >>>>>>>>>>> The Axiom SANE compiler / inte= rpreter has a few design points.<br> >>>>>>>>>>><br> >>>>>>>>>>> 1) It needs to mix interpreted= and compiled code in the same<br> >>>>>>>>>>> function.<br> >>>>>>>>>>> SANE allows dynamic constructi= on of code as well as dynamic type<br> >>>>>>>>>>> construction at runtime. Both = of these can occur in a runtime<br> >>>>>>>>>>> object.<br> >>>>>>>>>>> So there is potentially a mixt= ure of interpreted and compiled<br> >>>>>>>>>>> code.<br> >>>>>>>>>>><br> >>>>>>>>>>> 2) It needs to perform type re= solution at compile time without<br> >>>>>>>>>>> overhead<br> >>>>>>>>>>> where possible. Since this is = not always possible there needs to<br> >>>>>>>>>>> be<br> >>>>>>>>>>> a "prefix thunk" tha= t will perform the resolution. Trivially,<br> >>>>>>>>>>> for<br> >>>>>>>>>>> example,<br> >>>>>>>>>>> if we have a + function we nee= d to type-resolve the arguments.<br> >>>>>>>>>>><br> >>>>>>>>>>> However, if we can prove at co= mpile time that the types are both<br> >>>>>>>>>>> bounded-NNI and the result is = bounded-NNI (i.e. fixnum in lisp)<br> >>>>>>>>>>> then we can inline a call to += at runtime. If not, we might have<br> >>>>>>>>>>> + applied to NNI and POLY(FLOA= T), which requires a thunk to<br> >>>>>>>>>>> resolve types. The thunk could= even "specialize and compile"<br> >>>>>>>>>>> the code before executing it.<= br> >>>>>>>>>>><br> >>>>>>>>>>> It turns out that the Forth im= plementation of<br> >>>>>>>>>>> "threaded-interpreted&quo= t;<br> >>>>>>>>>>> languages model provides an ef= ficient and effective way to do<br> >>>>>>>>>>> this.[0]<br> >>>>>>>>>>> Type resolution can be "i= nserted" in intermediate thunks.<br> >>>>>>>>>>> The model also supports dynami= c overloading and tail recursion.<br> >>>>>>>>>>><br> >>>>>>>>>>> Combining high-level CLOS code= with low-level threading gives an<br> >>>>>>>>>>> easy to understand and robust = design.<br> >>>>>>>>>>><br> >>>>>>>>>>> Tim<br> >>>>>>>>>>><br> >>>>>>>>>>> [0] Loeliger, R.G. "Threa= ded Interpretive Languages" (1981)<br> >>>>>>>>>>> ISBN 0-07-038360-X<br> >>>>>>>>>>><br> >>>>>>>>>>><br> >>>>>>>>>>><br> >>>>>>>>>>><br> >>>>>>>>>>> On 2/5/21, Tim Daly <<a hre= f=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>>= ; wrote:<br> >>>>>>>>>>>> I've worked hard to ma= ke Axiom depend on almost no other<br> >>>>>>>>>>>> tools so that it would not= get caught by "code rot" of<br> >>>>>>>>>>>> libraries.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> However, I'm also tryi= ng to make the new SANE version much<br> >>>>>>>>>>>> easier to understand and d= ebug.To that end I've been<br> >>>>>>>>>>>> experimenting<br> >>>>>>>>>>>> with some ideas.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> It should be possible to v= iew source code, of course. But the<br> >>>>>>>>>>>> source<br> >>>>>>>>>>>> code is not the only, nor = possibly the best, representation of<br> >>>>>>>>>>>> the<br> >>>>>>>>>>>> ideas.<br> >>>>>>>>>>>> In particular, source code= gets compiled into data structures.<br> >>>>>>>>>>>> In<br> >>>>>>>>>>>> Axiom<br> >>>>>>>>>>>> these data structures real= ly are a graph of related structures.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> For example, looking at th= e gcd function from NNI, there is the<br> >>>>>>>>>>>> representation of the gcd = function itself. But there is also a<br> >>>>>>>>>>>> structure<br> >>>>>>>>>>>> that is the REP (and, in t= he new system, is separate from the<br> >>>>>>>>>>>> domain).<br> >>>>>>>>>>>><br> >>>>>>>>>>>> Further, there are associa= ted specification and proof<br> >>>>>>>>>>>> structures.<br> >>>>>>>>>>>> Even<br> >>>>>>>>>>>> further, the domain inheri= ts the category structures, and from<br> >>>>>>>>>>>> those<br> >>>>>>>>>>>> it<br> >>>>>>>>>>>> inherits logical axioms an= d definitions through the proof<br> >>>>>>>>>>>> structure.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> Clearly the gcd function i= s a node in a much larger graph<br> >>>>>>>>>>>> structure.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> When trying to decide why = code won't compile it would be useful<br> >>>>>>>>>>>> to<br> >>>>>>>>>>>> be able to see and walk th= ese structures. I've thought about<br> >>>>>>>>>>>> using<br> >>>>>>>>>>>> the<br> >>>>>>>>>>>> browser but browsers are t= oo weak. Either everything has to be<br> >>>>>>>>>>>> "in<br> >>>>>>>>>>>> a<br> >>>>>>>>>>>> single tab to show the gra= ph" or "the nodes of the graph are in<br> >>>>>>>>>>>> different<br> >>>>>>>>>>>> tabs". Plus, construc= ting dynamic graphs that change as the<br> >>>>>>>>>>>> software<br> >>>>>>>>>>>> changes (e.g. by loading a= new spad file or creating a new<br> >>>>>>>>>>>> function)<br> >>>>>>>>>>>> represents the huge proble= m of keeping the browser "in sync<br> >>>>>>>>>>>> with<br> >>>>>>>>>>>> the<br> >>>>>>>>>>>> Axiom workspace". So = something more dynamic and embedded is<br> >>>>>>>>>>>> needed.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> Axiom source gets compiled= into CLOS data structures. Each of<br> >>>>>>>>>>>> these<br> >>>>>>>>>>>> new SANE structures has an= associated surface representation,<br> >>>>>>>>>>>> so<br> >>>>>>>>>>>> they<br> >>>>>>>>>>>> can be presented in user-f= riendly form.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> Also, since Axiom is liter= ate software, it should be possible<br> >>>>>>>>>>>> to<br> >>>>>>>>>>>> look<br> >>>>>>>>>>>> at<br> >>>>>>>>>>>> the code in its literate f= orm with the surrounding explanation.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> Essentially we'd like = to have the ability to "deep dive" into<br> >>>>>>>>>>>> the<br> >>>>>>>>>>>> Axiom<br> >>>>>>>>>>>> workspace, not only for de= bugging, but also for understanding<br> >>>>>>>>>>>> what<br> >>>>>>>>>>>> functions are used, where = they come from, what they inherit,<br> >>>>>>>>>>>> and<br> >>>>>>>>>>>> how they are used in a com= putation.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> To that end I'm lookin= g at using McClim, a lisp windowing<br> >>>>>>>>>>>> system.<br> >>>>>>>>>>>> Since the McClim windows w= ould be part of the lisp image, they<br> >>>>>>>>>>>> have<br> >>>>>>>>>>>> access to display (and mod= ify) the Axiom workspace at all<br> >>>>>>>>>>>> times.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> The only hesitation is tha= t McClim uses quicklisp and drags in<br> >>>>>>>>>>>> a<br> >>>>>>>>>>>> lot<br> >>>>>>>>>>>> of other subsystems. It= 9;s all lisp, of course.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> These ideas aren't new= . They were available on Symbolics<br> >>>>>>>>>>>> machines,<br> >>>>>>>>>>>> a truly productive platfor= m and one I sorely miss.<br> >>>>>>>>>>>><br> >>>>>>>>>>>> Tim<br> >>>>>>>>>>>><br> >>>>>>>>>>>><br> >>>>>>>>>>>><br> >>>>>>>>>>>> On 1/19/21, Tim Daly <<= a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]</= a>> wrote:<br> >>>>>>>>>>>>> Also of interest is th= e talk<br> >>>>>>>>>>>>> "The Unreasonable= Effectiveness of Dynamic Typing for<br> >>>>>>>>>>>>> Practical<br> >>>>>>>>>>>>> Programs"<br> >>>>>>>>>>>>> <a href=3D"https://vim= eo.com/74354480" rel=3D"noreferrer" target=3D"_blank">https://vimeo.com/743= 54480</a><br> >>>>>>>>>>>>> which questions whethe= r static typing really has any benefit.<br> >>>>>>>>>>>>><br> >>>>>>>>>>>>> Tim<br> >>>>>>>>>>>>><br> >>>>>>>>>>>>><br> >>>>>>>>>>>>> On 1/19/21, Tim Daly &= lt;<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]= om</a>> wrote:<br> >>>>>>>>>>>>>> Peter Naur wrote a= n article of interest:<br> >>>>>>>>>>>>>> <a href=3D"http://= pages.cs.wisc.edu/~remzi/Naur.pdf" rel=3D"noreferrer" target=3D"_blank">htt= p://pages.cs.wisc.edu/~remzi/Naur.pdf</a><br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>> In particular, it = mirrors my notion that Axiom needs<br> >>>>>>>>>>>>>> to embrace literat= e programming so that the "theory<br> >>>>>>>>>>>>>> of the problem&quo= t; is presented as well as the "theory<br> >>>>>>>>>>>>>> of the solution&qu= ot;. I quote the introduction:<br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>> This article is, t= o my mind, the most accurate account<br> >>>>>>>>>>>>>> of what goes on in= designing and coding a program.<br> >>>>>>>>>>>>>> I refer to it regu= larly when discussing how much<br> >>>>>>>>>>>>>> documentation to c= reate, how to pass along tacit<br> >>>>>>>>>>>>>> knowledge, and the= value of the XP's metaphor-setting<br> >>>>>>>>>>>>>> exercise. It also = provides a way to examine a methodolgy's<br> >>>>>>>>>>>>>> economic structure= .<br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>> In the article, wh= ich follows, note that the quality of the<br> >>>>>>>>>>>>>> designing programm= er's work is related to the quality of<br> >>>>>>>>>>>>>> the match between = his theory of the problem and his theory<br> >>>>>>>>>>>>>> of the solution. N= ote that the quality of a later<br> >>>>>>>>>>>>>> programmer's<b= r> >>>>>>>>>>>>>> work is related to= the match between his theories and the<br> >>>>>>>>>>>>>> previous programme= r's theories.<br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>> Using Naur's i= deas, the designer's job is not to pass along<br> >>>>>>>>>>>>>> "the design&q= uot; but to pass along "the theories" driving the<br> >>>>>>>>>>>>>> design.<br> >>>>>>>>>>>>>> The latter goal is= more useful and more appropriate. It also<br> >>>>>>>>>>>>>> highlights that kn= owledge of the theory is tacit in the<br> >>>>>>>>>>>>>> owning,<br> >>>>>>>>>>>>>> and<br> >>>>>>>>>>>>>> so passing along t= he thoery requires passing along both<br> >>>>>>>>>>>>>> explicit<br> >>>>>>>>>>>>>> and tacit knowledg= e.<br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>>> Tim<br> >>>>>>>>>>>>>><br> >>>>>>>>>>>>><br> >>>>>>>>>>>><br> >>>>>>>>>>><br> >>>>>>>>>><br> >>>>>>>>><br> >>>>>>>><br> >>>>>>><br> >>>>>><br> >>>>><br> >>>><br> >>><br> >><br> ><br> </blockquote></div> </blockquote></div> </blockquote></div> </blockquote></div> --00000000000001b29105d0b319e8--