The=
weaver program can now process a latex document.

The end result =
is a tree structure of the same document.The parser needs to know the 'arity' o=
f tags since \tag{a}{b}

would parse one way, \tag{a}, for a 1-arity tag= and another

would parse one way, \tag{a}, for a 1-arity tag= and another

way \tag{a}{b} for a 2-arity tag. The code need=
s to be generalized

to parse given the arity.

=

The weaver program is structured so that the tree-parse outputas input and produce valid Axiom inputforms. This should make

On Sat, Aug 27, 2016 at 1:28 PM, Tim Daly <axiomcas@gmai=
l.com> wrote:

--001a1140591ab3d54f053b714d3f--
From MAILER-DAEMON Thu Sep 08 04:59:12 2016
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1bhvAu-0004Bv-NG
for mharc-axiom-developer@gnu.org; Thu, 08 Sep 2016 04:59:12 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:44970)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from On Sat, Aug 27, 2016 at 12:14 PM, Richard Fateman <fateman@berk= eley.edu> wrote:=20 =20 =20

Take up a book on complex analysis and see what problems you have

=C2=A0as you try to encode the statements, or especially the homework=

problems. I tried this decades ago with the text I used,

https://www.amazon.com/Functions-Complex-Variable-Technique- Mathematics/dp/0898715954

but probably any other text would do. My last project at CMU (Tires) involved work on mac= hine learning

using natural language (and Good-Old-Fashioned-AI (GOFAI)= ).I'm not smart enough to make progress in natural lang= uage.

=C2=A0

I think the emphasis on handbook or reference book representation

is natural, and I have certainly pursued this direction myself.=C2=A0 However

what you/we want to be able to encode is mathematical discourse. This

goes beyond "has the algorithm reproduced the reference value fo= r an

integration."=C2=A0=C2=A0 Can you encode in semantic latex a des= cription of the geometry

of the (perhaps infinitely layered) contour of a complex function?=C2=A0 You

might wonder if this is important, but then note that questions of this sort

appear in the problem section for chapter 1.Like any research project, there has to be = bounds on the ambition.At this point, the goal is to mod= ify the markup to disambiguate a latexformula so the machine= can import it. Axiom needs to import it to create

a test suite measuri= ng progress against existing knowledge.What y= ou're describing seems to be a way to encode topological issuesdealing with the structure of the space underlying the formulas. I h= ave noidea how to encode the Bloch sphere or a torus or any = other space exceptby referencing an Axiom domain, which impl= icitly encodes it.If the formula deals with q= uantum mechanics then the algorithms have animplicit, mechan= istic way of dealing with the Bloch sphere. So markup thatus= es these function calls use this implicit grounding. Simllarly, markup that=uses a branch cut implicitly uses the implementation semanti= cs.Axiom and Mathematics have one set of branch cuts, Ma= ple and Maximahave another (at far as I can tell). So the ma= rkup decisions have to becarefully chosen.=C2=A0

Here's the challenge then.=C2=A0 Take a mathematics book and &quo= t;encode"

=C2=A0it so that a program (hypothetically) could answer the problems at

the end of each chapter.<= /span>That's a much deeper can of worms than it appears. I spent a= lot oftime in the question-answering literature. I have no = idea how to makeprogress in that area. The Tires project inv= olved self-modifying lispbased on natural language interacti= on with a human in the limiteddomain of changing a car tire= . See(The grant ended before the projected ended. Sigh)TimP.S. Tires i= s self-modifying lisp code. It "learns" by changing itself.The initial code (the seed code) becomes &qu= ot;something else". Oneinteresti= ng insight is that two versions of the seed code will divergebased on "experience". That implies that y= ou can't "teach by copy",that is, you can't teach one system and then "just copy" it = to anotherexisting system since their = experiences (and the code structure)wi= ll differ. Any system that "learns" will fail "teach by copy= ", I believe.That means that AI w= ill not have the exponential growth that everyoneseems to believe.

