Re: Axiom musings...

[Tim Daly]

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 <axiomcas@gmail.com> wrote:
> =========================================
>
> 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=/usr/local/axiom/mnt/linux
> export AXIOM=/usr/lib/axiom-20170501
> export "PATH=/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=: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 <axiomcas@gmail.com> 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 related
>> 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 abstract:
>>
>>    "We show how a computational system can be constructed to "reason",
>> effectively
>>    and consequentially, about its own inferential processes. The
>> 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 behaviour 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 within 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 inspection 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 smoothly
>> between dealing with a given
>>    subject domain, and dealing with their own reasoning processes 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 is
>> rejected in favour of
>>    independent notions of simplification and reference, and in which
>> the respective categories
>>    of notation, structure, semantics, and behaviour are strictly
>> 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–35https://doi.org/10.1145/800017.800513
>>
>> On 6/29/21, Tim Daly <axiomcas@gmail.com> wrote:
>>> Having spent time playing with hardware it is perfectly clear that
>>> future computational mathematics efforts need to adapt to using
>>> 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 domain
>>> 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. eq:
>>>
>>>    rosnode list
>>>
>>> TOPICS:
>>>
>>> Any process can PUBLISH a topic (which is basically a typed data
>>> 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   ==> "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 provide
>>> services, one for each function. Any other process could request
>>> 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/subscribe
>>> 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 parallelism.
>>> It is very effective in the robot world and I think it might be 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 core.
>>>
>>> In addition. notice that each domain is independent of the others.
>>> So if we want to use BLAS Fortran code, it could just be another
>>> 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 <axiomcas@gmail.com> 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 <axiomcas@gmail.com> 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 you 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 and 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 vision to
>>>>> see the latex / lisp combination as natural. The latex markup,
>>>>> like the lisp parens, eventually just disappears. What remains
>>>>> is just lisp and natural language text.
>>>>>
>>>>> This seems painful at first but eyes quickly adapt. The upside
>>>>> 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 the
>>>>> 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 open 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 IDE
>>>>> style programming and "raw code" programming.
>>>>>
>>>>> Tim
>>>>>
>>>>>
>>>>> On 2/27/21, Tim Daly <axiomcas@gmail.com> wrote:
>>>>>> The systems I use have the interesting property of
>>>>>> "Living within the compiler".
>>>>>>
>>>>>> Lisp, Forth, Emacs, and other systems that present themselves
>>>>>> 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=W2hagw1VhhI&feature=youtu.be
>>>>>> and https://www.georgefairbanks.com/videos/
>>>>>>
>>>>>> My current thinking on SANE involves the ability to
>>>>>> dynamically define categories, representations, and functions
>>>>>> 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 want
>>>>>> different representations. For example, you might want dense,
>>>>>> 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 parts
>>>>>> such as its category hierarchy and representation properties.
>>>>>>
>>>>>> There is no such thing as a simple job. :-)
>>>>>>
>>>>>> Tim
>>>>>>
>>>>>>
>>>>>> On 2/18/21, Tim Daly <axiomcas@gmail.com> wrote:
>>>>>>> The Axiom SANE compiler / interpreter has a few design points.
>>>>>>>
>>>>>>> 1) It needs to mix interpreted and compiled code in the same
>>>>>>> function.
>>>>>>> SANE allows dynamic construction of code as well as dynamic 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 are 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 might have
>>>>>>> + applied to NNI and POLY(FLOAT), which requires a thunk to
>>>>>>> resolve types. The thunk could even "specialize and compile"
>>>>>>> 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 <axiomcas@gmail.com> 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 much
>>>>>>>> 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 the
>>>>>>>> software
>>>>>>>> changes (e.g. by loading a new spad file or creating a new
>>>>>>>> function)
>>>>>>>> represents the huge problem of keeping the browser "in sync with
>>>>>>>> the
>>>>>>>> Axiom workspace". So something more dynamic and embedded is needed.
>>>>>>>>
>>>>>>>> Axiom source gets compiled into CLOS data structures. Each 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 <axiomcas@gmail.com> 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 <axiomcas@gmail.com> 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 of
>>>>>>>>>> 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 the
>>>>>>>>>> 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 the 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
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>
>>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>