Re: Axiom musings...

[Tim Daly]

=========================================

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