But the MOST significant contribution by 20th-Ce=
ntury human
mathematicians and computer scientists
was the creation of COMPUTER ALGEBRA. It is
still in a very preliminary stage, but is already revolutionizing
the way we DO and THINK about mathematics. Even computer foes
often `cheat' and use Maple or Mathematica on the side.=20
It is a scandal that, so far, the pioneers of computer algebra
did not get their due recognition by the mathematical establishment.
One glaring oversight, reminiscent of G=C3=B6del only becoming
a professor at the age of 47, is that Bruno BUCHBERGER,
the great pioneer of computer algebra, whose algorithm revolutionized
all the spectrum of mathematics, from robotics to very abstract
algebraic geometry, does not get a tiny fraction of the recognition
granted to the Atiyahs and the Botts.
He is not even a member of the Academy of Science of
his native Austria!
But one should not fault
this or that specific Academy. After all, at least today,
national academies consist of=20
members of that narrow-minded, short-sighted species
called humans.=20
Bruno Buchberger's heritage, and his Gr=C3=B6bner Bases
will survive long after most of
the current members of the
Austrian Academy of Science will be forgotten.

-- quote from D=
oron Zeilberger (http://www.math.rutgers.edu/~zeilberg/Opinion47.html)Tim

Axiom now has the =
necessary machinery to process proofs

at build time (ACL2 for=
Lisp, COQ for Spad). While pondering

the subject I ended up =
reading "The Semantics of Destructive

Lisp"[0]. The=
re is an interesting quote from Scherlis and Scott[1]

which l=
eads me to think there is a crossover from Collin's work

=
on Cylindrical Algebraic Decomposition.[2]

The first tho=
ught involves the difference between a verification

proof and=
a derivation proof. Verification involves proving an

algorit=
hm that already exists. Derivation involves transformations

f=
rom an initial set to a final result. Both proofs work but [2] says

=

=

=C2=A0 "The traditional correctness proof -- that a program=
is consistent

=C2=A0 with its specifications -- does not co=
nstitute a derivation of the

=C2=A0 program. Conventional pro=
ofs, as currently presented in the

=C2=A0 literature, do lit=
tle to justify the structure of the program being

=C2=A0 pro=
ved, and they do even less to aid in the development of new

=
=C2=A0 programs that may be similar to the program that was proved. That

=C2=A0 is, they neither explicate existing programs nor aid in =
their

=C2=A0 modification and adaptation.

=C2=A0 modification and adaptation.

=C2=A0 We i=
ntend that program derivations serve as conceptual or idealized

=C2=A0 can be considered an idealized record of the se=
quence of design

=C2=A0 decisions that led to a particular re=
alization of a specification.

=C2=A0 Stripped down to ess=
entials, our claim is that the programs of the

=C2=A0 future =
will in fact be descriptions of program derivations. Documentation

be derived from the specification (e.g. LAPACK programs) that

<=
div>guarantee behavior?=C2=A0 methods based on stepwise-refinement methodologies are already=

=C2=A0 strong evidence that there is movement toward this a=
pproach. These

=C2=A0 documentation methods also provide supp=
ort for the hypothesis that

=C2=A0 program derivations offer =
a more intuitive and revealing way to explain

=C2=A0 programs=
than do conventional proofs of correctness. The proofs may

=
=C2=A0 succeed in convincing the reader of the correctness of the algorithm=

=C2=A0 without giving him any hint of why the algorithm work=
s or how it came

=C2=A0 about. On the other hand, a derivatio=
n may be thought of as an

=C2=A0 especially well-structured =
constructive proof of correctness of the

=C2=A0 algorithm, ta=
king the reader step by step from an inital abstract

=C2=A0 a=
lgorithm he accepts as meeting the specifications of the problem to

Matrices can be viewed as polynomials. Can numeric algorithms

=C2=A0 a highly connected and efficient implementation of it."<=
br>

For mathematical algorithms, Mason [0] points out that it=
is possible to

mechanically specialize an algorithm for a g=
iven case, often with an

order of magnitude of efficiency. Th=
is is very appealing, especially in

numeric domains where it =
can be proven that things cannot overflow.

Collins works =
in semialgebraic sets, basically polynomials with a few

compa=
rison limits and parameters. CAD could be "bent" to use it as

=

=

a compile step so that a CAD result would generate a program. No=
t

only would this give a complete specification, it would pro=
vide a solid

theoretical basis for the code. Can this be exte=
nded to derive other

algorithms?

Much more reading to do...

Tim

<= /div>[2] Collins, George E. "Quantifier elimination for the elementary=

33:134-183 (1975)