Re: Axiom musings...

--00000000000091c88405dadc582b
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

I have a deep interest in self-modifying programs. These are
trivial to create in lisp. The question is how to structure a computer
algebra program so it could be dynamically modified but still
well-structured. This is especially important since the user can
create new logical types at runtime.

One innovation, which I have never seen anywhere, is to structure
the program in a spreadsheet fashion. Spreadsheets cells can
reference other spreadsheet cells. Spreadsheets have a well-defined
evaluation method. This is equivalent to a form of object-oriented
programming where each cell is an object and has a well-defined
inheritance hierarchy through other cells. Simple manipulation
allows insertion, deletion, or modification of these chains at any time.

So by structuring a computer algebra program like a spreadsheet
I am able to dynamically adjust a program to fit the problem to be
solved, track which cells are needed, and optimize the program.

Spreadsheets do this naturally but I'm unaware of any non-spreadsheet
program that relies on that organization.

Tim


On Sun, Mar 13, 2022 at 4:01 AM Tim Daly <[email protected]> wrote:

> Axiom has an awkward 'attributes' category structure.
>
> In the SANE version it is clear that these attributes are much
> closer to logic 'definitions'. As a result one of the changes
> is to create a new 'category'-type structure for definitions.
> There will be a new keyword, like the category keyword,
> 'definition'.
>
> Tim
>
>
> On Fri, Mar 11, 2022 at 9:46 AM Tim Daly <[email protected]> wrote:
>
>> The github lockout continues...
>>
>> I'm spending some time adding examples to source code.
>>
>> Any function can have ++X comments added. These will
>> appear as examples when the function is )display For example,
>> in PermutationGroup there is a function 'strongGenerators'
>> defined as:
>>
>>   strongGenerators : % -> L PERM S
>>     ++ strongGenerators(gp) returns strong generators for
>>     ++ the group gp.
>>     ++
>>     ++X S:List(Integer) :=3D [1,2,3,4]
>>     ++X G :=3D symmetricGroup(S)
>>     ++X strongGenerators(G)
>>
>>
>>
>> Later, in the interpreter we see:
>>
>>
>>
>>
>> )d op strongGenerators
>>
>>   There is one exposed function called strongGenerators :
>>       [1] PermutationGroup(D2) -> List(Permutation(D2)) from
>>                PermutationGroup(D2)
>>                  if D2 has SETCAT
>>
>>   Examples of strongGenerators from PermutationGroup
>>
>>   S:List(Integer) :=3D [1,2,3,4]
>>   G :=3D symmetricGroup(S)
>>   strongGenerators(G)
>>
>>
>>
>>
>> This will show a working example for functions that the
>> user can copy and use. It is especially useful to show how
>> to construct working arguments.
>>
>> These "example" functions are run at build time when
>> the make command looks like
>>     make TESTSET=3Dalltests
>>
>> I hope to add this documentation to all Axiom functions.
>>
>> In addition, the plan is to add these function calls to the
>> usual test documentation. That means that all of these examples
>> will be run and show their output in the final distribution
>> (mnt/ubuntu/doc/src/input/*.dvi files) so the user can view
>> the expected output.
>>
>> Tim
>>
>>
>>
>>
>> On Fri, Feb 25, 2022 at 6:05 PM Tim Daly <[email protected]> wrote:
>>
>>> It turns out that creating SPAD-looking output is trivial
>>> in Common Lisp. Each class can have a custom print
>>> routine so signatures and ++ comments can each be
>>> printed with their own format.
>>>
>>> To ensure that I maintain compatibility I'll be printing
>>> the categories and domains so they look like SPAD code,
>>> at least until I get the proof technology integrated. I will
>>> probably specialize the proof printers to look like the
>>> original LEAN proof syntax.
>>>
>>> Internally, however, it will all be Common Lisp.
>>>
>>> Common Lisp makes so many desirable features so easy.
>>> It is possible to trace dynamically at any level. One could
>>> even write a trace that showed how Axiom arrived at the
>>> solution. Any domain could have special case output syntax
>>> without affecting any other domain so one could write a
>>> tree-like output for proofs. Using greek characters is trivial
>>> so the input and output notation is more mathematical.
>>>
>>> Tim
>>>
>>>
>>> On Thu, Feb 24, 2022 at 10:24 AM Tim Daly <[email protected]> wrote:
>>>
>>>> Axiom's SPAD code compiles to Common Lisp.
>>>> The AKCL version of Common Lisp compiles to C.
>>>> Three languages and 2 compilers is a lot to maintain.
>>>> Further, there are very few people able to write SPAD
>>>> and even fewer people able to maintain it.
>>>>
>>>> I've decided that the SANE version of Axiom will be
>>>> implemented in pure Common Lisp. I've outlined Axiom's
>>>> category / type hierarchy in the Common Lisp Object
>>>> System (CLOS). I am now experimenting with re-writing
>>>> the functions into Common Lisp.
>>>>
>>>> This will have several long-term effects. It simplifies
>>>> the implementation issues. SPAD code blocks a lot of
>>>> actions and optimizations that Common Lisp provides.
>>>> The Common Lisp language has many more people
>>>> who can read, modify, and maintain code. It provides for
>>>> interoperability with other Common Lisp projects with
>>>> no effort. Common Lisp is an international standard
>>>> which ensures that the code will continue to run.
>>>>
>>>> The input / output mathematics will remain the same.
>>>> Indeed, with the new generalizations for first-class
>>>> dependent types it will be more general.
>>>>
>>>> This is a big change, similar to eliminating BOOT code
>>>> and moving to Literate Programming. This will provide a
>>>> better platform for future research work. Current research
>>>> is focused on merging Axiom's computer algebra mathematics
>>>> with Lean's proof language. The goal is to create a system for
>>>>  "computational mathematics".
>>>>
>>>> Research is the whole point of Axiom.
>>>>
>>>> Tim
>>>>
>>>>
>>>>
>>>> On Sat, Jan 22, 2022 at 9:16 PM Tim Daly <[email protected]> wrote:
>>>>
>>>>> I can't stress enough how important it is to listen to Hamming's talk
>>>>> https://www.youtube.com/watch?v=3Da1zDuOPkMSw
>>>>>
>>>>> Axiom will begin to die the day I stop working on it.
>>>>>
>>>>> However, proving Axiom correct "down to the metal", is fundamental.
>>>>> It will merge computer algebra and logic, spawning years of new
>>>>> research.
>>>>>
>>>>> Work on fundamental problems.
>>>>>
>>>>> Tim
>>>>>
>>>>>
>>>>> On Thu, Dec 30, 2021 at 6:46 PM Tim Daly <[email protected]> wrote:
>>>>>
>>>>>> One of the interesting questions when obtaining a result
>>>>>> is "what functions were called and what was their return value?"
>>>>>> Otherwise known as the "show your work" idea.
>>>>>>
>>>>>> There is an idea called the "writer monad" [0], usually
>>>>>> implemented to facilitate logging. We can exploit this
>>>>>> idea to provide "show your work" capability. Each function
>>>>>> can provide this information inside the monad enabling the
>>>>>> question to be answered at any time.
>>>>>>
>>>>>> For those unfamiliar with the monad idea, the best explanation
>>>>>> I've found is this video [1].
>>>>>>
>>>>>> Tim
>>>>>>
>>>>>> [0] Deriving the writer monad from first principles
>>>>>> https://williamyaoh.com/posts/2020-07-26-deriving-writer-monad.html
>>>>>>
>>>>>> [1] The Absolute Best Intro to Monads for Software Engineers
>>>>>> https://www.youtube.com/watch?v=3DC2w45qRc3aU
>>>>>>
>>>>>> On Mon, Dec 13, 2021 at 12:30 AM Tim Daly <[email protected]> wrote=
:
>>>>>>
>>>>>>> ...(snip)...
>>>>>>>
>>>>>>> Common Lisp has an "open compiler". That allows the ability
>>>>>>> to deeply modify compiler behavior using compiler macros
>>>>>>> and macros in general. CLOS takes advantage of this to add
>>>>>>> typed behavior into the compiler in a way that ALLOWS strict
>>>>>>> typing such as found in constructive type theory and ML.
>>>>>>> Judgments, ala Crary, are front-and-center.
>>>>>>>
>>>>>>> Whether you USE the discipline afforded is the real question.
>>>>>>>
>>>>>>> Indeed, the Axiom research struggle is essentially one of how
>>>>>>> to have a disciplined use of first-class dependent types. The
>>>>>>> struggle raises issues of, for example, compiling a dependent
>>>>>>> type whose argument is recursive in the compiled type. Since
>>>>>>> the new type is first-class it can be constructed at what you
>>>>>>> improperly call "run-time". However, it appears that the recursive
>>>>>>> type may have to call the compiler at each recursion to generate
>>>>>>> the next step since in some cases it cannot generate "closed code".
>>>>>>>
>>>>>>> I am embedding proofs (in LEAN language) into the type
>>>>>>> hierarchy so that theorems, which depend on the type hierarchy,
>>>>>>> are correctly inherited. The compiler has to check the proofs of
>>>>>>> functions
>>>>>>> at compile time using these. Hacking up nonsense just won't cut it.
>>>>>>> Think
>>>>>>> of the problem of embedding LEAN proofs in ML or ML in LEAN.
>>>>>>> (Actually, Jeremy Avigad might find that research interesting.)
>>>>>>>
>>>>>>> So Matrix(3,3,Float) has inverses (assuming Float is a
>>>>>>> field (cough)). The type inherits this theorem and proofs of
>>>>>>> functions can use this. But Matrix(3,4,Integer) does not have
>>>>>>> inverses so the proofs cannot use this. The type hierarchy has
>>>>>>> to ensure that the proper theorems get inherited.
>>>>>>>
>>>>>>> Making proof technology work at compile time is hard.
>>>>>>> (Worse yet, LEAN is a moving target. Sigh.)
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> On Thu, Nov 25, 2021 at 9:43 AM Tim Daly <[email protected]> wrote=
:
>>>>>>>
>>>>>>>>
>>>>>>>> As you know I've been re-architecting Axiom to use first class
>>>>>>>> dependent types and proving the algorithms correct. For example,
>>>>>>>> the GCD of natural numbers or the GCD of polynomials.
>>>>>>>>
>>>>>>>> The idea involves "boxing up" the proof with the algorithm (aka
>>>>>>>> proof carrying code) in the ELF file (under a crypto hash so it
>>>>>>>> can't be changed).
>>>>>>>>
>>>>>>>> Once the code is running on the CPU, the proof is run in parallel
>>>>>>>> on the field programmable gate array (FPGA). Intel data center
>>>>>>>> servers have CPUs with built-in FPGAs these days.
>>>>>>>>
>>>>>>>> There is a bit of a disconnect, though. The GCD code is compiled
>>>>>>>> machine code but the proof is LEAN-level.
>>>>>>>>
>>>>>>>> What would be ideal is if the compiler not only compiled the GCD
>>>>>>>> code to machine code, it also compiled the proof to "machine code"=
.
>>>>>>>> That is, for each machine instruction, the FPGA proof checker
>>>>>>>> would ensure that the proof was not violated at the individual
>>>>>>>> instruction level.
>>>>>>>>
>>>>>>>> What does it mean to "compile a proof to the machine code level"?
>>>>>>>>
>>>>>>>> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
>>>>>>>> To quote from the article [0]:
>>>>>>>>
>>>>>>>>    We begin with a simple proof checker, call it A, which is short
>>>>>>>>    enough to verify by the ``social process'' of mathematics -- an=
d
>>>>>>>>   more recently with a theorem prover for a more expressive logic.
>>>>>>>>
>>>>>>>>    We then develop a series of increasingly powerful proof checker=
s,
>>>>>>>>   call the B, C, D, and so on. We show each of these programs only
>>>>>>>>    accepts the same formulas as A, using A to verify B, and B to
>>>>>>>> verify
>>>>>>>>    C, and so on. Then, since we trust A, and A says B is
>>>>>>>> trustworthy, we
>>>>>>>>    can trust B. Then, since we trust B, and B says C is
>>>>>>>> trustworthy, we
>>>>>>>>    can trust C.
>>>>>>>>
>>>>>>>> This gives a technique for "compiling the proof" down the the
>>>>>>>> machine
>>>>>>>> code level. Ideally, the compiler would have judgments for each
>>>>>>>> step of
>>>>>>>> the compilation so that each compile step has a justification. I
>>>>>>>> don't
>>>>>>>> know of any compiler that does this yet. (References welcome).
>>>>>>>>
>>>>>>>> At the machine code level, there are techniques that would allow
>>>>>>>> the FPGA proof to "step in sequence" with the executing code.
>>>>>>>> Some work has been done on using "Hoare Logic for Realistically
>>>>>>>> Modelled Machine Code" (paper attached, Myre07a.pdf),
>>>>>>>> "Decompilation into Logic -- Improved (Myre12a.pdf).
>>>>>>>>
>>>>>>>> So the game is to construct a GCD over some type (Nats, Polys, etc=
.
>>>>>>>> Axiom has 22), compile the dependent type GCD to machine code.
>>>>>>>> In parallel, the proof of the code is compiled to machine code. Th=
e
>>>>>>>> pair is sent to the CPU/FPGA and, while the algorithm runs, the FP=
GA
>>>>>>>> ensures the proof is not violated, instruction by instruction.
>>>>>>>>
>>>>>>>> (I'm ignoring machine architecture issues such pipelining,
>>>>>>>> out-of-order,
>>>>>>>> branch prediction, and other machine-level things to ponder. I'm
>>>>>>>> looking
>>>>>>>> at the RISC-V Verilog details by various people to understand
>>>>>>>> better but
>>>>>>>> it is still a "misty fog" for me.)
>>>>>>>>
>>>>>>>> The result is proven code "down to the metal".
>>>>>>>>
>>>>>>>> Tim
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>> [0]
>>>>>>>> https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/=
index-seo.php/ACL2____MILAWA
>>>>>>>>
>>>>>>>> On Thu, Nov 25, 2021 at 6:05 AM Tim Daly <[email protected]>
>>>>>>>> wrote:
>>>>>>>>
>>>>>>>>>
>>>>>>>>> As you know I've been re-architecting Axiom to use first class
>>>>>>>>> dependent types and proving the algorithms correct. For example,
>>>>>>>>> the GCD of natural numbers or the GCD of polynomials.
>>>>>>>>>
>>>>>>>>> The idea involves "boxing up" the proof with the algorithm (aka
>>>>>>>>> proof carrying code) in the ELF file (under a crypto hash so it
>>>>>>>>> can't be changed).
>>>>>>>>>
>>>>>>>>> Once the code is running on the CPU, the proof is run in parallel
>>>>>>>>> on the field programmable gate array (FPGA). Intel data center
>>>>>>>>> servers have CPUs with built-in FPGAs these days.
>>>>>>>>>
>>>>>>>>> There is a bit of a disconnect, though. The GCD code is compiled
>>>>>>>>> machine code but the proof is LEAN-level.
>>>>>>>>>
>>>>>>>>> What would be ideal is if the compiler not only compiled the GCD
>>>>>>>>> code to machine code, it also compiled the proof to "machine code=
".
>>>>>>>>> That is, for each machine instruction, the FPGA proof checker
>>>>>>>>> would ensure that the proof was not violated at the individual
>>>>>>>>> instruction level.
>>>>>>>>>
>>>>>>>>> What does it mean to "compile a proof to the machine code level"?
>>>>>>>>>
>>>>>>>>> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
>>>>>>>>> To quote from the article [0]:
>>>>>>>>>
>>>>>>>>>    We begin with a simple proof checker, call it A, which is shor=
t
>>>>>>>>>    enough to verify by the ``social process'' of mathematics -- a=
nd
>>>>>>>>>   more recently with a theorem prover for a more expressive logic=
.
>>>>>>>>>
>>>>>>>>>    We then develop a series of increasingly powerful proof
>>>>>>>>> checkers,
>>>>>>>>>   call the B, C, D, and so on. We show each of these programs onl=
y
>>>>>>>>>    accepts the same formulas as A, using A to verify B, and B to
>>>>>>>>> verify
>>>>>>>>>    C, and so on. Then, since we trust A, and A says B is
>>>>>>>>> trustworthy, we
>>>>>>>>>    can trust B. Then, since we trust B, and B says C is
>>>>>>>>> trustworthy, we
>>>>>>>>>    can trust C.
>>>>>>>>>
>>>>>>>>> This gives a technique for "compiling the proof" down the the
>>>>>>>>> machine
>>>>>>>>> code level. Ideally, the compiler would have judgments for each
>>>>>>>>> step of
>>>>>>>>> the compilation so that each compile step has a justification. I
>>>>>>>>> don't
>>>>>>>>> know of any compiler that does this yet. (References welcome).
>>>>>>>>>
>>>>>>>>> At the machine code level, there are techniques that would allow
>>>>>>>>> the FPGA proof to "step in sequence" with the executing code.
>>>>>>>>> Some work has been done on using "Hoare Logic for Realistically
>>>>>>>>> Modelled Machine Code" (paper attached, Myre07a.pdf),
>>>>>>>>> "Decompilation into Logic -- Improved (Myre12a.pdf).
>>>>>>>>>
>>>>>>>>> So the game is to construct a GCD over some type (Nats, Polys, et=
c.
>>>>>>>>> Axiom has 22), compile the dependent type GCD to machine code.
>>>>>>>>> In parallel, the proof of the code is compiled to machine code. T=
he
>>>>>>>>> pair is sent to the CPU/FPGA and, while the algorithm runs, the
>>>>>>>>> FPGA
>>>>>>>>> ensures the proof is not violated, instruction by instruction.
>>>>>>>>>
>>>>>>>>> (I'm ignoring machine architecture issues such pipelining,
>>>>>>>>> out-of-order,
>>>>>>>>> branch prediction, and other machine-level things to ponder. I'm
>>>>>>>>> looking
>>>>>>>>> at the RISC-V Verilog details by various people to understand
>>>>>>>>> better but
>>>>>>>>> it is still a "misty fog" for me.)
>>>>>>>>>
>>>>>>>>> The result is proven code "down to the metal".
>>>>>>>>>
>>>>>>>>> Tim
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> [0]
>>>>>>>>> https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual=
/index-seo.php/ACL2____MILAWA
>>>>>>>>>
>>>>>>>>> On Sat, Nov 13, 2021 at 5:28 PM Tim Daly <[email protected]>
>>>>>>>>> wrote:
>>>>>>>>>
>>>>>>>>>> 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/d=
p/0262610744
>>>>>>>>>> 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 System=
s
>>>>>>>>>>> (ref: Kinematics of Self Reproducing Machines
>>>>>>>>>>> http://www.molecularassembler.com/KSRM.htm)
>>>>>>>>>>>
>>>>>>>>>>> which led to watching "Strange Dreams of Stranger Loops" by Wil=
l
>>>>>>>>>>> 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 representatio=
n
>>>>>>>>>>> will change behavior.
>>>>>>>>>>>
>>>>>>>>>>> This leads to two thoughts in the SANE research.
>>>>>>>>>>>
>>>>>>>>>>> First, "Declarative Representation". That is, most of the thing=
s
>>>>>>>>>>> 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-0=
0625.pdf
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> [5] OPS5 User Manual
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> https://kilthub.cmu.edu/articles/journal_contribution/OPS5_u=
ser_s_manual/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 hav=
e
>>>>>>>>>>>>>> > 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 o=
r
>>>>>>>>>>>>>> > 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 201=
8
>>>>>>>>>>>>>> Turing
>>>>>>>>>>>>>> > Award for Deep Learning
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> https://people.idsia.ch/~juergen/scientific-integrity-turing=
-award-deep-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 believe
>>>>>>>>>>>>>> > I've seen these books mentioned in any recent bibliography=
.
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> https://mitpress.mit.edu/books/parallel-distributed-processi=
ng-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-sci=
entific-software.html
>>>>>>>>>>>>>> >>
>>>>>>>>>>>>>> >> which is a really interesting read. For example"
>>>>>>>>>>>>>> >>
>>>>>>>>>>>>>> >>  [Hatton1994], is now a quarter of a century old, but its
>>>>>>>>>>>>>> conclusions
>>>>>>>>>>>>>> >> 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 commutativ=
e
>>>>>>>>>>>>>> >>>> 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 t=
he
>>>>>>>>>>>>>> >>>> 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 compile=
r
>>>>>>>>>>>>>> >>>> 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 mechanis=
m
>>>>>>>>>>>>>> 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 t=
o
>>>>>>>>>>>>>> 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 successiv=
e
>>>>>>>>>>>>>> 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 languagesJanuar=
y
>>>>>>>>>>>>>> 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 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 o=
n
>>>>>>>>>>>>>> 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   =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 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 jus=
t
>>>>>>>>>>>>>> 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 <[email protected]> wrote:
>>>>>>>>>>>>>> >>>>>>>> Axiom is based on first-class dependent types.
>>>>>>>>>>>>>> Deciding when
>>>>>>>>>>>>>> >>>>>>>> two types are equivalent may involve computation. S=
ee
>>>>>>>>>>>>>> >>>>>>>> Christiansen, David Thrane "Checking Dependent Type=
s
>>>>>>>>>>>>>> with
>>>>>>>>>>>>>> >>>>>>>> Normalization by Evaluation" (2019)
>>>>>>>>>>>>>> >>>>>>>>
>>>>>>>>>>>>>> >>>>>>>> This puts an interesting constraint on building
>>>>>>>>>>>>>> types. The
>>>>>>>>>>>>>> >>>>>>>> constructed types has to export a function to decid=
e
>>>>>>>>>>>>>> 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 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 a=
n
>>>>>>>>>>>>>> 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 o=
f
>>>>>>>>>>>>>> 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 "se=
a
>>>>>>>>>>>>>> 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 easil=
y
>>>>>>>>>>>>>> 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 <[email protected]> wrote:
>>>>>>>>>>>>>> >>>>>>>>>> The systems I use have the interesting property o=
f
>>>>>>>>>>>>>> >>>>>>>>>> "Living within the compiler".
>>>>>>>>>>>>>> >>>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>>> Lisp, Forth, Emacs, and other systems that presen=
t
>>>>>>>>>>>>>> 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=3DW2hagw1VhhI&feature=3Dyout=
u.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 withi=
n
>>>>>>>>>>>>>> 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 <[email protected]> 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 compil=
e
>>>>>>>>>>>>>> time without
>>>>>>>>>>>>>> >>>>>>>>>>> overhead
>>>>>>>>>>>>>> >>>>>>>>>>> where possible. Since this is not always possibl=
e
>>>>>>>>>>>>>> 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 th=
e
>>>>>>>>>>>>>> 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 intermediat=
e
>>>>>>>>>>>>>> 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 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 <[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 Axio=
m
>>>>>>>>>>>>>> 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 accurat=
e
>>>>>>>>>>>>>> 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
>>>>>>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>>
>>>>>>>>>>>>>> >>>>>>>>
>>>>>>>>>>>>>> >>>>>>>
>>>>>>>>>>>>>> >>>>>>
>>>>>>>>>>>>>> >>>>>
>>>>>>>>>>>>>> >>>>
>>>>>>>>>>>>>> >>>
>>>>>>>>>>>>>> >>
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>
>>>>>>>>>>>>>

--00000000000091c88405dadc582b
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>I have a deep interest in self-modifying programs. Th=
ese are</div><div>trivial to create in lisp. The question is how to structu=
re a computer</div><div>algebra program so it could be dynamically modified=
 but still <br></div><div>well-structured. This is especially important sin=
ce the user can</div><div>create new logical types at runtime.</div><div><b=
r></div><div>One innovation, which I have never seen anywhere, is to struct=
ure</div><div>the program in a spreadsheet fashion. Spreadsheets cells can<=
/div><div>reference other spreadsheet cells. Spreadsheets have a well-defin=
ed</div><div>evaluation method. This is equivalent to a form of object-orie=
nted</div><div>programming where each cell is an object and has a well-defi=
ned</div><div>inheritance hierarchy through other cells. Simple manipulatio=
n</div><div>allows insertion, deletion, or modification of these chains at =
any time.</div><div><br></div><div>So by structuring a computer algebra pro=
gram like a spreadsheet</div><div>I am able to dynamically adjust a program=
 to fit the problem to be</div><div>solved, track which cells are needed, a=
nd optimize the program.</div><div><br></div><div>Spreadsheets do this natu=
rally but I&#39;m unaware of any non-spreadsheet</div><div>program that rel=
ies on that organization.</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 Sun, Mar 13, 2022 at 4:01 AM Tim Daly &lt;<a href=3D"mailto:axiomcas@gma=
il.com">[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gma=
il_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,2=
04,204);padding-left:1ex"><div dir=3D"ltr"><div>Axiom has an awkward &#39;a=
ttributes&#39; category structure.</div><div><br></div><div>In the SANE ver=
sion it is clear that these attributes are much</div><div>closer to logic &=
#39;definitions&#39;. As a result one of the changes</div><div>is to create=
 a new &#39;category&#39;-type structure for definitions.</div><div>There w=
ill be a new keyword, like the category keyword,</div><div>&#39;definition&=
#39;.</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 Fri, Mar 11, 2022=
 at 9:46 AM Tim Daly &lt;<a href=3D"mailto:[email protected]" target=3D"_b=
lank">[email protected]</a>&gt; 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>The github lockout continues.=
.. <br></div><div><br></div><div>I&#39;m spending some time adding examples=
 to source code.</div><div><br></div><div>Any function can have ++X comment=
s added. These will</div><div>appear as examples when the function is )disp=
lay For example,</div><div>in PermutationGroup there is a function &#39;str=
ongGenerators&#39;</div><div>defined as:</div><div><br></div><div>=C2=A0 st=
rongGenerators : % -&gt; L PERM S</div><div>=C2=A0=C2=A0=C2=A0 ++ strongGen=
erators(gp) returns strong generators for</div><div>=C2=A0=C2=A0=C2=A0 ++ t=
he group gp.</div><div>=C2=A0=C2=A0=C2=A0 ++</div><div>=C2=A0=C2=A0=C2=A0 +=
+X S:List(Integer) :=3D [1,2,3,4]</div><div>=C2=A0=C2=A0=C2=A0 ++X G :=3D s=
ymmetricGroup(S)</div><div>=C2=A0=C2=A0=C2=A0 ++X strongGenerators(G)</div>=
<div><br></div><div><br></div><div><br></div><div>Later, in the interpreter=
 we see:</div><div><br></div><div><br></div><div><br></div><div><br></div><=
div>)d op strongGenerators</div><div><br></div><div>=C2=A0 There is one exp=
osed function called strongGenerators :</div><div>=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0 [1] PermutationGroup(D2) -&gt; List(Permutation(D2)) from</div><div>=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0 PermutationGroup(D2)</div><div>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 if D2 has S=
ETCAT</div><div><br></div><div>=C2=A0 Examples of strongGenerators from Per=
mutationGroup</div><div>=C2=A0 <br></div><div>=C2=A0 S:List(Integer) :=3D [=
1,2,3,4]</div><div>=C2=A0 G :=3D symmetricGroup(S)</div><div>=C2=A0 strongG=
enerators(G)</div><div><br></div><div><br></div><div><br></div><div><br></d=
iv><div>This will show a working example for functions that the</div><div>u=
ser can copy and use. It is especially useful to show how</div><div>to cons=
truct working arguments.</div><div><br></div><div>These &quot;example&quot;=
 functions are run at build time when</div><div>the make command looks like=
</div><div>=C2=A0=C2=A0=C2=A0 make TESTSET=3Dalltests<br></div><div><br></d=
iv><div>I hope to add this documentation to all Axiom functions.</div><div>=
<br></div><div>In addition, the plan is to add these function calls to the<=
/div><div>usual test documentation. That means that all of these examples</=
div><div>will be run and show their output in the final distribution</div><=
div>(mnt/ubuntu/doc/src/input/*.dvi files) so the user can view</div><div>t=
he expected output.<br></div><div><br></div><div>Tim</div><div><br></div><d=
iv><br></div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=
=3D"ltr" class=3D"gmail_attr">On Fri, Feb 25, 2022 at 6:05 PM Tim Daly &lt;=
<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]<=
/a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0=
px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><=
div dir=3D"ltr"><div>It turns out that creating SPAD-looking output is triv=
ial <br></div><div>in Common Lisp. Each class can have a custom print</div>=
<div>routine so signatures and ++ comments can each be</div><div>printed wi=
th their own format.</div><div><br></div><div>To ensure that I maintain com=
patibility I&#39;ll be printing</div><div>the categories and domains so the=
y look like SPAD code,</div><div>at least until I get the proof technology =
integrated. I will</div><div>probably specialize the proof printers to look=
 like the</div><div>original LEAN proof syntax.</div><div><br></div><div>In=
ternally, however, it will all be Common Lisp.</div><div><br></div><div>Com=
mon Lisp makes so many desirable features so easy.</div><div>It is possible=
 to trace dynamically at any level. One could</div><div>even write a trace =
that showed how Axiom arrived at the</div><div>solution. Any domain could h=
ave special case output syntax</div><div>without affecting any other domain=
 so one could write a</div><div>tree-like output for proofs. Using greek ch=
aracters is trivial</div><div>so the input and output notation is more math=
ematical.<br></div><div><br></div><div>Tim</div><div><br></div></div><br><d=
iv class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Feb =
24, 2022 at 10:24 AM Tim Daly &lt;<a href=3D"mailto:[email protected]" tar=
get=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote class=
=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rg=
b(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>Axiom&#39;s SPAD cod=
e compiles to Common Lisp.</div><div>The AKCL version of Common Lisp compil=
es to C.</div><div>Three languages and 2 compilers is a lot to maintain.</d=
iv><div>Further, there are very few people able to write SPAD</div><div>and=
 even fewer people able to maintain it.<br></div><div><br></div><div>I&#39;=
ve decided that the SANE version of Axiom will be <br></div><div>implemente=
d in pure Common Lisp. I&#39;ve outlined Axiom&#39;s<br></div><div>category=
 / type hierarchy in the Common Lisp Object</div><div>System (CLOS). I am n=
ow experimenting with re-writing</div><div>the functions into Common Lisp.<=
br></div><div><br></div><div>This will have several long-term effects. It s=
implifies</div><div>the implementation issues. SPAD code blocks a lot of</d=
iv><div>actions and optimizations that Common Lisp provides.</div><div>The =
Common Lisp language has many more people<br></div><div>who can read, modif=
y, and maintain code. It provides for</div><div>interoperability with other=
 Common Lisp projects with</div><div>no effort. Common Lisp is an internati=
onal standard</div><div>which ensures that the code will continue to run.<b=
r></div><div><br></div><div>The input / output mathematics will remain the =
same.</div><div>Indeed, with the new generalizations for first-class</div><=
div>dependent types it will be more general.</div><div><br></div><div>This =
is a big change, similar to eliminating BOOT code</div><div>and moving to L=
iterate Programming. This will provide a</div><div>better platform for futu=
re research work. Current research</div><div>is focused on merging Axiom&#3=
9;s computer algebra mathematics</div><div>with Lean&#39;s proof language. =
The goal is to create a system for</div><div>=C2=A0&quot;computational math=
ematics&quot;.<br></div><div><br></div><div>Research is the whole point of =
Axiom.</div><div><br></div><div>Tim</div><div><br></div><div><br></div></di=
v><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On S=
at, Jan 22, 2022 at 9:16 PM Tim Daly &lt;<a href=3D"mailto:[email protected]=
om" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquot=
e class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px s=
olid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>I can&#39;t s=
tress enough how important it is to listen to Hamming&#39;s talk</div><div>=
<a href=3D"https://www.youtube.com/watch?v=3Da1zDuOPkMSw" target=3D"_blank"=
>https://www.youtube.com/watch?v=3Da1zDuOPkMSw</a></div><div><br></div><div=
>Axiom will begin to die the day I stop working on it.</div><div><br></div>=
<div>However, proving Axiom correct &quot;down to the metal&quot;, is funda=
mental.</div><div>It will merge computer algebra and logic, spawning years =
of new</div><div>research.</div><div><br></div><div>Work on fundamental pro=
blems.</div><div><br></div><div>Tim</div><div><br></div></div><br><div clas=
s=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Dec 30, 202=
1 at 6:46 PM Tim Daly &lt;<a href=3D"mailto:[email protected]" target=3D"_=
blank">[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gmai=
l_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,20=
4,204);padding-left:1ex"><div dir=3D"ltr"><div>One of the interesting quest=
ions when obtaining a result</div><div>is &quot;what functions were called =
and what was their return value?&quot;</div><div>Otherwise known as the &qu=
ot;show your work&quot; idea.</div><div><br></div><div>There is an idea cal=
led the &quot;writer monad&quot; [0], usually <br></div><div>implemented to=
 facilitate logging. We can exploit this</div><div>idea to provide &quot;sh=
ow your work&quot; capability. Each function</div><div>can provide this inf=
ormation inside the monad enabling the</div><div>question to be answered at=
 any time.</div><div><br></div><div>For those unfamiliar with the monad ide=
a, the best explanation</div><div>I&#39;ve found is this video [1].</div><d=
iv><br></div><div>Tim<br></div><div><br></div><div>[0] Deriving the writer =
monad from first principles<br></div><div><a href=3D"https://williamyaoh.co=
m/posts/2020-07-26-deriving-writer-monad.html" target=3D"_blank">https://wi=
lliamyaoh.com/posts/2020-07-26-deriving-writer-monad.html</a></div><div><br=
></div><div>[1] The Absolute Best Intro to Monads for Software Engineers</d=
iv><div><a href=3D"https://www.youtube.com/watch?v=3DC2w45qRc3aU" target=3D=
"_blank">https://www.youtube.com/watch?v=3DC2w45qRc3aU</a></div></div><br><=
div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, Dec=
 13, 2021 at 12:30 AM Tim Daly &lt;<a href=3D"mailto:[email protected]" ta=
rget=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote clas=
s=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid r=
gb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>...(snip)...<br></d=
iv><div><br></div><div>Common Lisp has an &quot;open compiler&quot;. That a=
llows the ability</div><div>to deeply modify compiler behavior using compil=
er macros</div><div>and macros in general. CLOS takes advantage of this to =
add</div><div>typed behavior into the compiler in a way that ALLOWS strict<=
/div><div>typing such as found in constructive type theory and ML.</div><di=
v>Judgments, ala Crary, are front-and-center.<br></div><div><br></div><div>=
Whether you USE the discipline afforded is the real question.</div><div><br=
></div><div>Indeed, the Axiom research struggle is essentially one of how</=
div><div>to have a disciplined use of first-class dependent types. The</div=
><div>struggle raises issues of, for example, compiling a dependent</div><d=
iv>type whose argument is recursive in the compiled type. Since</div><div>t=
he new type is first-class it can be constructed at what you</div><div>impr=
operly call &quot;run-time&quot;. However, it appears that the recursive</d=
iv><div>type may have to call the compiler at each recursion to generate</d=
iv><div>the next step since in some cases it cannot generate &quot;closed c=
ode&quot;.<br></div><div><br></div><div>I am embedding proofs (in LEAN lang=
uage) into the type</div><div>hierarchy so that theorems, which depend on t=
he type hierarchy,<br></div><div>are correctly inherited. The compiler has =
to check the proofs of functions</div><div>at compile time using these. Hac=
king up nonsense just won&#39;t cut it. Think</div><div>of the problem of e=
mbedding LEAN proofs in ML or ML in LEAN.</div><div>(Actually, Jeremy Aviga=
d might find that research interesting.)</div><div><br></div><div>So Matrix=
(3,3,Float) has inverses (assuming Float is a</div><div>field (cough)). The=
 type inherits this theorem and proofs of</div><div>functions can use this.=
 But Matrix(3,4,Integer) does not have</div><div>inverses so the proofs can=
not use this. The type hierarchy has</div><div>to ensure that the proper th=
eorems get inherited.<br></div><div><br></div><div>Making proof technology =
work at compile time is hard.</div><div>(Worse yet, LEAN is a moving target=
. Sigh.)<br></div><div><br><br></div></div><br><div class=3D"gmail_quote"><=
div dir=3D"ltr" class=3D"gmail_attr">On Thu, Nov 25, 2021 at 9:43 AM Tim Da=
ly &lt;<a href=3D"mailto:[email protected]" target=3D"_blank">axiomcas@gma=
il.com</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"m=
argin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left=
:1ex"><div dir=3D"ltr"><div dir=3D"ltr"><div><br></div><div dir=3D"ltr"><di=
v>As you know I&#39;ve been re-architecting Axiom to use first class</div><=
div>dependent types and proving the algorithms correct. For example,</div><=
div>the GCD of natural numbers or the GCD of polynomials.</div><div><br></d=
iv><div>The idea involves &quot;boxing up&quot; the proof with the algorith=
m (aka</div><div>proof carrying code) in the ELF file (under a crypto hash =
so it</div><div>can&#39;t be changed).</div><div><br></div><div>Once the co=
de is running on the CPU, the proof is run in parallel</div><div>on the fie=
ld programmable gate array (FPGA). Intel data center</div><div>servers have=
 CPUs with built-in FPGAs these days.</div><div><br></div><div>There is a b=
it of a disconnect, though. The GCD code is compiled</div><div>machine code=
 but the proof is LEAN-level.</div><div><br></div><div>What would be ideal =
is if the compiler not only compiled the GCD</div><div>code to machine code=
, it also compiled the proof to &quot;machine code&quot;.</div><div>That is=
, for each machine instruction, the FPGA proof checker</div><div>would ensu=
re that the proof was not violated at the individual</div><div>instruction =
level.<br></div><div><br></div><div>What does it mean to &quot;compile a pr=
oof to the machine code level&quot;?</div><div><br></div><div>The Milawa ef=
fort (Myre14.pdf) does incremental proofs in layers.</div><div>To quote fro=
m the article [0]:<br></div><div><br></div><div>=C2=A0=C2=A0 We begin with =
a simple proof checker, call it A, which is short</div><div>=C2=A0=C2=A0 en=
ough to verify by the ``social process&#39;&#39; of mathematics -- and</div=
><div>=C2=A0 more recently with a theorem prover for a more expressive logi=
c.</div><div><br></div><div>=C2=A0=C2=A0 We then develop a series of increa=
singly powerful proof checkers,</div><div>=C2=A0 call the B, C, D, and so o=
n. We show each of these programs only</div><div>=C2=A0=C2=A0 accepts the s=
ame formulas as A, using A to verify B, and B to verify</div><div>=C2=A0=C2=
=A0 C, and so on. Then, since we trust A, and A says B is trustworthy, we</=
div><div>=C2=A0=C2=A0 can trust B. Then, since we trust B, and B says C is =
trustworthy, we</div><div>=C2=A0=C2=A0 can trust C. <br></div><div><br></di=
v><div>This gives a technique for &quot;compiling the proof&quot; down the =
the machine</div><div>code level. Ideally, the compiler would have judgment=
s for each step of</div><div>the compilation so that each compile step has =
a justification. I don&#39;t</div><div>know of any compiler that does this =
yet. (References welcome).<br></div><div><div><br></div><div>At the machine=
 code level, there are techniques that would allow</div><div>the FPGA proof=
 to &quot;step in sequence&quot; with the executing code.<br></div><div>Som=
e work has been done on using &quot;Hoare Logic for Realistically</div><div=
>Modelled Machine Code&quot; (paper attached, Myre07a.pdf),</div><div>&quot=
;Decompilation into Logic -- Improved (Myre12a.pdf).</div><div><br></div><d=
iv>So the game is to construct a GCD over some type (Nats, Polys, etc.</div=
><div>Axiom has 22), compile the dependent type GCD to machine code.</div><=
div>In parallel, the proof of the code is compiled to machine code. The</di=
v><div>pair is sent to the CPU/FPGA and, while the algorithm runs, the FPGA=
</div><div>ensures the proof is not violated, instruction by instruction.</=
div><div><br></div><div>(I&#39;m ignoring machine architecture issues such =
pipelining, out-of-order,</div><div>branch prediction, and other machine-le=
vel things to ponder. I&#39;m looking</div><div>at the RISC-V Verilog detai=
ls by various people to understand better but</div><div>it is still a &quot=
;misty fog&quot; for me.)<br></div><div><br></div><div>The result is proven=
 code &quot;down to the metal&quot;.</div><div><br></div><div>Tim</div><div=
><br></div><div><br></div><div><br></div><div>[0] <a href=3D"https://www.cs=
.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____M=
ILAWA" target=3D"_blank">https://www.cs.utexas.edu/users/moore/acl2/manuals=
/current/manual/index-seo.php/ACL2____MILAWA</a></div></div></div></div></d=
iv><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On =
Thu, Nov 25, 2021 at 6:05 AM Tim Daly &lt;<a href=3D"mailto:axiomcas@gmail.=
com" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquo=
te 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"><br><div dir=3D"l=
tr"><div>As you know I&#39;ve been re-architecting Axiom to use first class=
</div><div>dependent types and proving the algorithms correct. For example,=
</div><div>the GCD of natural numbers or the GCD of polynomials.</div><div>=
<br></div><div>The idea involves &quot;boxing up&quot; the proof with the a=
lgorithm (aka</div><div>proof carrying code) in the ELF file (under a crypt=
o hash so it</div><div>can&#39;t be changed).</div><div><br></div><div>Once=
 the code is running on the CPU, the proof is run in parallel</div><div>on =
the field programmable gate array (FPGA). Intel data center</div><div>serve=
rs have CPUs with built-in FPGAs these days.</div><div><br></div><div>There=
 is a bit of a disconnect, though. The GCD code is compiled</div><div>machi=
ne code but the proof is LEAN-level.</div><div><br></div><div>What would be=
 ideal is if the compiler not only compiled the GCD</div><div>code to machi=
ne code, it also compiled the proof to &quot;machine code&quot;.</div><div>=
That is, for each machine instruction, the FPGA proof checker</div><div>wou=
ld ensure that the proof was not violated at the individual</div><div>instr=
uction level.<br></div><div><br></div><div>What does it mean to &quot;compi=
le a proof to the machine code level&quot;?</div><div><br></div><div>The Mi=
lawa effort (Myre14.pdf) does incremental proofs in layers.</div><div>To qu=
ote from the article [0]:<br></div><div><br></div><div>=C2=A0=C2=A0 We begi=
n with a simple proof checker, call it A, which is short</div><div>=C2=A0=
=C2=A0 enough to verify by the ``social process&#39;&#39; of mathematics --=
 and</div><div>=C2=A0 more recently with a theorem prover for a more expres=
sive logic.</div><div><br></div><div>=C2=A0=C2=A0 We then develop a series =
of increasingly powerful proof checkers,</div><div>=C2=A0 call the B, C, D,=
 and so on. We show each of these programs only</div><div>=C2=A0=C2=A0 acce=
pts the same formulas as A, using A to verify B, and B to verify</div><div>=
=C2=A0=C2=A0 C, and so on. Then, since we trust A, and A says B is trustwor=
thy, we</div><div>=C2=A0=C2=A0 can trust B. Then, since we trust B, and B s=
ays C is trustworthy, we</div><div>=C2=A0=C2=A0 can trust C. <br></div><div=
><br></div><div>This gives a technique for &quot;compiling the proof&quot; =
down the the machine</div><div>code level. Ideally, the compiler would have=
 judgments for each step of</div><div>the compilation so that each compile =
step has a justification. I don&#39;t</div><div>know of any compiler that d=
oes this yet. (References welcome).<br></div><div><div><br></div><div>At th=
e machine code level, there are techniques that would allow</div><div>the F=
PGA proof to &quot;step in sequence&quot; with the executing code.<br></div=
><div>Some work has been done on using &quot;Hoare Logic for Realistically<=
/div><div>Modelled Machine Code&quot; (paper attached, Myre07a.pdf),</div><=
div>&quot;Decompilation into Logic -- Improved (Myre12a.pdf).</div><div><br=
></div><div>So the game is to construct a GCD over some type (Nats, Polys, =
etc.</div><div>Axiom has 22), compile the dependent type GCD to machine cod=
e.</div><div>In parallel, the proof of the code is compiled to machine code=
. The</div><div>pair is sent to the CPU/FPGA and, while the algorithm runs,=
 the FPGA</div><div>ensures the proof is not violated, instruction by instr=
uction.</div><div><br></div><div>(I&#39;m ignoring machine architecture iss=
ues such pipelining, out-of-order,</div><div>branch prediction, and other m=
achine-level things to ponder. I&#39;m looking</div><div>at the RISC-V Veri=
log details by various people to understand better but</div><div>it is stil=
l a &quot;misty fog&quot; for me.)<br></div><div><br></div><div>The result =
is proven code &quot;down to the metal&quot;.</div><div><br></div><div>Tim<=
/div><div><br></div><div><br></div><div><br></div><div>[0] <a href=3D"https=
://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/=
ACL2____MILAWA" target=3D"_blank">https://www.cs.utexas.edu/users/moore/acl=
2/manuals/current/manual/index-seo.php/ACL2____MILAWA</a></div></div></div>=
</div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">=
On Sat, Nov 13, 2021 at 5:28 PM Tim Daly &lt;<a href=3D"mailto:axiomcas@gma=
il.com" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><block=
quote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1=
px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>Full supp=
ort for general, first-class dependent types requires</div><div>some change=
s to the Axiom design. That implies some language</div><div>design question=
s.</div><div><br></div><div>Given that mathematics is such a general subjec=
t with a lot of</div><div>&quot;local&quot; notation and ideas (witness log=
ical judgment notation)</div><div>careful thought is needed to design a lan=
guage that is able to</div><div>handle a wide range.</div><div><br></div><d=
iv>Normally language design is a two-level process. The language</div><div>=
designer creates a language and then an implementation. Various</div><div>d=
esign choices affect the final language.<br></div><div><br></div><div>There=
 is &quot;The Metaobject Protocol&quot; (MOP)<br></div><div><a href=3D"http=
s://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kiczales/dp/0262610744" t=
arget=3D"_blank">https://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kicz=
ales/dp/0262610744</a></div><div>which encourages a three-level process. Th=
e language designer <br></div><div>works at a Metalevel to design a family =
of languages, then the</div><div>language specializations, then the impleme=
ntation. A MOP design</div><div>allows the language user to optimize the la=
nguage to their problem.</div><div><br></div><div>A simple paper on the sub=
ject is &quot;Metaobject Protocols&quot;</div><div><a href=3D"https://users=
.cs.duke.edu/~vahdat/ps/mop.pdf" target=3D"_blank">https://users.cs.duke.ed=
u/~vahdat/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">O=
n Mon, Oct 25, 2021 at 7:42 PM Tim Daly &lt;<a href=3D"mailto:axiomcas@gmai=
l.com" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockq=
uote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1p=
x solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>I have a s=
eparate thread of research on Self-Replicating Systems</div><div>(ref: Kine=
matics of Self Reproducing Machines</div><div><a href=3D"http://www.molecul=
arassembler.com/KSRM.htm" target=3D"_blank">http://www.molecularassembler.c=
om/KSRM.htm</a>)<br></div><div><br></div><div>which led to watching &quot;S=
trange Dreams of Stranger Loops&quot; by Will Byrd</div><div><a href=3D"htt=
ps://www.youtube.com/watch?v=3DAffW-7ika0E" target=3D"_blank">https://www.y=
outube.com/watch?v=3DAffW-7ika0E</a></div><div><br></div><div>Will referenc=
ed a PhD Thesis by Jon Doyle</div><div>&quot;A Model for Deliberation, Acti=
on, and Introspection&quot;</div><div><br></div><div>I also read the thesis=
 by J.C.G. Sturdy</div><div>&quot;A Lisp through the Looking Glass&quot;</d=
iv><div><br></div><div>Self-replication requires the ability to manipulate =
your own</div><div>representation in such a way that changes to that repres=
entation</div><div>will change behavior.</div><div><br></div><div>This lead=
s to two thoughts in the SANE research.</div><div><br></div><div>First, &qu=
ot;Declarative Representation&quot;. That is, most of the things</div><div>=
about the representation should be declarative rather than</div><div>proced=
ural. Applying this idea as much as possible makes it</div><div>easier to u=
nderstand and manipulate.<br></div><div><br></div><div>Second, &quot;Explic=
it Call Stack&quot;. Function calls form an implicit</div><div>call stack. =
This can usually be displayed in a running lisp system.</div><div>However, =
having the call stack explicitly available would mean</div><div>that a syst=
em could &quot;introspect&quot; at the first-class level.</div><div><br></d=
iv><div>These two ideas would make it easy, for example, to let the</div><d=
iv>system &quot;show the work&quot;. One of the normal complaints is that</=
div><div>a system presents an answer but there is no way to know how</div><=
div>that answer was derived. These two ideas make it possible to</div><div>=
understand, display, and even post-answer manipulate</div><div>the intermed=
iate steps.</div><div><br></div><div>Having the intermediate steps also all=
ows proofs to be</div><div>inserted in a step-by-step fashion. This aids th=
e effort to</div><div>have proofs run in parallel with computation at the h=
ardware</div><div>level.<br></div><div><br></div><div>Tim</div><div><br></d=
iv><div><br></div><div><br></div><div><br></div><div><br> </div></div><br><=
div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Oct=
 21, 2021 at 9:50 AM Tim Daly &lt;<a href=3D"mailto:[email protected]" tar=
get=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote class=
=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rg=
b(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>So the current strug=
gle involves the categories in Axiom.</div><div><br></div><div>The categori=
es and domains constructed using categories</div><div>are dependent types. =
When are dependent types &quot;equal&quot;?</div><div>Well, hummmm, that de=
pends on the arguments to the</div><div>constructor.</div><div><br></div><d=
iv>But in order to decide(?) equality we have to evaluate</div><div>the arg=
uments (which themselves can be dependent types).</div><div>Indeed, we may,=
 and in general, we must evaluate the <br></div><div>arguments at compile t=
ime (well, &quot;construction time&quot; as</div><div>there isn&#39;t reall=
y a compiler / interpreter separation anymore.)<br></div><div><br></div><di=
v>That raises the question of what &quot;equality&quot; means. This</div><d=
iv>is not simply a &quot;set equality&quot; relation. It falls into the</di=
v><div>infinite-groupoid of homotopy type theory. In general</div><div>it a=
ppears that deciding category / domain equivalence</div><div>might force us=
 to climb the type hierarchy.</div><div><br></div><div>Beyond that, there i=
s the question of &quot;which proof&quot;</div><div>applies to the resultin=
g object. Proofs depend on their</div><div>assumptions which might be diffe=
rent for different</div><div>constructions. As yet I have no clue how to &q=
uot;index&quot;</div><div>proofs based on their assumptions, nor how to <br=
></div><div>connect these assumptions to the groupoid structure.</div><div>=
<br></div><div>My brain hurts.</div><div><br></div><div>Tim</div><div><br><=
/div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_a=
ttr">On Mon, Oct 18, 2021 at 2:00 AM Tim Daly &lt;<a href=3D"mailto:axiomca=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><=
blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l=
eft:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>&quo=
t;Birthing Computational Mathematics&quot;</div><div><br></div><div>The Axi=
om SANE project is difficult at a very fundamental</div><div>level. The tit=
le &quot;SANE&quot; was chosen due to the various</div><div>words found in =
a thesuarus... &quot;rational&quot;, &quot;coherent&quot;,</div><div>&quot;=
judicious&quot; and &quot;sound&quot;.</div><div><br></div><div>These are v=
ery high level, amorphous ideas. But so is</div><div>the design of SANE. Br=
eaking away from tradition in</div><div>computer algebra, type theory, and =
proof assistants</div><div>is very difficult. Ideas tend to fall into stand=
ard jargon</div><div>which limits both the frame of thinking (e.g. dependen=
t</div><div>types) and the content (e.g. notation).</div><div><br></div><di=
v>Questioning both frame and content is very difficult.</div><div>It is har=
d to even recognize when they are accepted</div><div>&quot;by default&quot;=
 rather than &quot;by choice&quot;. What does the idea<br></div><div>&quot;=
power tools&quot; mean in a primitive, hand labor culture?<br></div><div><b=
r></div><div>Christopher Alexander [0] addresses this problem in</div><div>=
a lot of his writing. Specifically, in his book &quot;Notes on</div><div>th=
e Synthesis of Form&quot;, in his chapter 5 &quot;The Selfconsious</div><di=
v>Process&quot;, he addresses this problem directly. This is a</div><div>&q=
uot;must read&quot; book.<br></div><div><br></div><div>Unlike building desi=
gn and contruction, however, there</div><div>are almost no constraints to u=
se as guides. Alexander</div><div>quotes Plato&#39;s Phaedrus:</div><div><b=
r></div><div>=C2=A0 &quot;First, the taking in of scattered particulars und=
er</div><div>=C2=A0=C2=A0 one Idea, so that everyone understands what is be=
ing</div><div>=C2=A0=C2=A0 talked about ... Second, the separation of the I=
dea</div><div>=C2=A0=C2=A0 into parts, by dividing it at the joints, as nat=
ure</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.&quot;<br></div><div><br></div><di=
v>Lisp, which has been called &quot;clay for the mind&quot; can</div><div>b=
uild virtually anything that can be thought. The <br></div><div>&quot;joint=
s&quot; are also &quot;of one&#39;s choosing&quot; so one is</div><div>both=
 carver and &quot;nature&quot;.<br></div><div><br></div><div>Clearly the pr=
oblem is no longer &quot;the tools&quot;.</div><div>*I* am the problem cons=
training the solution.</div><div>Birthing this &quot;new thing&quot; is slo=
w, difficult, and</div><div>uncertain at best.</div><div><br></div><div>Tim=
</div><div><br></div><div>[0] Alexander, Christopher &quot;Notes on the Syn=
thesis</div><div>of Form&quot; 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 &lt;<a href=3D"mailto:[email protected]" target=3D"_blank">axiomcas@=
gmail.com</a>&gt; 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: writing a paper... I&#39;m not connected to Academia<br>
so anything I&#39;d write would never make it into print.<br>
<br>
&quot;Language level parsing&quot; 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&#39;t understand Platzer&#39;s &quot;funny<br>
fraction notation&quot; (proof judgements) despite being<br>
an expert in Platzer&#39;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&#39;s OPS5 rule based program [5],<br>
and Fahlman&#39;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&#39;ve given it a lot of thought over<br>
the years :-)<br>
<br>
A mathematical language seems to need &gt;6 components<br>
<br>
1) We need some sort of a specification language, possibly<br>
somewhat &#39;propositional&#39; 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&#39;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 &quot;scaffolding&quot;. 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&#39;s &quot;category&quot;<br>
structure has &quot;Category&quot; things like Ring. Claiming<br>
to be a Ring brings in a lot of &quot;Signatures&quot; 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 &quot;Domain&quot; &quot;is a Ring&quot;. Category<br>
theory might provide similar structural scaffolding<br>
(eventually... I&#39;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&#39;t<br>
sufficient to say &quot;undergraduate math&quot; 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 &quot;spreading&quot;. 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>
&quot;commutative&quot; included in the code.<br>
<br>
That way, when you claim to be a &quot;Commutative Ring&quot;<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&#39;s definitions and theorems with<br>
an eye to &quot;spreading&quot; them into the group scaffold of<br>
Axiom.<br>
<br>
4) We need &quot;carriers&quot; (Axiom calls them representations,<br>
aka &quot;REP&quot;). 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 &quot;dense&quot; (all coefficients in a list),<br>
&quot;sparse&quot; (only non-zero coefficients), &quot;recursive&quot;, etc=
.<br>
<br>
A &quot;dense polynomial&quot; and a &quot;sparse polynomial&quot; 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 &quot;got this wrong&quot; because it didn&#39;t sufficiently<br>
separate the REP from the &quot;Domain&quot;. I plan to fix this.<br>
<br>
LEAN ought to have a &quot;data structures&quot; 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 &quot;Domains&quot; (in Axiom speak). That is, we<br>
need a box that holds all of the functions that implement<br>
a &quot;Domain&quot;. For example, a &quot;Polynomial Domain&quot; would<br=
>
hold all of the functions for manipulating polynomials<br>
(e.g polynomial multiplication). The &quot;Domain&quot; box<br>
is a dependent type that:<br>
<br>
=C2=A0 A) has an argument list of &quot;Categories&quot; that this &quot;Do=
main&quot;<br>
=C2=A0 =C2=A0 =C2=A0 box inherits. Thus, the &quot;Integer Domain&quot; inh=
erits<br>
=C2=A0 =C2=A0 =C2=A0 the definitions and axioms from &quot;Commutative&quot=
;<br>
<br>
=C2=A0 =C2=A0 =C2=A0Functions in the &quot;Domain&quot; 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 &quot;REP&quot;<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 &quot;spread&quot; 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 &quot;Square Matrix&quot; 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 &quot;Square Matrix&quot; 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 &#39;2&#39; 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 &quot;Category&quot; could have a signature fo=
r a GCD<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0function and the &quot;Category&quot; could have=
 a default<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0implementation. However, the &quot;Domain&quot; =
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 &quot;Domain&quot; 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 &quot;pre- and post- conditions&quot; 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 &quot;helper&quot; 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&#39;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 &quot;Category&quot;, &quot;Representation&q=
uot;, the &quot;Domain<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0Local&quot;, 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 &quot;books&quot; or &quot;pamphlets&quot; 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&#39;m trying to connect LEAN&#39;s GCD and Axiom&#39;s GCD<=
br>
=C2=A0 =C2=A0 so there is a &quot;computational mathematics&quot; 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 &quot;down to the metal&quot; 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&#39;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 &quot;Chapter on TLA+&quot;<br>
in &quot;Software Specification Methods&quot;<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&#39;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] &quot;ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE&quot;<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 &quot;SCONE&quot;<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 &lt;<a href=3D"mailto:[email protected]" target=3D"_b=
lank">[email protected]</a>&gt; wrote:<br>
&gt; I have tried to maintain a list of names of people who have<br>
&gt; helped Axiom, going all the way back to the pre-Scratchpad<br>
&gt; days. The names are listed at the beginning of each book.<br>
&gt; I also maintain a bibliography of publications I&#39;ve read or<br>
&gt; that have had an indirect influence on Axiom.<br>
&gt;<br>
&gt; Credit is &quot;the coin of the realm&quot;. It is easy to share and w=
rong<br>
&gt; to ignore. It is especially damaging to those in Academia who<br>
&gt; are affected by credit and citations in publications.<br>
&gt;<br>
&gt; Apparently I&#39;m not the only person who feels that way. The ACM<br>
&gt; Turing award seems to have ignored a lot of work:<br>
&gt;<br>
&gt; Scientific Integrity, the 2021 Turing Lecture, and the 2018 Turing<br>
&gt; Award for Deep Learning<br>
&gt; <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>
&gt;<br>
&gt; I worked on an AI problem at IBM Research called Ketazolam.<br>
&gt; (<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>
&gt; and associated 3D chemical drawings with their drug counterparts.<br>
&gt; I used Rumelhart, and McClelland&#39;s books. These books contained<br=
>
&gt; quite a few ideas that seem to be &quot;new and innovative&quot; among=
 the<br>
&gt; machine learning crowd... but the books are from 1987. I don&#39;t bel=
ieve<br>
&gt; I&#39;ve seen these books mentioned in any recent bibliography.<br>
&gt; <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>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; On 9/27/21, Tim Daly &lt;<a href=3D"mailto:[email protected]" target=
=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt; Greg Wilson asked &quot;How Reliable is Scientific Software?&quot;=
<br>
&gt;&gt; <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>
&gt;&gt;<br>
&gt;&gt; which is a really interesting read. For example&quot;<br>
&gt;&gt;<br>
&gt;&gt;=C2=A0 [Hatton1994], is now a quarter of a century old, but its con=
clusions<br>
&gt;&gt; are still fresh. The authors fed the same data into nine commercia=
l<br>
&gt;&gt; geophysical software packages and compared the results; they found=
<br>
&gt;&gt; that, &quot;numerical disagreement grows at around the rate of 1% =
in<br>
&gt;&gt; average absolute difference per 4000 fines of implemented code, an=
d,<br>
&gt;&gt; even worse, the nature of the disagreement is nonrandom&quot; (i.e=
., the<br>
&gt;&gt; authors of different packages make similar mistakes).<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On 9/26/21, Tim Daly &lt;<a href=3D"mailto:[email protected]" tar=
get=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt; I should note that the lastest board I&#39;ve just unboxed<br>
&gt;&gt;&gt; (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; What makes it interesting is that it contains 2 hard<br>
&gt;&gt;&gt; core processors and an FPGA, connected by 9 paths<br>
&gt;&gt;&gt; for communication. The processors can be run<br>
&gt;&gt;&gt; independently so there is the possibility of a parallel<br>
&gt;&gt;&gt; version of some Axiom algorithms (assuming I had<br>
&gt;&gt;&gt; the time, which I don&#39;t).<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Previously either the hard (physical) processor was<br>
&gt;&gt;&gt; separate from the FPGA with minimal communication<br>
&gt;&gt;&gt; or the soft core processor had to be created in the FPGA<br>
&gt;&gt;&gt; and was much slower.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Now the two have been combined in a single chip.<br>
&gt;&gt;&gt; That means that my effort to run a proof checker on<br>
&gt;&gt;&gt; the FPGA and the algorithm on the CPU just got to<br>
&gt;&gt;&gt; the point where coordination is much easier.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Now all I have to do is figure out how to program this<br>
&gt;&gt;&gt; beast.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; There is no such thing as a simple job.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; On 9/26/21, Tim Daly &lt;<a href=3D"mailto:[email protected]"=
 target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt; I&#39;m familiar with most of the traditional approaches<b=
r>
&gt;&gt;&gt;&gt; like Theorema. The bibliography contains most of the<br>
&gt;&gt;&gt;&gt; more interesting sources. [0]<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; There is a difference between traditional approaches to<br=
>
&gt;&gt;&gt;&gt; connecting computer algebra and proofs and my approach.<br=
>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Proving an algorithm, like the GCD, in Axiom is hard.<br>
&gt;&gt;&gt;&gt; There are many GCDs (e.g. NNI vs POLY) and there<br>
&gt;&gt;&gt;&gt; are theorems and proofs passed at runtime in the<br>
&gt;&gt;&gt;&gt; arguments of the newly constructed domains. This<br>
&gt;&gt;&gt;&gt; involves a lot of dependent type theory and issues of<br>
&gt;&gt;&gt;&gt; compile time / runtime argument evaluation. The issues<br>
&gt;&gt;&gt;&gt; that arise are difficult and still being debated in the ty=
pe<br>
&gt;&gt;&gt;&gt; theory community.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I am putting the definitions, theorems, and proofs (DTP)<b=
r>
&gt;&gt;&gt;&gt; directly into the category/domain hierarchy. Each category=
<br>
&gt;&gt;&gt;&gt; will have the DTP specific to it. That way a commutative<b=
r>
&gt;&gt;&gt;&gt; domain will inherit a commutative theorem and a<br>
&gt;&gt;&gt;&gt; non-commutative domain will not.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Each domain will have additional DTPs associated with<br>
&gt;&gt;&gt;&gt; the domain (e.g. NNI vs Integer) as well as any DTPs<br>
&gt;&gt;&gt;&gt; it inherits from the category hierarchy. Functions in the<=
br>
&gt;&gt;&gt;&gt; domain will have associated DTPs.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; A function to be proven will then inherit all of the relev=
ant<br>
&gt;&gt;&gt;&gt; DTPs. The proof will be attached to the function and<br>
&gt;&gt;&gt;&gt; both will be sent to the hardware (proof-carrying code).<b=
r>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; The proof checker, running on a field programmable<br>
&gt;&gt;&gt;&gt; gate array (FPGA), will be checked at runtime in<br>
&gt;&gt;&gt;&gt; parallel with the algorithm running on the CPU<br>
&gt;&gt;&gt;&gt; (aka &quot;trust down to the metal&quot;). (Note that Inte=
l<br>
&gt;&gt;&gt;&gt; and AMD have built CPU/FPGA combined chips,<br>
&gt;&gt;&gt;&gt; currently only available in the cloud.)<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I am (slowly) making progress on the research.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I have the hardware and nearly have the proof<br>
&gt;&gt;&gt;&gt; checker from LEAN running on my FPGA.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I&#39;m in the process of spreading the DTPs from<br>
&gt;&gt;&gt;&gt; LEAN across the category/domain hierarchy.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; The current Axiom build extracts all of the functions<br>
&gt;&gt;&gt;&gt; but does not yet have the DTPs.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I have to restructure the system, including the compiler<b=
r>
&gt;&gt;&gt;&gt; and interpreter to parse and inherit the DTPs. I<br>
&gt;&gt;&gt;&gt; have some of that code but only some of the code<br>
&gt;&gt;&gt;&gt; has been pushed to the repository (volume 15) but<br>
&gt;&gt;&gt;&gt; that is rather trivial, out of date, and incomplete.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I&#39;m clearly not smart enough to prove the Risch<br>
&gt;&gt;&gt;&gt; algorithm and its associated machinery but the needed<br>
&gt;&gt;&gt;&gt; definitions and theorems will be available to someone<br>
&gt;&gt;&gt;&gt; who wants to try.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; [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>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; On 8/19/21, Tim Daly &lt;<a href=3D"mailto:axiomcas@gmail.=
com" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt; =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>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; REVIEW (Axiom on WSL2 Windows)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; So the steps to run Axiom from a Windows desktop<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 1 Windows) install XMing on Windows for X11 server<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; <a href=3D"http://www.straightrunning.com/XmingNotes/"=
 rel=3D"noreferrer" target=3D"_blank">http://www.straightrunning.com/XmingN=
otes/</a><br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 2 WSL2) Install Axiom in WSL2<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; sudo apt install axiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 3 WSL2) modify /usr/bin/axiom to fix the bug:<br>
&gt;&gt;&gt;&gt;&gt; (someone changed the axiom startup script.<br>
&gt;&gt;&gt;&gt;&gt; It won&#39;t work on WSL2. I don&#39;t know who or<br>
&gt;&gt;&gt;&gt;&gt; how to get it fixed).<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; sudo emacs /usr/bin/axiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; (split the line into 3 and add quote marks)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; export SPADDEFAULT=3D/usr/local/axiom/mnt/linux<br>
&gt;&gt;&gt;&gt;&gt; export AXIOM=3D/usr/lib/axiom-20170501<br>
&gt;&gt;&gt;&gt;&gt; export &quot;PATH=3D/usr/lib/axiom-20170501/bin:$PATH&=
quot;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 4 WSL2) create a .axiom.input file to include startup =
cmds:<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; emacs .axiom.input<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; )cd &quot;/mnt/c/yourpath&quot;<br>
&gt;&gt;&gt;&gt;&gt; )sys pwd<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 5 WSL2) create a &quot;myaxiom&quot; command that sets=
 the<br>
&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 =C2=A0DISPLAY variable and starts axiom<b=
r>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; emacs myaxiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; #! /bin/bash<br>
&gt;&gt;&gt;&gt;&gt; export DISPLAY=3D:0.0<br>
&gt;&gt;&gt;&gt;&gt; axiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 6 WSL2) put it in the /usr/bin directory<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; chmod +x myaxiom<br>
&gt;&gt;&gt;&gt;&gt; sudo cp myaxiom /usr/bin/myaxiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 7 WINDOWS) start the X11 server<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; (XMing XLaunch Icon on your desktop)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 8 WINDOWS) run myaxiom from PowerShell<br>
&gt;&gt;&gt;&gt;&gt; (this should start axiom with graphics available)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; wsl myaxiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 8 WINDOWS) make a PowerShell desktop<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; <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>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; On 8/13/21, Tim Daly &lt;<a href=3D"mailto:axiomcas@gm=
ail.com" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt; A great deal of thought is directed toward making =
the SANE version<br>
&gt;&gt;&gt;&gt;&gt;&gt; of Axiom as flexible as possible, decoupling mecha=
nism from theory.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; An interesting publication by Brian Cantwell Smith=
 [0], &quot;Reflection<br>
&gt;&gt;&gt;&gt;&gt;&gt; and Semantics in LISP&quot; seems to contain inter=
esting ideas related<br>
&gt;&gt;&gt;&gt;&gt;&gt; to our goal. Of particular interest is the ability=
 to reason about<br>
&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt; perform self-referential manipulations. In a depen=
dently-typed<br>
&gt;&gt;&gt;&gt;&gt;&gt; system it seems interesting to be able &quot;adapt=
&quot; code to handle<br>
&gt;&gt;&gt;&gt;&gt;&gt; run-time computed arguments to dependent functions=
. The abstract:<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 &quot;We show how a computational sys=
tem can be constructed to<br>
&gt;&gt;&gt;&gt;&gt;&gt; &quot;reason&quot;,<br>
&gt;&gt;&gt;&gt;&gt;&gt; effectively<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 and consequentially, about its own in=
ferential processes. The<br>
&gt;&gt;&gt;&gt;&gt;&gt; analysis proceeds in two<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 parts. First, we consider the general=
 question of computational<br>
&gt;&gt;&gt;&gt;&gt;&gt; semantics, rejecting<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 traditional approaches, and arguing t=
hat the declarative and<br>
&gt;&gt;&gt;&gt;&gt;&gt; procedural aspects of<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 computational symbols (what they stan=
d for, and what behaviour<br>
&gt;&gt;&gt;&gt;&gt;&gt; they<br>
&gt;&gt;&gt;&gt;&gt;&gt; engender) should be<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 analysed independently, in order that=
 they may be coherently<br>
&gt;&gt;&gt;&gt;&gt;&gt; related. Second, we<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 investigate self-referential behavior=
 in computational processes,<br>
&gt;&gt;&gt;&gt;&gt;&gt; and show how to embed an<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 effective procedural model of a compu=
tational calculus within that<br>
&gt;&gt;&gt;&gt;&gt;&gt; calculus (a model not<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 unlike a meta-circular interpreter, b=
ut connected to the<br>
&gt;&gt;&gt;&gt;&gt;&gt; fundamental operations of the<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 machine in such a way as to provide, =
at any point in a<br>
&gt;&gt;&gt;&gt;&gt;&gt; computation,<br>
&gt;&gt;&gt;&gt;&gt;&gt; fully articulated<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 descriptions of the state of that com=
putation, for inspection and<br>
&gt;&gt;&gt;&gt;&gt;&gt; possible modification). In<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 terms of the theories that result fro=
m these investigations, we<br>
&gt;&gt;&gt;&gt;&gt;&gt; present a general architecture<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 for procedurally reflective processes=
, able to shift smoothly<br>
&gt;&gt;&gt;&gt;&gt;&gt; between dealing with a given<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 subject domain, and dealing with thei=
r own reasoning processes<br>
&gt;&gt;&gt;&gt;&gt;&gt; over<br>
&gt;&gt;&gt;&gt;&gt;&gt; that domain.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 An instance of the general solution i=
s worked out in the context<br>
&gt;&gt;&gt;&gt;&gt;&gt; of<br>
&gt;&gt;&gt;&gt;&gt;&gt; an applicative<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 language. Specifically, we present th=
ree successive dialects of<br>
&gt;&gt;&gt;&gt;&gt;&gt; LISP: 1-LISP, a distillation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 current practice, for comparison purp=
oses; 2-LISP, a dialect<br>
&gt;&gt;&gt;&gt;&gt;&gt; constructed in terms of our<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 rationalised semantics, in which the =
concept of evaluation is<br>
&gt;&gt;&gt;&gt;&gt;&gt; rejected in favour of<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 independent notions of simplification=
 and reference, and in which<br>
&gt;&gt;&gt;&gt;&gt;&gt; the respective categories<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 of notation, structure, semantics, an=
d behaviour are strictly<br>
&gt;&gt;&gt;&gt;&gt;&gt; aligned; and 3-LISP, an<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 extension of 2-LISP endowed with refl=
ective powers.&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Axiom SANE builds dependent types on the fly. The =
ability to access<br>
&gt;&gt;&gt;&gt;&gt;&gt; both the refection<br>
&gt;&gt;&gt;&gt;&gt;&gt; of the tower of algebra and the reflection of the =
tower of proofs at<br>
&gt;&gt;&gt;&gt;&gt;&gt; the time of construction<br>
&gt;&gt;&gt;&gt;&gt;&gt; makes the construction of a new domain or specific=
 algorithm easier<br>
&gt;&gt;&gt;&gt;&gt;&gt; and more general.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; This is of particular interest because one of the =
efforts is to build<br>
&gt;&gt;&gt;&gt;&gt;&gt; &quot;all the way down to the<br>
&gt;&gt;&gt;&gt;&gt;&gt; metal&quot;. If each layer is constructed on top o=
f previous proven layers<br>
&gt;&gt;&gt;&gt;&gt;&gt; and the new layer<br>
&gt;&gt;&gt;&gt;&gt;&gt; can &quot;reach below&quot; to lower layers then t=
he tower of layers can be<br>
&gt;&gt;&gt;&gt;&gt;&gt; built without duplication.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; [0], Smith, Brian Cantwell &quot;Reflection and Se=
mantics in LISP&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt; POPL &#39;84: Proceedings of the 11th ACM SIGACT-S=
IGPLAN<br>
&gt;&gt;&gt;&gt;&gt;&gt; ymposium on Principles of programming languagesJan=
uary 1<br>
&gt;&gt;&gt;&gt;&gt;&gt; 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>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; On 6/29/21, Tim Daly &lt;<a href=3D"mailto:axiomca=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Having spent time playing with hardware it is =
perfectly clear that<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; future computational mathematics efforts need =
to adapt to using<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; parallel processing.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; I&#39;ve spent a fair bit of time thinking abo=
ut structuring Axiom to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; be parallel. Most past efforts have tried to f=
ocus on making a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; particular algorithm parallel, such as a matri=
x multiply.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; But I think that it might be more effective to=
 make each domain<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; run in parallel. A computation crosses multipl=
e domains so a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; particular computation could involve multiple =
parallel copies.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; For example, computing the Cylindrical Algebra=
ic Decomposition<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; could recursively decompose the plane. Indeed,=
 any tree-recursive<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; algorithm could be run in parallel &quot;in th=
e large&quot; by creating new<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; running copies of the domain for each sub-prob=
lem.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So the question becomes, how does one manage t=
his?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; A similar problem occurs in robotics where one=
 could have multiple<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; wheels, arms, propellers, etc. that need to ac=
t independently but<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; in coordination.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; The robot solution uses ROS2. The three ideas =
are ROSCORE,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; TOPICS with publish/subscribe, and SERVICES wi=
th request/response.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; These are communication paths defined between =
processes.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; ROS2 has a &quot;roscore&quot; which is basica=
lly a phonebook of &quot;topics&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can create or look up the current =
active topics. eq:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 rosnode list<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; TOPICS:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can PUBLISH a topic (which is basi=
cally a typed data<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure), e.g the topic /hw with the String =
data &quot;Hello World&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; eg:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 rostopic pub /hw std_msgs/String =
&quot;Hello, World&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can SUBSCRIBE to a topic, such as =
/hw, and get a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; copy of the data.=C2=A0 eg:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 rostopic echo /hw=C2=A0 =C2=A0=3D=
=3D&gt; &quot;Hello, World&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Publishers talk, subscribers listen.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; SERVICES:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can make a REQUEST of a SERVICE an=
d get a RESPONSE.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; This is basically a remote function call.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom in parallel?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So domains could run, each in its own process.=
 It could provide<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; services, one for each function. Any other pro=
cess could request<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; a computation and get the result as a response=
. Domains could<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; request services from other domains, either wa=
iting for responses<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; or continuing while the response is being comp=
uted.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; The output could be sent anywhere, to a termin=
al, to a browser,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; to a network, or to another process using the =
publish/subscribe<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; protocol, potentially all at the same time sin=
ce there can be many<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; subscribers to a topic.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Available domains could be dynamically added b=
y announcing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; themselves as new &quot;topics&quot; and could=
 be dynamically looked-up<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; at runtime.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; This structure allows function-level / domain-=
level parallelism.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is very effective in the robot world and I =
think it might be a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; good structuring mechanism to allow computatio=
nal mathematics<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; to take advantage of multiple processors in a =
disciplined fashion.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom has a thousand domains and each could ru=
n on its own core.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; In addition. notice that each domain is indepe=
ndent of the others.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So if we want to use BLAS Fortran code, it cou=
ld just be another<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; service node. In fact, any &quot;foreign funct=
ion&quot; could transparently<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; cooperate in a distributed Axiom.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Another key feature is that proofs can be &quo=
t;by node&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 6/5/21, Tim Daly &lt;<a href=3D"mailto:axio=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom is based on first-class dependent ty=
pes. Deciding when<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; two types are equivalent may involve compu=
tation. See<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Christiansen, David Thrane &quot;Checking =
Dependent Types with<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Normalization by Evaluation&quot; (2019)<b=
r>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This puts an interesting constraint on bui=
lding types. The<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; constructed types has to export a function=
 to decide if a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; given type is &quot;equivalent&quot; to it=
self.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The notion of &quot;equivalence&quot; migh=
t involve category ideas<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of natural transformation and univalence. =
Sigh.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; That&#39;s an interesting design point.<br=
>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 5/5/21, Tim Daly &lt;<a href=3D"mailto:=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is interesting that programmer&#39;=
s eyes and expectations adapt<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to the tools they use. For instance, I=
 use emacs and expect to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; work directly in files and multiple bu=
ffers. When I try to use one<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the many IDE tools I find they tend=
 to &quot;get in the way&quot;. I<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; already<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; know or can quickly find whatever they=
 try to tell me. If you use<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; IDE you probably find emacs &quot;too =
sparse&quot; for programming.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Recently I&#39;ve been working in a sp=
arse programming environment.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I&#39;m exploring the question of runn=
ing a proof checker in an FPGA.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The FPGA development tools are painful=
 at best and not intuitive<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; since you SEEM to be programming but y=
ou&#39;re actually describing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; hardware gates, connections, and timin=
g. This is an environment<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; where everything happens all-at-once a=
nd all-the-time (like the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; circuits in your computer). It is the =
&quot;assembly language of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; circuits&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Naturally, my eyes have adapted to thi=
s rather raw level.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; That said, I&#39;m normally doing lite=
rate programming all the time.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; My typical file is a document which is=
 a mixture of latex and<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; lisp.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is something of a shock to return t=
o that world. It is clear<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; why<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; people who program in Python find lisp=
 to be a &quot;sea of parens&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Yet as a lisp programmer, I don&#39;t =
even see the parens, just code.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It takes a few minutes in a literate d=
ocument to adapt vision to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; see the latex / lisp combination as na=
tural. The latex markup,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; like the lisp parens, eventually just =
disappears. What remains<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; is just lisp and natural language text=
.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This seems painful at first but eyes q=
uickly adapt. The upside<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; is that there is always a &quot;finish=
ed&quot; document that describes the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; state of the code. The overhead of wri=
ting a paragraph to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; describe a new function or change a pa=
ragraph to describe the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; changed function is very small.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Using a Makefile I latex the document =
to generate a current PDF<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and then I extract, load, and execute =
the code. This loop catches<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; errors in both the latex and the sourc=
e code. Keeping an open file<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; my pdf viewer shows all of the changes=
 in the document after every<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; run of make. That way I can edit the b=
ook as easily as the code.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Ultimately I find that writing the boo=
k while writing the code is<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; more productive. I don&#39;t have to r=
emember why I wrote something<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; since the explanation is already there=
.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; We all have our own way of programming=
 and our own tools.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; But I find literate programming to be =
a real advance over IDE<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; style programming and &quot;raw code&q=
uot; programming.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 2/27/21, Tim Daly &lt;<a href=3D"ma=
ilto:[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote=
:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The systems I use have the interes=
ting property of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;Living within the compiler&q=
uot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Lisp, Forth, Emacs, and other syst=
ems that present themselves<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; through the Read-Eval-Print-Loop (=
REPL) allow the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ability to deeply interact with th=
e system, shaping it to your<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; need.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; My current thread of study is soft=
ware architecture. See<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"https://www.youtube.com=
/watch?v=3DW2hagw1VhhI&amp;feature=3Dyoutu.be" rel=3D"noreferrer" target=3D=
"_blank">https://www.youtube.com/watch?v=3DW2hagw1VhhI&amp;feature=3Dyoutu.=
be</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and <a href=3D"https://www.georgef=
airbanks.com/videos/" rel=3D"noreferrer" target=3D"_blank">https://www.geor=
gefairbanks.com/videos/</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; My current thinking on SANE involv=
es the ability to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; dynamically define categories, rep=
resentations, and functions<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; along with &quot;composition funct=
ions&quot; that permits choosing a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; combination at the time of use.<br=
>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; You might want a domain for handli=
ng polynomials. There are<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a lot of choices, depending on you=
r use case. You might want<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; different representations. For exa=
mple, you might want dense,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; sparse, recursive, or &quot;machin=
e compatible fixnums&quot; (e.g. to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; interface with C code). If these d=
on&#39;t exist it ought to be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; possible<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to create them. Such &quot;lego-li=
ke&quot; building blocks require careful<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; thought about creating &quot;fully=
 factored&quot; objects.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Given that goal, the traditional b=
arrier of &quot;compiler&quot; vs<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;interpreter&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; does not seem useful. It is better=
 to &quot;live within the compiler&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; which<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; gives the ability to define new th=
ings &quot;on the fly&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Of course, the SANE compiler is go=
ing to want an associated<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; proof of the functions you create =
along with the other parts<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; such as its category hierarchy and=
 representation properties.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; There is no such thing as a simple=
 job. :-)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 2/18/21, Tim Daly &lt;<a href=
=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt;=
 wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The Axiom SANE compiler / inte=
rpreter has a few design points.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; 1) It needs to mix interpreted=
 and compiled code in the same<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; function.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; SANE allows dynamic constructi=
on of code as well as dynamic type<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; construction at runtime. Both =
of these can occur in a runtime<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; object.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; So there is potentially a mixt=
ure of interpreted and compiled<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; code.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; 2) It needs to perform type re=
solution at compile time without<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; overhead<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; where possible. Since this is =
not always possible there needs to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a &quot;prefix thunk&quot; tha=
t will perform the resolution. Trivially,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; for<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; example,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; if we have a + function we nee=
d to type-resolve the arguments.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; However, if we can prove at co=
mpile time that the types are both<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; bounded-NNI and the result is =
bounded-NNI (i.e. fixnum in lisp)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; then we can inline a call to +=
 at runtime. If not, we might have<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; + applied to NNI and POLY(FLOA=
T), which requires a thunk to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; resolve types. The thunk could=
 even &quot;specialize and compile&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the code before executing it.<=
br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It turns out that the Forth im=
plementation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;threaded-interpreted&quo=
t;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; languages model provides an ef=
ficient and effective way to do<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; this.[0]<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Type resolution can be &quot;i=
nserted&quot; in intermediate thunks.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The model also supports dynami=
c overloading and tail recursion.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Combining high-level CLOS code=
 with low-level threading gives an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; easy to understand and robust =
design.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; [0] Loeliger, R.G. &quot;Threa=
ded Interpretive Languages&quot; (1981)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ISBN 0-07-038360-X<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 2/5/21, Tim Daly &lt;<a hre=
f=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt=
; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I&#39;ve worked hard to ma=
ke Axiom depend on almost no other<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; tools so that it would not=
 get caught by &quot;code rot&quot; of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; libraries.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; However, I&#39;m also tryi=
ng to make the new SANE version much<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; easier to understand and d=
ebug.To that end I&#39;ve been<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; experimenting<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; with some ideas.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It should be possible to v=
iew source code, of course. But the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; source<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; code is not the only, nor =
possibly the best, representation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ideas.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In particular, source code=
 gets compiled into data structures.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; these data structures real=
ly are a graph of related structures.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; For example, looking at th=
e gcd function from NNI, there is the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; representation of the gcd =
function itself. But there is also a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; that is the REP (and, in t=
he new system, is separate from the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; domain).<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Further, there are associa=
ted specification and proof<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structures.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Even<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; further, the domain inheri=
ts the category structures, and from<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; those<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; it<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; inherits logical axioms an=
d definitions through the proof<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Clearly the gcd function i=
s a node in a much larger graph<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; When trying to decide why =
code won&#39;t compile it would be useful<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; be able to see and walk th=
ese structures. I&#39;ve thought about<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; using<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; browser but browsers are t=
oo weak. Either everything has to be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; single tab to show the gra=
ph&quot; or &quot;the nodes of the graph are in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; different<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; tabs&quot;. Plus, construc=
ting dynamic graphs that change as the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; software<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; changes (e.g. by loading a=
 new spad file or creating a new<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; function)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; represents the huge proble=
m of keeping the browser &quot;in sync<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; with<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom workspace&quot;. So =
something more dynamic and embedded is<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; needed.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom source gets compiled=
 into CLOS data structures. Each of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; these<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; new SANE structures has an=
 associated surface representation,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; so<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; they<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; can be presented in user-f=
riendly form.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Also, since Axiom is liter=
ate software, it should be possible<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; look<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; at<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the code in its literate f=
orm with the surrounding explanation.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Essentially we&#39;d like =
to have the ability to &quot;deep dive&quot; into<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; workspace, not only for de=
bugging, but also for understanding<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; what<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; functions are used, where =
they come from, what they inherit,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; how they are used in a com=
putation.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; To that end I&#39;m lookin=
g at using McClim, a lisp windowing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; system.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Since the McClim windows w=
ould be part of the lisp image, they<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; have<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; access to display (and mod=
ify) the Axiom workspace at all<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; times.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The only hesitation is tha=
t McClim uses quicklisp and drags in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; lot<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of other subsystems. It&#3=
9;s all lisp, of course.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; These ideas aren&#39;t new=
. They were available on Symbolics<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; machines,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a truly productive platfor=
m and one I sorely miss.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 1/19/21, Tim Daly &lt;<=
a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]</=
a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Also of interest is th=
e talk<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;The Unreasonable=
 Effectiveness of Dynamic Typing for<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Practical<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Programs&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"https://vim=
eo.com/74354480" rel=3D"noreferrer" target=3D"_blank">https://vimeo.com/743=
54480</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; which questions whethe=
r static typing really has any benefit.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 1/19/21, Tim Daly &=
lt;<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]=
om</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Peter Naur wrote a=
n article of interest:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <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>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In particular, it =
mirrors my notion that Axiom needs<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to embrace literat=
e programming so that the &quot;theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the problem&quo=
t; is presented as well as the &quot;theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the solution&qu=
ot;. I quote the introduction:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This article is, t=
o my mind, the most accurate account<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of what goes on in=
 designing and coding a program.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I refer to it regu=
larly when discussing how much<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; documentation to c=
reate, how to pass along tacit<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; knowledge, and the=
 value of the XP&#39;s metaphor-setting<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; exercise. It also =
provides a way to examine a methodolgy&#39;s<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; economic structure=
.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In the article, wh=
ich follows, note that the quality of the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; designing programm=
er&#39;s work is related to the quality of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the match between =
his theory of the problem and his theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the solution. N=
ote that the quality of a later<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; programmer&#39;s<b=
r>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; work is related to=
 the match between his theories and the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; previous programme=
r&#39;s theories.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Using Naur&#39;s i=
deas, the designer&#39;s job is not to pass along<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;the design&q=
uot; but to pass along &quot;the theories&quot; driving the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; design.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The latter goal is=
 more useful and more appropriate. It also<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; highlights that kn=
owledge of the theory is tacit in the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; owning,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; so passing along t=
he thoery requires passing along both<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; explicit<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and tacit knowledg=
e.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>

--00000000000091c88405dadc582b--