From MAILER-DAEMON Sat Jul 04 11:13:27 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZBP8B-0004nx-3g
for mharc-axiom-developer@gnu.org; Sat, 04 Jul 2015 11:13:27 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:41323)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZBP87-0004mZ-Ns
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 11:13:24 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZBP84-0002kv-Gh
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 11:13:23 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:51277
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZBP84-0002iE-Bh
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 11:13:20 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t64FDIFI019725;
Sat, 4 Jul 2015 10:13:18 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t64FDINA019722;
Sat, 4 Jul 2015 10:13:18 -0500
Date: Sat, 4 Jul 2015 10:13:18 -0500
Message-Id: <201507041513.t64FDINA019722@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Directions
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 04 Jul 2015 15:13:25 -0000
I've been spending a lot of time working on Field Programmable Gate
Arrays (FPGAs) which is basically hardware that can be reprogrammed.
There have been some interesting developments in this area.
First, FPGAs are a lot more powerful and much cheaper.
Second, Intel just bought the second largest FPGA company, Altera.
http://www.cnbc.com/id/102723697
Third, FPGAs are moving toward computational mathematics.
https://github.com/Gladdy/numerical-fpga-thesis
I believe, though I don't know for sure, that Intel will eventually
put an FPGA fabric on the same chip (Sytem on a Chip, SoC) as their
CPUs.
Axiom is in a unique position to exploit this kind of hardware merger.
If anyone has pointers to work on hardware-based symbolic/numeric
work, please send me a link.
Tim
From MAILER-DAEMON Sat Jul 04 11:46:24 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZBPe4-0007wA-4i
for mharc-axiom-developer@gnu.org; Sat, 04 Jul 2015 11:46:24 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:50177)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZBPe0-0007vN-Ty
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 11:46:22 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZBPdw-0006ne-JA
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 11:46:20 -0400
Received: from cgate.sci.ccny.cuny.edu ([134.74.34.100]:62553)
by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZBPdw-0006ln-FP
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 11:46:16 -0400
Received: from [108.30.208.33] (account wyscc@sci.ccny.cuny.edu)
by cgate.sci.ccny.cuny.edu (CommuniGate Pro WebUser 4.2.10)
with HTTP id 32804039; Sat, 04 Jul 2015 11:33:58 -0400
From: "William Sit"
To: daly@axiom-developer.org,axiom-developer@nongnu.org
X-Mailer: CommuniGate Pro WebUser Interface v.4.2.10
Date: Sat, 04 Jul 2015 11:33:58 -0400
Message-ID:
In-Reply-To: <201507041513.t64FDINA019722@axiom-developer.org>
References: <201507041513.t64FDINA019722@axiom-developer.org>
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"; format="flowed"
Content-Transfer-Encoding: 8bit
X-detected-operating-system: by eggs.gnu.org: Solaris 10
X-Received-From: 134.74.34.100
Subject: Re: [Axiom-developer] Directions
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 04 Jul 2015 15:46:22 -0000
Dear Tim:
I don't have pointers applying FPGA techniques to symbolic
computations. However, the trend is to use something
similar to FPGA all the way down to the manufacture level.
For some background, see
http://www.rambus.com/technology/item/979-rambus-cryptography-research-division-unveils-cryptomanager-secure-feature-management-platform.
Qualcomm, for example already licenses this technology, as
do many other companies. Their idea is to tailor each
individual chip at the single consumer level to enhance
security.
By the way, the link
https://github.com/Gladdy/numerical-fpga-thesis/blob/master/thesis/thesis.pdf
is not readable by Adobe or Preview on Macs.
However, according to your link (scroll down to bottom),
the abstract mentions:
" This thesis describes the process of implementing an
accelerator in which the computational part is specified
using the functional hardware description language CÎ»aSH
and discusses the feasibility of performing numerical
mathematics on this accelerator by computing
approximations to ordinary differential equations. The
accelerator is capable of using the methods of Euler and
Runge-Kutta (second order) to perform the approximations,
but due to the use of a fixed-point number representation
the accuracy suffers."
So this is mainly a numerical set up. Graphics processors
have been used for numerical scientific work for a long
time already since GPUs have improved tremendously in
power (my layman observation is the advance is faster than
CPUs in terms of number of cores, speed, and low power
consumption).
Since Axiom is software, I am not sure how the technique
may be applied, unless you are thinking about an Axiom
chip, or some hybrid numerical-symbolic approach is used.
However, Axiom is a relatively small system (compared to
modern mammoth bloated software), and I think the priority
should be to make Axiom's learning curve less steep than
make Axiom run faster, or even more securely.
William
On Sat, 4 Jul 2015 10:13:18 -0500
daly@axiom-developer.org wrote:
> I've been spending a lot of time working on Field
>Programmable Gate
> Arrays (FPGAs) which is basically hardware that can be
>reprogrammed.
>
> There have been some interesting developments in this
>area.
>
>First, FPGAs are a lot more powerful and much cheaper.
>
> Second, Intel just bought the second largest FPGA
>company, Altera.
> http://www.cnbc.com/id/102723697
>
> Third, FPGAs are moving toward computational
>mathematics.
> https://github.com/Gladdy/numerical-fpga-thesis
>
> I believe, though I don't know for sure, that Intel will
>eventually
> put an FPGA fabric on the same chip (Sytem on a Chip,
>SoC) as their
> CPUs.
>
> Axiom is in a unique position to exploit this kind of
>hardware merger.
> If anyone has pointers to work on hardware-based
>symbolic/numeric
> work, please send me a link.
>
> Tim
>
>
>
> _______________________________________________
> Axiom-developer mailing list
> Axiom-developer@nongnu.org
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
William Sit, Professor Emeritus
Mathematics, City College of New York
Office: R6/291D Tel: 212-650-5179
Home Page: http://scisun.sci.ccny.cuny.edu/~wyscc/
From MAILER-DAEMON Sat Jul 04 12:47:08 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZBQaq-0000RT-NW
for mharc-axiom-developer@gnu.org; Sat, 04 Jul 2015 12:47:08 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:33691)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZBQao-0000PO-32
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 12:47:07 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZBQak-0003IC-Rk
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 12:47:06 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:50940
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZBQak-0003I8-MT
for axiom-developer@nongnu.org; Sat, 04 Jul 2015 12:47:02 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t64Gl1FI020678;
Sat, 4 Jul 2015 11:47:01 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t64Gl1Ar020675;
Sat, 4 Jul 2015 11:47:01 -0500
Date: Sat, 4 Jul 2015 11:47:01 -0500
Message-Id: <201507041647.t64Gl1Ar020675@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: Re: [Axiom-developer] directions
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 04 Jul 2015 16:47:07 -0000
>I don't have pointers applying FPGA techniques to symbolic
>computations. However, the trend is to use something
>similar to FPGA all the way down to the manufacture level.
>For some background, see
>http://www.rambus.com/technology/item/979-rambus-cryptography-research-division-unveils-cryptomanager-secure-feature-management-platform.
>Qualcomm, for example already licenses this technology, as
>do many other companies. Their idea is to tailor each
>individual chip at the single consumer level to enhance
>security.
I'm actually working with FPGAs to do hardware security with some
people at CMU.
>By the way, the link
>https://github.com/Gladdy/numerical-fpga-thesis/blob/master/thesis/thesis.pdf
>is not readable by Adobe or Preview on Macs.
I cloned the repo and can read the thesis.pdf file.
>So this is mainly a numerical set up. Graphics processors
>have been used for numerical scientific work for a long
>time already since GPUs have improved tremendously in
>power (my layman observation is the advance is faster than
>CPUs in terms of number of cores, speed, and low power
>consumption).
>Since Axiom is software, I am not sure how the technique
>may be applied, unless you are thinking about an Axiom
>chip, or some hybrid numerical-symbolic approach is used.
>However, Axiom is a relatively small system (compared to
>modern mammoth bloated software),
The speculation is that Intel will merge the Altera FPGA fabric
into the CPU. This already exists on my FGPA board (dual hardware
CPUs, dual firmware CPUs, and a large FPGA fabric in one chip).
Think of this as a "programmable ALU" where you can temporarily
(or permanently) run an ALU to do computational mathematics. At
the moment this undergrad thesis shows that one can do a lot of
ODE (exponential, simple harmonic, cosine hyperbolic, simple
forcd harmonic) numerical computation.
The extrapolation would be to do a symbolic computation, compile
the result to the "FPGA ALU", and do blindingly fast evaluations.
I'm already pushing forward on the BLAS work (bookvol10.5).
Given a programmable "FPGA ALU", this could really change the game.
> and I think the priority
>should be to make Axiom's learning curve less steep than
>make Axiom run faster, or even more securely.
I'm still pushing forward on "making the learning curve less steep".
I have been collecting permissions from authors to use their work as
part of the books, the most recent being work on Clifford Algebra.
I'm trying to collect permissions for each of the domains. These will
be used to introduce domains in a book-like readable treatment of the
Spad code so people can understand the algorithms while reading the
code. I have material to write, a document structure that will
organize it, and the permission to use it. It just takes time.
I'm also pulling yet more of the code into the books, eliminating dead
code, providing signatures for the lisp code, organizing the code into
chapters and sections, documenting the data structures, developing
help, )display examples, and input files for domains, and working on
both an enlarged computer algebra test suite and program proof
technology. It just takes time.
The incremental changes are hard to spot until there is a major
completion point. These have happened (e.g. replace noweb with
straight latex, remove boot and aldor, continuous integration with
docker, restructure the algebra, a new browser front end, additional
algebra, merged lisp code, enlarged test suite, etc.) It just takes time.
Eventually Axiom will be a system can be maintained, modified,
extended, and taught by people who are not the original authors
or one of the three gurus. It just takes time.
Fortunately Axiom has a 30 year horizon.
Tim
From MAILER-DAEMON Tue Jul 07 21:17:23 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZCdzH-00038P-Fs
for mharc-axiom-developer@gnu.org; Tue, 07 Jul 2015 21:17:23 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:49728)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZCdzF-00038G-9r
for axiom-developer@nongnu.org; Tue, 07 Jul 2015 21:17:22 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZCdzC-0002Nb-1z
for axiom-developer@nongnu.org; Tue, 07 Jul 2015 21:17:21 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:54980
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZCdzB-0002NR-Sn
for axiom-developer@nongnu.org; Tue, 07 Jul 2015 21:17:17 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t681HGFI011007;
Tue, 7 Jul 2015 20:17:16 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t681HFuC011004;
Tue, 7 Jul 2015 20:17:15 -0500
Date: Tue, 7 Jul 2015 20:17:15 -0500
Message-Id: <201507080117.t681HFuC011004@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] How to prove large software projects correct
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Wed, 08 Jul 2015 01:17:22 -0000
One long term Axiom goal is proving Axiom implementation of algorithms
correct. After all, this is computational MATHEMATICS. The state of the
art involves writing code but ignores the formal aspects. This is not
acceptable for the long term. When Axiom gives an answer there needs to
be some assurance that the answer is formally correct.
I'm climbing the learning curve for program proofs, trying to find
a good way to handle something as complex as Axiom. There are three
interlocking approaches, one for the algebra, one for the lisp code,
and one for the machine level code.
At the moment I'm spending most of my time at the lisp level. I've
created a \sig macro so that the function signatures can be written
out in haskell-like syntax.
Gabriel Gonzalez gave an interesting talk, bridging the gap between
programming and equational reasoning for program proofs.
How to prove large software projects correct
http://www.techcast.com/events/bigtechday8/maffei-1450/?q=maffei-1450
Using this approach requires some bottom-up construction of monoid
behavior. I've marked "primitive" functions, that is, functions which
are implemented using only common lisp function calls. These will be
the early functions with signature maps. Once the signatures exist the
code need to be refactored to have equational semantics. Once that is
done each use has to be examined and refactored, recursively.
This gives hope that we can create some equational proofs. This
becomes more interesting when we look at lisp primitives used by the
algebra. Refactoring the algebra's use of lisp into a single package
would give Axiom-level semantics with proven code. Equational
semantics for lisp-based algebra primitives will fit well in COQ, the
tool that seems most likely to handle the algebra level.
It looks like the pieces are slowly falling into place.
SO much more to learn though...
Tim
From MAILER-DAEMON Fri Jul 10 16:07:48 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZDeaK-0007K0-Gx
for mharc-axiom-developer@gnu.org; Fri, 10 Jul 2015 16:07:48 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:54450)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDeaH-0007JT-Ct
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 16:07:46 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZDeaC-0000bj-BZ
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 16:07:45 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:49002
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDeaC-0000bZ-6m
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 16:07:40 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6AK7cFI017754;
Fri, 10 Jul 2015 15:07:38 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6AK7bgE017751;
Fri, 10 Jul 2015 15:07:37 -0500
Date: Fri, 10 Jul 2015 15:07:37 -0500
Message-Id: <201507102007.t6AK7bgE017751@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Literate programming
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Fri, 10 Jul 2015 20:07:47 -0000
This quote by Bill Thurston[1] makes it clear why we need to document
the algorithms in Axiom (emphasis mine):
Mathematical understanding does not expand in a monotone direction.
Our understanding frequently deteriorates as well. There are several
obvious mechanisms of decay. THE EXPERTS IN A SUBJECT RETIRE AND DIE,
OR SIMPLY MOVE ON TO OTHER SUBJECTS AND FORGET. Mathematics is
commonly explained and recorded in symbolic and concrete forms that
are easy to communicate, rather than in conceptual forms that are easy
to understand once communicated. Translation in the direction
conceptual -> concrete and symbolic is much easier than translation in
the reverse direction, and symbolic forms often replaces the
conceptual forms of understanding. And mathematical conventions and
taken-for-granted knowledge change, so older texts may become hard to
understand. In short, mathematics only exists in a living community of
mathematicians that spreads understanding and breaths life into ideas
both old and new.
The people who wrote the vast bulk of Axiom's algorithms have either
retired or died. They no longer maintain the code. We really must
collect the papers and document the algorithms. This is especially
critical going forward as open source projects tend to fall out of
interest when real life makes it inconvenient to maintain code.
Tim
[1] http://blog.computationalcomplexity.org/2015/07/will-our-understanding-of-math.html
From MAILER-DAEMON Fri Jul 10 19:29:57 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZDhjx-0003Qt-LM
for mharc-axiom-developer@gnu.org; Fri, 10 Jul 2015 19:29:57 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:32943)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDhjv-0003PO-4E
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 19:29:56 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZDhjr-0006bV-Uf
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 19:29:55 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:59121
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDhjr-0006bP-Px
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 19:29:51 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6ANToFI019218;
Fri, 10 Jul 2015 18:29:50 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6ANTojx019215;
Fri, 10 Jul 2015 18:29:50 -0500
Date: Fri, 10 Jul 2015 18:29:50 -0500
Message-Id: <201507102329.t6ANTojx019215@axiom-developer.org>
To: axiom-developer@nongnu.org, "William Sit"
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: Re: [Axiom-developer] Literate programming
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Fri, 10 Jul 2015 23:29:56 -0000
William,
Back in the day I struggled to cross the great chasm, moving from
real programming to "structured programming", i.e. not using GOTOs.
Dijkstra was asking me to change a fundamental part of my thinking,
to throw away the focus on the machine's BRANCH instruction, albeit
in my high-level FORTRAN programs. I was going to lose my precious
computed GOTOs. Even my Lisp programs had gotos. I was writing
assembler "at a higher level", being efficient; saving time; using
"best practices".
I crossed that chasm by forcing myself read what Dijkstra wrote and
forcing myself to write in the new sytle. It was painful, pointless,
and unnatural but eventually I understood. The GOTO statement,
especially my precious computed-goto, made programs hard to understand,
maintain, and modify. I haven't written a GOTO statement in years.
Literate programming is painful, pointless, and unnatural. We're being
efficient; saving time; using "best practices"! Hierarchies of tiny
files built with MAKE and without annoying comments are best practices!
If you want to understand the theory just read the code! Understanding,
maintaining, and modifying raw code is for real programmers. If you
can't do that... go away.
Knuth is trying to take away my precious hacker badge. He wants me to
write natural language to communicate ideas to other humans. What a
worthless waste of my time.
There is no argument I can make that will convince anyone that
literate programming is worthwhile. Like lisp programming, literate
programming is an "Aha!" epiphany event. You don't "get it" until you
"get it", or as the dictionary says it is "an illuminating discovery,
realization, or disclosure".
The only way to cross the chasm is to use the new tool.
Once you "get it" you'll never go back.
Axiom is about ideas, not code. It is a way of structuring
computational mathematics. It is not just a tool to get an answer, it
is a tool to get the right answer. Using the tool properly implies you
understand the tool, its uses, and its limitations. Enhancing the tool
implies you understand the model and its assumptions. All of that
means that we have to communicate to people as well as machines.
Literate programming is a vehicle to communicate to both.
Tim
From MAILER-DAEMON Fri Jul 10 20:19:27 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZDiVr-0000Cp-Ka
for mharc-axiom-developer@gnu.org; Fri, 10 Jul 2015 20:19:27 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:43949)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDiVo-0000CF-SJ
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 20:19:25 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZDiVl-0004Vj-M8
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 20:19:24 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:49594
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDiVl-0004VZ-Gv
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 20:19:21 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6B0JKFI019474;
Fri, 10 Jul 2015 19:19:20 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6B0JJMT019471;
Fri, 10 Jul 2015 19:19:19 -0500
Date: Fri, 10 Jul 2015 19:19:19 -0500
Message-Id: <201507110019.t6B0JJMT019471@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Proving Axiom correct
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 11 Jul 2015 00:19:25 -0000
There is a free book "Certified Programming with Dependent Types"
about COQ available at:
http://adam.chlipala.net/cpdt/cpdt.pdf
Tim
From MAILER-DAEMON Fri Jul 10 20:55:05 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZDj4L-0002Ii-K9
for mharc-axiom-developer@gnu.org; Fri, 10 Jul 2015 20:55:05 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:47980)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDj4K-0002IB-6U
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 20:55:04 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZDj4G-0001gV-7J
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 20:55:04 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:59781
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDj4G-0001gJ-2L
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 20:55:00 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6B0stFI019555;
Fri, 10 Jul 2015 19:54:55 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6B0ssf0019552;
Fri, 10 Jul 2015 19:54:54 -0500
Date: Fri, 10 Jul 2015 19:54:54 -0500
Message-Id: <201507110054.t6B0ssf0019552@axiom-developer.org>
To: thery@sophia.inria.fr, Laurent.Thery@inria.fr
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Cc: axiom-developer@nongnu.org
Subject: [Axiom-developer] Machine Checked Implementation of BuchBerger's
Algorithm
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 11 Jul 2015 00:55:05 -0000
I'm Tim Daly, lead developer on the Axiom computer algebra system.
I'm sorry if this is not to the correct person.
I'm looking to contact Laurent Thery about the files for the
implementation and proof of Buchberger's Algorithm. There is a
link in the paper to http://www.inria.fr/lemme/buch but it is dead.
Is there somewhere I can reach the sources? I'd like to reproduce
the work to understand it better.
Tim Daly
From MAILER-DAEMON Fri Jul 10 21:16:43 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZDjPH-0007Bl-2X
for mharc-axiom-developer@gnu.org; Fri, 10 Jul 2015 21:16:43 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:50619)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDjPE-0007BY-5o
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 21:16:41 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZDjPB-0001xt-0W
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 21:16:40 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:36834
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZDjPA-0001xp-SA
for axiom-developer@nongnu.org; Fri, 10 Jul 2015 21:16:36 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6B1GZFI019822;
Fri, 10 Jul 2015 20:16:35 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6B1GWxb019819;
Fri, 10 Jul 2015 20:16:32 -0500
Date: Fri, 10 Jul 2015 20:16:32 -0500
Message-Id: <201507110116.t6B1GWxb019819@axiom-developer.org>
To: immaculada.medina@uca.es, rancisco.palomo@uca.es, jalonso@us.es,
jruiz@us.es
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Cc: axiom-developer@nongnu.org
Subject: [Axiom-developer] Verified Computer Algebra in ACL2
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 11 Jul 2015 01:16:41 -0000
I'm Tim Daly, Lead developer on the Axiom computer algebra system.
I'm reading the paper "Verified Computer Algebra in ACL2".
Is the code available somewhere? I'd like to reproduce the result
and understand the details.
Tim Daly
http://daly.axiom-developer.org
From MAILER-DAEMON Sun Jul 12 16:01:48 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZENRc-0002pZ-Eo
for mharc-axiom-developer@gnu.org; Sun, 12 Jul 2015 16:01:48 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:42255)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZENRZ-0002o9-K0
for axiom-developer@nongnu.org; Sun, 12 Jul 2015 16:01:46 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZENRV-0006Fr-DI
for axiom-developer@nongnu.org; Sun, 12 Jul 2015 16:01:45 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:45898
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZENRV-0006FU-7x
for axiom-developer@nongnu.org; Sun, 12 Jul 2015 16:01:41 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6CK1dFI015250;
Sun, 12 Jul 2015 15:01:39 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6CK1d5h015247;
Sun, 12 Jul 2015 15:01:39 -0500
Date: Sun, 12 Jul 2015 15:01:39 -0500
Message-Id: <201507122001.t6CK1d5h015247@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] COQ and Axiom
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 12 Jul 2015 20:01:46 -0000
Axiom has a project goal of Proving Axiom Correct. This is
computational mathematics. It needs a solid foundation.
There are limits to what can be proven, of course, but the power
of the proof systems has really improved since Axiom was born.
Of the half-dozen or more proof systems and it appears that COQ
is closest to Spad in spirit. COQ has the ability to handle dependent
types (e.g. specifying that an array has a fixed known length). COQ
has the ability to generate OCAML programs from proofs. This will
make it easy to compare with the Spad implementations. A major win
in the long term would be to auto-generate the Spad code but that's
a distant dream at the moment.
Axiom is being attacked from two directions. The first is from the
"categories down", trying to specify Axiom's category signatures in
COQ. The second is from the "bits up", trying to specify the lisp
functions that are implemented using only common lisp primitives.
These are marked in the interpreter already and will soon have
OCAML-like type signatures.
If anyone knows of prior work on either path, please let me know.
We have already gotten permission from Laurant Thery to use his work
on the proof of Buchberger's algorithm, some of which will show up
in Volume 13. I have to reverse-engineer his proof into the Spad
implementation.
Tim
From MAILER-DAEMON Wed Jul 15 16:13:12 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZFT3I-0001CG-Dk
for mharc-axiom-developer@gnu.org; Wed, 15 Jul 2015 16:13:12 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:52358)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZFT3D-00014Z-4q
for axiom-developer@nongnu.org; Wed, 15 Jul 2015 16:13:11 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZFT36-0005QG-2y
for axiom-developer@nongnu.org; Wed, 15 Jul 2015 16:13:06 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:41525
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZFT35-0005Ox-VE
for axiom-developer@nongnu.org; Wed, 15 Jul 2015 16:13:00 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6FKCwFI006884;
Wed, 15 Jul 2015 15:12:58 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6FKCvAC006881;
Wed, 15 Jul 2015 15:12:57 -0500
Date: Wed, 15 Jul 2015 15:12:57 -0500
Message-Id: <201507152012.t6FKCvAC006881@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Proving Axiom Correct
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Wed, 15 Jul 2015 20:13:11 -0000
The latest update contains the first proof of Axiom's Common Lisp
code using ACL2. ACL2 is a common lisp that has proof technology
and since Axiom is all common lisp (no boot code), this is a good
basis for proofs.
This update proves that the predicate isWrapped takes anything as
an argument and returns either t or nil. One caveat is that ACL2
does not handle floating point so (floatp x) is omitted but this
is fine for now. The signature line is
isWrapped: t -> (or t nil)
The plan of attack is to prove functions which use only common lisp
primitives in their implementation first and then work upward through
functions that use only the proven set. The base level functions are
already marked in the interpreter.
In the longer term ACL2 will be integrated into the build process so
each release has an ever-growing proven subset.
This is the first step in a very large task.
Tim
From MAILER-DAEMON Wed Jul 15 22:47:45 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZFZD6-0000Dq-NO
for mharc-axiom-developer@gnu.org; Wed, 15 Jul 2015 22:47:44 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:49023)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZFZD4-00009m-CZ
for axiom-developer@nongnu.org; Wed, 15 Jul 2015 22:47:43 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZFZD1-0004aQ-5T
for axiom-developer@nongnu.org; Wed, 15 Jul 2015 22:47:42 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:48098
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZFZD1-0004aM-0V
for axiom-developer@nongnu.org; Wed, 15 Jul 2015 22:47:39 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6G2lbFI007523;
Wed, 15 Jul 2015 21:47:37 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6G2lbfm007520;
Wed, 15 Jul 2015 21:47:37 -0500
Date: Wed, 15 Jul 2015 21:47:37 -0500
Message-Id: <201507160247.t6G2lbfm007520@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Proving Axiom Correct
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 16 Jul 2015 02:47:43 -0000
The system build has now been updated to automatically extract
and prove any acl2 stanzas. This behavior is activated by including
ACL2=acl2 on the make command line. This will, of course, only work
if you have acl2 installed.
This automation will make sure the proofs occur at build time
in order to catch failures. Currently, failing tests will not
stop the build. The plan is to report failures after the build
just as we do with the regression test suite.
Tim
From MAILER-DAEMON Thu Jul 16 02:03:16 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZFcGK-0007R5-4s
for mharc-axiom-developer@gnu.org; Thu, 16 Jul 2015 02:03:16 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:36227)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZFcGF-0007QU-WD
for axiom-developer@nongnu.org; Thu, 16 Jul 2015 02:03:12 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZFcGB-0001q7-W0
for axiom-developer@nongnu.org; Thu, 16 Jul 2015 02:03:11 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:59166
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZFcGB-0001q3-Rc
for axiom-developer@nongnu.org; Thu, 16 Jul 2015 02:03:07 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6G636FI007930;
Thu, 16 Jul 2015 01:03:06 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6G636xa007927;
Thu, 16 Jul 2015 01:03:06 -0500
Date: Thu, 16 Jul 2015 01:03:06 -0500
Message-Id: <201507160603.t6G636xa007927@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Proving Axiom Correct
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 16 Jul 2015 06:03:14 -0000
COQ is being used as the proof engine for Spad-level code.
The latest change will automatically extract literate chunks
labelled 'coq' into a separate location for the COQ proof engine.
This can be controlled from the make command line by adding COQ=coq.
ACL2, with its lisp-based syntax and semantics, is the appropriate
engine for proving the interpreter and compiler. COQ, with its
ability to form dependent types, is the appropriate engine for
proving the algebra. Thus we're able to use the best tool for
each level of abstraction.
Tim
From MAILER-DAEMON Sat Jul 18 20:50:02 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZGcnq-00067V-6D
for mharc-axiom-developer@gnu.org; Sat, 18 Jul 2015 20:50:02 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:55180)
by lists.gnu.org with esmtp (Exim 4.71) (envelope-from )
id 1ZGcnn-000670-Ql
for axiom-developer@nongnu.org; Sat, 18 Jul 2015 20:50:00 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZGcnk-0006Q7-L5
for axiom-developer@nongnu.org; Sat, 18 Jul 2015 20:49:59 -0400
Received: from server22.hostfactory.ch ([62.146.13.88]:35719)
by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from )
id 1ZGcnk-0006P2-EL
for axiom-developer@nongnu.org; Sat, 18 Jul 2015 20:49:56 -0400
Received: from [192.168.0.100] (unknown [109.71.88.60])
by server22.hostfactory.ch (Postfix) with ESMTPSA id A7F9C600124EC
for ; Sun, 19 Jul 2015 02:49:52 +0200 (CEST)
Message-ID: <55AAF423.1040700@scios.ch>
Date: Sun, 19 Jul 2015 02:49:39 +0200
From: Kurt Pagani
Organization: SciOS Scientific Operating Systems GmbH
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64;
rv:31.0) Gecko/20100101 Thunderbird/31.7.0
MIME-Version: 1.0
To: axiom-developer@nongnu.org
References: <201507160603.t6G636xa007927@axiom-developer.org>
In-Reply-To: <201507160603.t6G636xa007927@axiom-developer.org>
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: 7bit
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x
X-Received-From: 62.146.13.88
Subject: Re: [Axiom-developer] Proving Axiom Correct
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 19 Jul 2015 00:50:01 -0000
Hi Tim
that's great, indeed. Coq also seems to me best suited for this
challenging task, however, I would suggest to use "the mathematical
proof language (MPL)" as described in chapeter 11 of the reference
manual. It's a matter of taste, of courese, but imho MPL is much more
readable (at least to mathematicians) I guess.
The following primitive example (standard vs. mpl) might be convincing.
Standard proof language:
------------------------
Section Group.
Parameter S : Set.
Parameter e : S.
Parameter inv : S -> S.
Parameter op: S -> S -> S.
Infix "*" := op.
Axiom left_id : forall x:S, e * x = x.
Axiom left_inv : forall x:S, inv x * x = e.
Axiom assoc : forall x y z:S, x * (y * z) = (x * y) * z.
Proposition left_cancel :
forall x y z:S, x * y = x * z -> y = z.
Proof.
intros.
assert (inv x * (x * y) = inv x * (x * z)) as H1.
rewrite H.
reflexivity.
rewrite assoc in H1.
rewrite assoc in H1.
rewrite left_inv in H1.
rewrite left_id in H1.
rewrite left_id in H1.
assumption.
Qed.
Proposition right_id :
forall x:S, x * e = x.
Proof.
intros.
apply left_cancel with (x:=inv x).
rewrite assoc.
rewrite left_inv.
apply left_id.
Qed.
the same in MPL:
----------------
Section Group.
Parameter S : Set.
Parameter e : S.
Parameter inv : S -> S.
Parameter op: S -> S -> S.
Infix "*" := op.
Axiom left_id : forall x:S, e * x = x.
Axiom left_inv : forall x:S, inv x * x = e.
Axiom assoc : forall x y z:S, x * (y * z) = (x * y) * z.
Proposition left_cancel :
forall x y z:S, x * y = x * z -> y = z.
proof.
let x:S, y:S, z:S.
assume (x*y=x*z).
then (inv x *(x*y) = inv x * (x*z)).
then ((inv x * x)*y=(inv x* x)*z) by assoc.
then (e*y=e*z) by left_inv.
then (y=z) by left_id.
take _fact0.
end proof.
Qed.
Proposition right_id :
forall x:S, x * e = x.
proof.
let x:S.
then (e*e=e) by left_id.
then ((inv x * x)*e=inv x * x) by left_inv.
then (inv x*(x*e)= inv x * x) by assoc.
hence (x*e=x) by left_cancel.
end proof.
Qed.
Well, it's a quick hack, however, it contains almost every principle to
prove the 'algebra' correct.
Kurt
Am 16.07.2015 um 08:03 schrieb daly@axiom-developer.org:
> COQ is being used as the proof engine for Spad-level code.
>
> The latest change will automatically extract literate chunks
> labelled 'coq' into a separate location for the COQ proof engine.
> This can be controlled from the make command line by adding COQ=coq.
>
> ACL2, with its lisp-based syntax and semantics, is the appropriate
> engine for proving the interpreter and compiler. COQ, with its
> ability to form dependent types, is the appropriate engine for
> proving the algebra. Thus we're able to use the best tool for
> each level of abstraction.
>
> Tim
>
> _______________________________________________
> Axiom-developer mailing list
> Axiom-developer@nongnu.org
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>
From MAILER-DAEMON Sat Jul 18 21:00:31 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZGcxz-0007iy-Jz
for mharc-axiom-developer@gnu.org; Sat, 18 Jul 2015 21:00:31 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:56556)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZGcxx-0007in-Ev
for axiom-developer@nongnu.org; Sat, 18 Jul 2015 21:00:30 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZGcxu-0001uC-AR
for axiom-developer@nongnu.org; Sat, 18 Jul 2015 21:00:29 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:37253
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZGcxu-0001tV-5U
for axiom-developer@nongnu.org; Sat, 18 Jul 2015 21:00:26 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6J10OFI021599;
Sat, 18 Jul 2015 20:00:24 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6J10Oe4021596;
Sat, 18 Jul 2015 20:00:24 -0500
Date: Sat, 18 Jul 2015 20:00:24 -0500
Message-Id: <201507190100.t6J10Oe4021596@axiom-developer.org>
To: Kurt Pagani , axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] MPL declarative style proofs
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 19 Jul 2015 01:00:30 -0000
Very nice.
I will try to use it as a first example. I've been concentrating
on the ACL2 level at the moment but I just changed Axiom to use
COQ on extracted proofs. Since this works from coqtop it looks like
I can use it for checking during the build.
Thanks for the reference.
Tim
From MAILER-DAEMON Sat Jul 25 07:38:12 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZIxmO-00013b-29
for mharc-axiom-developer@gnu.org; Sat, 25 Jul 2015 07:38:12 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:55522)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZIxmJ-00013L-UI
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 07:38:09 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZIxmG-0001w0-JR
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 07:38:07 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:48482
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZIxmG-0001vw-E9
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 07:38:04 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6PBc3FI031085;
Sat, 25 Jul 2015 06:38:03 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6PBc2jr031082;
Sat, 25 Jul 2015 06:38:02 -0500
Date: Sat, 25 Jul 2015 06:38:02 -0500
Message-Id: <201507251138.t6PBc2jr031082@axiom-developer.org>
To: axiom-developer@nongnu.org
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Subject: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 25 Jul 2015 11:38:09 -0000
Axiom has moved into a new phase. The goal is to prove Axiom correct.
There are several tools and several levels of proof. I've added
the machinery to run proofs in COQ (for algebra) and ACL2 (for
the interpreter and compiler).
One of the first steps for the algebra proofs involves decorating
the categories with their mathematical axioms. That's where I am
asking for your help.
There are 241 categories, such as Monoid, which need to be annotated.
I've listed them below, sorted in the order by which they inherit
from prior categories, so that the complexity increases. The file
http://axiom-developer.org/axiom-website/endpaper.pdf
has a graph of the categories from the Jenks book which could be
a great help.
Please look at the categories and find or create the axioms.
If you have a particularly good reference page on the web or
a particularly good book that lists them, please let me know.
The axioms have to be in a certain form so they can be used in
the calculus of inductive constructions (the theory behind COQ).
The plan is to decorate the categories, then provide proofs for
category-default code. Unfortunately, Axiom is circular so some
of the domains are going to require proofs also.
This task should be at least as hard as it was to get Axiom to
build stand-alone in the first place which took about a year.
The best case will be that the implementations are proven correct.
The bad case will be corner cases where the implementation cannot
be proven.
In any case, your help will make this first step easier. Drag out
your favorite reference book and decorate LeftModule :-).
Thanks,
Tim
==================================================================
ATADDVA AdditiveValuationAttribute
ATAPPRO ApproximateAttribute
ATARBEX ArbitraryExponentAttribute
ATARBPR ArbitraryPrecisionAttribute
AHYP ArcHyperbolicFunctionCategory
ATRIG ArcTrigonometricFunctionCategory
ATTREG AttributeRegistry
BASTYPE BasicType
ATCANON CanonicalAttribute
ATCANCL CanonicalClosedAttribute
ATCUNOR CanonicalUnitNormalAttribute
ATCENRL CentralAttribute
KOERCE CoercibleTo
CFCAT CombinatorialFunctionCategory
ATCS CommutativeStarAttribute
KONVERT ConvertibleTo
ELEMFUN ElementaryFunctionCategory
ELTAB Eltable
ATFINAG FiniteAggregateAttribute
HYPCAT HyperbolicFunctionCategory
IEVALAB InnerEvalable
ATJACID JacobiIdentityAttribute
ATLR LazyRepresentationAttribute
ATLUNIT LeftUnitaryAttribute
MAGCDOC ModularAlgebraicGcdOperations
ATMULVA MultiplicativeValuationAttribute
ATNOTHR NotherianAttribute
ATNZDIV NoZeroDivisorsAttribute
ATNULSQ NullSquareAttribute
OM OpenMath
ATPOSET PartiallyOrderedSetAttribute
PTRANFN PartialTranscendentalFunctions
PATAB Patternable
PRIMCAT PrimitiveFunctionCategory
RADCAT RadicalCategory
RETRACT RetractableTo
ATRUNIT RightUnitaryAttribute
ATSHMUT ShallowlyMutableAttribute
SPFCAT SpecialFunctionCategory
TRIGCAT TrigonometricFunctionCategory
TYPE Type
ATUNIKN UnitsKnownAttribute
AGG Aggregate
COMBOPC CombinatorialOpsCategory
COMPAR Comparable
ELTAGG EltableAggregate
EVALAB Evalable
FORTCAT FortranProgramCategory
FRETRCT FullyRetractableTo
FPATMAB FullyPatternMatchable
LOGIC Logic
PPCURVE PlottablePlaneCurveCategory
PSCURVE PlottableSpaceCurveCategory
REAL RealConstant
SEGCAT SegmentCategory
SETCAT SetCategory
TRANFUN TranscendentalFunctionCategory
ABELSG AbelianSemiGroup
BLMETCT BlowUpMethodCategory
DSTRCAT DesingTreeCategory
FORTFN FortranFunctionCategory
FMC FortranMatrixCategory
FMFUN FortranMatrixFunctionCategory
FVC FortranVectorCategory
FVFUN FortranVectorFunctionCategory
FEVALAB FullyEvalableOver
FILECAT FileCategory
FINITE Finite
FNCAT FileNameCategory
GRMOD GradedModule
LORER LeftOreRing
HOAGG HomogeneousAggregate
IDPC IndexedDirectProductCategory
LFCAT LiouvillianFunctionCategory
MONAD Monad
NUMINT NumericalIntegrationCategory
OPTCAT NumericalOptimizationCategory
ODECAT OrdinaryDifferentialEquationsSolverCategory
ORDSET OrderedSet
PDECAT PartialDifferentialEquationsSolverCategory
PATMAB PatternMatchable
RRCC RealRootCharacterizationCategory
SEGXCAT SegmentExpansionCategory
SGROUP SemiGroup
SETCATD SetCategoryWithDegree
SEXCAT SExpressionCategory
STEP StepThrough
SPACEC ThreeSpaceCategory
ABELMON AbelianMonoid
AFSPCAT AffineSpaceCategory
BGAGG BagAggregate
CACHSET CachableSet
CLAGG Collection
DVARCAT DifferentialVariableCategory
ES ExpressionSpace
GRALG GradedAlgebra
IXAGG IndexedAggregate
MONADWU MonadWithUnit
MONOID Monoid
ORDFIN OrderedFinite
PLACESC PlacesCategory
PRSPCAT ProjectiveSpaceCategory
RCAGG RecursiveAggregate
ARR2CAT TwoDimensionalArrayCategory
BRAGG BinaryRecursiveAggregate
CABMON CancellationAbelianMonoid
DIOPS DictionaryOperations
DLAGG DoublyLinkedAggregate
GROUP Group
LNAGG LinearAggregate
MATCAT MatrixCategory
OASGP OrderedAbelianSemiGroup
ORDMON OrderedMonoid
PSETCAT PolynomialSetCategory
PRQAGG PriorityQueueAggregate
QUAGG QueueAggregate
SETAGG SetAggregate
SKAGG StackAggregate
URAGG UnaryRecursiveAggregate
ABELGRP AbelianGroup
BTCAT BinaryTreeCategory
DIAGG Dictionary
DQAGG DequeueAggregate
ELAGG ExtensibleLinearAggregate
FLAGG FiniteLinearAggregate
FAMONC FreeAbelianMonoidCategory
MDAGG MultiDictionary
OAMON OrderedAbelianMonoid
PERMCAT PermutationCategory
STAGG StreamAggregate
TSETCAT TriangularSetCategory
FDIVCAT FiniteDivisorCategory
FSAGG FiniteSetAggregate
KDAGG KeyedDictionary
LZSTAGG LazyStreamAggregate
LMODULE LeftModule
LSAGG ListAggregate
MSETAGG MultisetAggregate
NARNG NonAssociativeRng
A1AGG OneDimensionalArrayAggregate
OCAMON OrderedCancellationAbelianMonoid
RSETCAT RegularTriangularSetCategory
RMODULE RightModule
RNG Rng
BMODULE BiModule
BTAGG BitAggregate
NASRING NonAssociativeRing
NTSCAT NormalizedTriangularSetCategory
OAGROUP OrderedAbelianGroup
OAMONS OrderedAbelianMonoidSup
OMSAGG OrderedMultisetAggregate
RING Ring
SFRTCAT SquareFreeRegularTriangularSetCategory
SRAGG StringAggregate
TBAGG TableAggregate
VECTCAT VectorCategory
ALAGG AssociationListAggregate
CHARNZ CharacteristicNonZero
CHARZ CharacteristicZero
COMRING CommutativeRing
DIFRING DifferentialRing
ENTIRER EntireRing
FMCAT FreeModuleCat
LALG LeftAlgebra
LINEXP LinearlyExplicitRingOver
MODULE Module
ORDRING OrderedRing
PDRING PartialDifferentialRing
PTCAT PointCategory
RMATCAT RectangularMatrixCategory
SNTSCAT SquareFreeNormalizedTriangularSetCategory
STRICAT StringCategory
OREPCAT UnivariateSkewPolynomialCategory
XALG XAlgebra
ALGEBRA Algebra
DIFEXT DifferentialExtension
FLINEXP FullyLinearlyExplicitRingOver
LIECAT LieAlgebra
LODOCAT LinearOrdinaryDifferentialOperatorCategory
NAALG NonAssociativeAlgebra
VSPACE VectorSpace
XFALG XFreeAlgebra
DIRPCAT DirectProductCategory
DIVRING DivisionRing
FINAALG FiniteRankNonAssociativeAlgebra
FLALG FreeLieAlgebra
INTDOM IntegralDomain
MLO MonogenicLinearOperator
OC OctonionCategory
QUATCAT QuaternionCategory
SMATCAT SquareMatrixCategory
XPOLYC XPolynomialsCat
AMR AbelianMonoidRing
FMTC FortranMachineTypeCategory
FRNAALG FramedNonAssociativeAlgebra
GCDDOM GcdDomain
OINTDOM OrderedIntegralDomain
FAMR FiniteAbelianMonoidRing
INTCAT IntervalCategory
PSCAT PowerSeriesCategory
PID PrincipalIdealDomain
UFD UniqueFactorizationDomain
DIVCAT DivisorCategory
EUCDOM EuclideanDomain
MTSCAT MultivariateTaylorSeriesCategory
PFECAT PolynomialFactorizationExplicit
UPSCAT UnivariatePowerSeriesCategory
FIELD Field
INS IntegerNumberSystem
LOCPOWC LocalPowerSeriesCategory
PADICCT PAdicIntegerCategory
POLYCAT PolynomialCategory
UTSCAT UnivariateTaylorSeriesCategory
ACF AlgebraicallyClosedField
DPOLCAT DifferentialPolynomialCategory
FPC FieldOfPrimeCharacteristic
FINRALG FiniteRankAlgebra
FS FunctionSpace
INFCLCT InfinitlyClosePointCategory
PACPERC PseudoAlgebraicClosureOfPerfectFieldCategory
QFCAT QuotientFieldCategory
RCFIELD RealClosedField
RNS RealNumberSystem
RPOLCAT RecursivePolynomialCategory
ULSCAT UnivariateLaurentSeriesCategory
UPXSCAT UnivariatePuiseuxSeriesCategory
UPOLYC UnivariatePolynomialCategory
ACFS AlgebraicallyClosedFunctionSpace
XF ExtensionField
FFIELDC FiniteFieldCategory
FPS FloatingPointSystem
FRAMALG FramedAlgebra
PACFFC PseudoAlgebraicClosureOfFiniteFieldCategory
ULSCCAT UnivariateLaurentSeriesConstructorCategory
UPXSCCA UnivariatePuiseuxSeriesConstructorCategory
FAXF FiniteAlgebraicExtensionField
MONOGEN MonogenicAlgebra
PACRATC PseudoAlgebraicClosureOfRationalNumberCategory
COMPCAT ComplexCategory
FFCAT FunctionFieldCategory
PACEXTC PseudoAlgebraicClosureOfAlgExtOfRationalNumberCategory
From MAILER-DAEMON Sat Jul 25 10:55:57 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZJ0rl-0008VA-Qv
for mharc-axiom-developer@gnu.org; Sat, 25 Jul 2015 10:55:57 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:45050)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJ0ri-0008Ua-3e
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 10:55:55 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZJ0rd-0001x3-2H
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 10:55:54 -0400
Received: from mail-qg0-x232.google.com ([2607:f8b0:400d:c04::232]:35523)
by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJ0rc-0001vv-HR
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 10:55:48 -0400
Received: by qgii95 with SMTP id i95so26032614qgi.2
for ; Sat, 25 Jul 2015 07:55:47 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113;
h=message-id:date:from:user-agent:mime-version:to:subject:references
:in-reply-to:content-type:content-transfer-encoding;
bh=BDe1QctihYEP5EHDoiCpceIhsW/bdRT21QWB2xsEK9U=;
b=pVVnR3XhQ3HQv4+G0M+kTjdViAwugxV34AOVD76UzGg9pyw1k6dKrsiJraNs3HYg+L
6IcBQTq6RABZ2j0cdS2XnKxAqTVUBAZZGMlqxoga/0Zg/oA7+5otPpnFE4IBaI16xD7z
qnLlwFbJ49o99Th6I9Lg+ya9bcY8cCtQYSCDBBbPE9CNRiKc5Kx9IObSzLbkwc2rRqNO
P8DBHzvfiqiv/pu6QGg72sz2dP59SglHJVbXxJMViIL8IyupIe+Q7agTWswzDyl6Hsr6
IJnV7VZ0p3zX+mCYTGv5WGwEWgDPKalBljwEibWI/AHW2SzBliYLNR/U43DYdyGnrXIN
UGYg==
X-Received: by 10.140.35.200 with SMTP id n66mr15527481qgn.21.1437836147401;
Sat, 25 Jul 2015 07:55:47 -0700 (PDT)
Received: from [192.168.1.122] (c-69-139-19-89.hsd1.pa.comcast.net.
[69.139.19.89]) by smtp.googlemail.com with ESMTPSA id
188sm5741604qhf.42.2015.07.25.07.55.46
for
(version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
Sat, 25 Jul 2015 07:55:46 -0700 (PDT)
Message-ID: <55B3A371.9060809@gmail.com>
Date: Sat, 25 Jul 2015 10:55:45 -0400
From: Raymond Rogers
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
rv:31.0) Gecko/20100101 Thunderbird/31.8.0
MIME-Version: 1.0
To: axiom-developer@nongnu.org
References: <201507251138.t6PBc2jr031082@axiom-developer.org>
In-Reply-To: <201507251138.t6PBc2jr031082@axiom-developer.org>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address
(bad octet value).
X-Received-From: 2607:f8b0:400d:c04::232
Subject: Re: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 25 Jul 2015 14:55:56 -0000
You will have to excuse me if I dozed off in the back seat during the trip.
Is this where we are?
We have a programming language (say SPAD or lisp) and a program in that
language represented by a series of statements.
The intent is to construct, in a literate manner, a series of statements
in MPL and SPAD that are flagged and readable by the respective
compilers such that if the MPL statements are logically correct
(assertions match conclusions) then SPAD will also reach the same
conclusions as you stated in MPL. Presumably that is also done by MPL
via a dictionary or some such.
For instance in Left Module Construction the assertions are equivalent
to a triple F: (R(\cdot , +),G(+),RxG->G(+) and the base qualification is:
R is a ring
G is a group
RxG is legitimate map from R,G to G
etc...
And fail (hopefully informatively) if one of these fails
or Return a construct that has all of the functional properties of Left
Modules.
Now the literate program has a "model" of Left Module in MPL and then
checks the SPAD code to see if it correctly does all the of the above
checks. If you have done all that then it seems to me that there should
also be a "hook" that check my custom code as well; of course that
should be optional and only done when required. And requires that I can
define my expectations for my code (which unfortunately I sometimes can't).
Forgive any ignorance but I left off back in the 80's with a Sandia (I
think) formalism to check the correctness of code. That is: make
assertions about what the code will do with the input and verify that
the code does that. To give credit this was supposed to be done by
first order predicate expressions that can be verified.
I would appreciate constructive corrections and suggestions.
Ray
On 07/25/2015 07:38 AM, daly@axiom-developer.org wrote:
> Axiom has moved into a new phase. The goal is to prove Axiom correct.
>
> There are several tools and several levels of proof. I've added
> the machinery to run proofs in COQ (for algebra) and ACL2 (for
> the interpreter and compiler).
>
> One of the first steps for the algebra proofs involves decorating
> the categories with their mathematical axioms. That's where I am
> asking for your help.
>
> There are 241 categories, such as Monoid, which need to be annotated.
> I've listed them below, sorted in the order by which they inherit
> from prior categories, so that the complexity increases. The file
> http://axiom-developer.org/axiom-website/endpaper.pdf
> has a graph of the categories from the Jenks book which could be
> a great help.
>
> Please look at the categories and find or create the axioms.
> If you have a particularly good reference page on the web or
> a particularly good book that lists them, please let me know.
>
> The axioms have to be in a certain form so they can be used in
> the calculus of inductive constructions (the theory behind COQ).
>
> The plan is to decorate the categories, then provide proofs for
> category-default code. Unfortunately, Axiom is circular so some
> of the domains are going to require proofs also.
>
> This task should be at least as hard as it was to get Axiom to
> build stand-alone in the first place which took about a year.
> The best case will be that the implementations are proven correct.
> The bad case will be corner cases where the implementation cannot
> be proven.
>
> In any case, your help will make this first step easier. Drag out
> your favorite reference book and decorate LeftModule :-).
>
> Thanks,
> Tim
>
> ==================================================================
>
> ATADDVA AdditiveValuationAttribute
> ATAPPRO ApproximateAttribute
> ATARBEX ArbitraryExponentAttribute
> ATARBPR ArbitraryPrecisionAttribute
> AHYP ArcHyperbolicFunctionCategory
> ATRIG ArcTrigonometricFunctionCategory
> ATTREG AttributeRegistry
> BASTYPE BasicType
> ATCANON CanonicalAttribute
> ATCANCL CanonicalClosedAttribute
> ATCUNOR CanonicalUnitNormalAttribute
> ATCENRL CentralAttribute
> KOERCE CoercibleTo
> CFCAT CombinatorialFunctionCategory
> ATCS CommutativeStarAttribute
> KONVERT ConvertibleTo
> ELEMFUN ElementaryFunctionCategory
> ELTAB Eltable
> ATFINAG FiniteAggregateAttribute
> HYPCAT HyperbolicFunctionCategory
> IEVALAB InnerEvalable
> ATJACID JacobiIdentityAttribute
> ATLR LazyRepresentationAttribute
> ATLUNIT LeftUnitaryAttribute
> MAGCDOC ModularAlgebraicGcdOperations
> ATMULVA MultiplicativeValuationAttribute
> ATNOTHR NotherianAttribute
> ATNZDIV NoZeroDivisorsAttribute
> ATNULSQ NullSquareAttribute
> OM OpenMath
> ATPOSET PartiallyOrderedSetAttribute
> PTRANFN PartialTranscendentalFunctions
> PATAB Patternable
> PRIMCAT PrimitiveFunctionCategory
> RADCAT RadicalCategory
> RETRACT RetractableTo
> ATRUNIT RightUnitaryAttribute
> ATSHMUT ShallowlyMutableAttribute
> SPFCAT SpecialFunctionCategory
> TRIGCAT TrigonometricFunctionCategory
> TYPE Type
> ATUNIKN UnitsKnownAttribute
> AGG Aggregate
> COMBOPC CombinatorialOpsCategory
> COMPAR Comparable
> ELTAGG EltableAggregate
> EVALAB Evalable
> FORTCAT FortranProgramCategory
> FRETRCT FullyRetractableTo
> FPATMAB FullyPatternMatchable
> LOGIC Logic
> PPCURVE PlottablePlaneCurveCategory
> PSCURVE PlottableSpaceCurveCategory
> REAL RealConstant
> SEGCAT SegmentCategory
> SETCAT SetCategory
> TRANFUN TranscendentalFunctionCategory
> ABELSG AbelianSemiGroup
> BLMETCT BlowUpMethodCategory
> DSTRCAT DesingTreeCategory
> FORTFN FortranFunctionCategory
> FMC FortranMatrixCategory
> FMFUN FortranMatrixFunctionCategory
> FVC FortranVectorCategory
> FVFUN FortranVectorFunctionCategory
> FEVALAB FullyEvalableOver
> FILECAT FileCategory
> FINITE Finite
> FNCAT FileNameCategory
> GRMOD GradedModule
> LORER LeftOreRing
> HOAGG HomogeneousAggregate
> IDPC IndexedDirectProductCategory
> LFCAT LiouvillianFunctionCategory
> MONAD Monad
> NUMINT NumericalIntegrationCategory
> OPTCAT NumericalOptimizationCategory
> ODECAT OrdinaryDifferentialEquationsSolverCategory
> ORDSET OrderedSet
> PDECAT PartialDifferentialEquationsSolverCategory
> PATMAB PatternMatchable
> RRCC RealRootCharacterizationCategory
> SEGXCAT SegmentExpansionCategory
> SGROUP SemiGroup
> SETCATD SetCategoryWithDegree
> SEXCAT SExpressionCategory
> STEP StepThrough
> SPACEC ThreeSpaceCategory
> ABELMON AbelianMonoid
> AFSPCAT AffineSpaceCategory
> BGAGG BagAggregate
> CACHSET CachableSet
> CLAGG Collection
> DVARCAT DifferentialVariableCategory
> ES ExpressionSpace
> GRALG GradedAlgebra
> IXAGG IndexedAggregate
> MONADWU MonadWithUnit
> MONOID Monoid
> ORDFIN OrderedFinite
> PLACESC PlacesCategory
> PRSPCAT ProjectiveSpaceCategory
> RCAGG RecursiveAggregate
> ARR2CAT TwoDimensionalArrayCategory
> BRAGG BinaryRecursiveAggregate
> CABMON CancellationAbelianMonoid
> DIOPS DictionaryOperations
> DLAGG DoublyLinkedAggregate
> GROUP Group
> LNAGG LinearAggregate
> MATCAT MatrixCategory
> OASGP OrderedAbelianSemiGroup
> ORDMON OrderedMonoid
> PSETCAT PolynomialSetCategory
> PRQAGG PriorityQueueAggregate
> QUAGG QueueAggregate
> SETAGG SetAggregate
> SKAGG StackAggregate
> URAGG UnaryRecursiveAggregate
> ABELGRP AbelianGroup
> BTCAT BinaryTreeCategory
> DIAGG Dictionary
> DQAGG DequeueAggregate
> ELAGG ExtensibleLinearAggregate
> FLAGG FiniteLinearAggregate
> FAMONC FreeAbelianMonoidCategory
> MDAGG MultiDictionary
> OAMON OrderedAbelianMonoid
> PERMCAT PermutationCategory
> STAGG StreamAggregate
> TSETCAT TriangularSetCategory
> FDIVCAT FiniteDivisorCategory
> FSAGG FiniteSetAggregate
> KDAGG KeyedDictionary
> LZSTAGG LazyStreamAggregate
> LMODULE LeftModule
> LSAGG ListAggregate
> MSETAGG MultisetAggregate
> NARNG NonAssociativeRng
> A1AGG OneDimensionalArrayAggregate
> OCAMON OrderedCancellationAbelianMonoid
> RSETCAT RegularTriangularSetCategory
> RMODULE RightModule
> RNG Rng
> BMODULE BiModule
> BTAGG BitAggregate
> NASRING NonAssociativeRing
> NTSCAT NormalizedTriangularSetCategory
> OAGROUP OrderedAbelianGroup
> OAMONS OrderedAbelianMonoidSup
> OMSAGG OrderedMultisetAggregate
> RING Ring
> SFRTCAT SquareFreeRegularTriangularSetCategory
> SRAGG StringAggregate
> TBAGG TableAggregate
> VECTCAT VectorCategory
> ALAGG AssociationListAggregate
> CHARNZ CharacteristicNonZero
> CHARZ CharacteristicZero
> COMRING CommutativeRing
> DIFRING DifferentialRing
> ENTIRER EntireRing
> FMCAT FreeModuleCat
> LALG LeftAlgebra
> LINEXP LinearlyExplicitRingOver
> MODULE Module
> ORDRING OrderedRing
> PDRING PartialDifferentialRing
> PTCAT PointCategory
> RMATCAT RectangularMatrixCategory
> SNTSCAT SquareFreeNormalizedTriangularSetCategory
> STRICAT StringCategory
> OREPCAT UnivariateSkewPolynomialCategory
> XALG XAlgebra
> ALGEBRA Algebra
> DIFEXT DifferentialExtension
> FLINEXP FullyLinearlyExplicitRingOver
> LIECAT LieAlgebra
> LODOCAT LinearOrdinaryDifferentialOperatorCategory
> NAALG NonAssociativeAlgebra
> VSPACE VectorSpace
> XFALG XFreeAlgebra
> DIRPCAT DirectProductCategory
> DIVRING DivisionRing
> FINAALG FiniteRankNonAssociativeAlgebra
> FLALG FreeLieAlgebra
> INTDOM IntegralDomain
> MLO MonogenicLinearOperator
> OC OctonionCategory
> QUATCAT QuaternionCategory
> SMATCAT SquareMatrixCategory
> XPOLYC XPolynomialsCat
> AMR AbelianMonoidRing
> FMTC FortranMachineTypeCategory
> FRNAALG FramedNonAssociativeAlgebra
> GCDDOM GcdDomain
> OINTDOM OrderedIntegralDomain
> FAMR FiniteAbelianMonoidRing
> INTCAT IntervalCategory
> PSCAT PowerSeriesCategory
> PID PrincipalIdealDomain
> UFD UniqueFactorizationDomain
> DIVCAT DivisorCategory
> EUCDOM EuclideanDomain
> MTSCAT MultivariateTaylorSeriesCategory
> PFECAT PolynomialFactorizationExplicit
> UPSCAT UnivariatePowerSeriesCategory
> FIELD Field
> INS IntegerNumberSystem
> LOCPOWC LocalPowerSeriesCategory
> PADICCT PAdicIntegerCategory
> POLYCAT PolynomialCategory
> UTSCAT UnivariateTaylorSeriesCategory
> ACF AlgebraicallyClosedField
> DPOLCAT DifferentialPolynomialCategory
> FPC FieldOfPrimeCharacteristic
> FINRALG FiniteRankAlgebra
> FS FunctionSpace
> INFCLCT InfinitlyClosePointCategory
> PACPERC PseudoAlgebraicClosureOfPerfectFieldCategory
> QFCAT QuotientFieldCategory
> RCFIELD RealClosedField
> RNS RealNumberSystem
> RPOLCAT RecursivePolynomialCategory
> ULSCAT UnivariateLaurentSeriesCategory
> UPXSCAT UnivariatePuiseuxSeriesCategory
> UPOLYC UnivariatePolynomialCategory
> ACFS AlgebraicallyClosedFunctionSpace
> XF ExtensionField
> FFIELDC FiniteFieldCategory
> FPS FloatingPointSystem
> FRAMALG FramedAlgebra
> PACFFC PseudoAlgebraicClosureOfFiniteFieldCategory
> ULSCCAT UnivariateLaurentSeriesConstructorCategory
> UPXSCCA UnivariatePuiseuxSeriesConstructorCategory
> FAXF FiniteAlgebraicExtensionField
> MONOGEN MonogenicAlgebra
> PACRATC PseudoAlgebraicClosureOfRationalNumberCategory
> COMPCAT ComplexCategory
> FFCAT FunctionFieldCategory
> PACEXTC PseudoAlgebraicClosureOfAlgExtOfRationalNumberCategory
>
> _______________________________________________
> Axiom-developer mailing list
> Axiom-developer@nongnu.org
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
--
Two views on life:
life is an art not to be learned by observation.
George Santayana:Interpretations of Poetry and Religion
It's kinda nice to participate in your life
Raymond Rogers
From MAILER-DAEMON Sat Jul 25 17:41:02 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZJ7Bm-0000YW-8K
for mharc-axiom-developer@gnu.org; Sat, 25 Jul 2015 17:41:02 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:42851)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJ7Bj-0000YI-Fl
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 17:41:01 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZJ7Bg-00083p-59
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 17:40:59 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:41358
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJ7Bg-00082x-0I
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 17:40:56 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6PLesFI008826;
Sat, 25 Jul 2015 16:40:54 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6PLersh008823;
Sat, 25 Jul 2015 16:40:53 -0500
Date: Sat, 25 Jul 2015 16:40:53 -0500
Message-Id: <201507252140.t6PLersh008823@axiom-developer.org>
To: Raymond Rogers
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Cc: axiom-developer@nongnu.org
Subject: Re: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 25 Jul 2015 21:41:01 -0000
>You will have to excuse me if I dozed off in the back seat during the
>trip. Is this where we are?
We're still lost but things have changed a bit since the 80s.
>We have a programming language (say SPAD or lisp) and a program in
>that language represented by a series of statements.
>The intent is to construct, in a literate manner, a series of
>statements in MPL and SPAD that are flagged and readable by the
>respective compilers such that if the MPL statements are logically
>correct (assertions match conclusions) then SPAD will also reach the
>same conclusions as you stated in MPL. Presumably that is also done
>by MPL via a dictionary or some such.
>For instance in Left Module Construction the assertions are equivalent
>to a triple F: (R(\cdot , +),G(+),RxG->G(+) and the base qualification is:
>R is a ring
>G is a group
>RxG is legitimate map from R,G to G
>etc...
>And fail (hopefully informatively) if one of these fails
>or Return a construct that has all of the functional properties of Left
>Modules.
>Now the literate program has a "model" of Left Module in MPL and then
>checks the SPAD code to see if it correctly does all the of the above
>checks. If you have done all that then it seems to me that there
>should also be a "hook" that check my custom code as well; of course
>that should be optional and only done when required. And requires
>that I can define my expectations for my code (which unfortunately I
>sometimes can't).
>Forgive any ignorance but I left off back in the 80's with a Sandia (I
>think) formalism to check the correctness of code. That is: make
>assertions about what the code will do with the input and verify that
>the code does that. To give credit this was supposed to be done by
>first order predicate expressions that can be verified.
>I would appreciate constructive corrections and suggestions.
It depends on what horizon we're discussing. There are at least 3
"in plan" at the moment, although like everything that isn't in
running code, this is subject to change.
THE NEAR TERM HORIZON
The near-term goal is to get the "first turn of the crank".
This first step in happening now.
Lisp Level Code
At the lisp level I've begun marking the code with two pieces of
information, a haskell-like type signature and a "level" indicator.
Lisp-level data structures will initially be used. These will get
closer to the Spad-level types (e.g. constructors) as the code gets
closer to Spad, which from the lisp viewpoint nothing more than a
domain-specific language (DSL).
The "level" indicator marks code with its "height" in the lisp
hierarchy. Code which is pure common lisp is marked at level 0.
Code implemented using only common lisp and level 0 code is level 1,
etc. This allows us to crawl up the code from ground-level.
Lisp-level code is being proven using ACL2 and side-level proofs.
That is, the "proof" is a version of the code that fits within the
ACL2 constraints (e.g. is not using floats). Some ACL2 code is
directly executable Common Lisp and will be used verbatim.
Currently this proven code is automatically extracted at build time
and given to ACL2 to prove.
Spad Level Code
At the Spad level, it appears that COQ is the closest in spirit.
COQ allows dependent types (e.g. arrays with fixed length) and
executable primitives so properties can be defined by code.
Here the game is to decorate the categories with mathematical
axioms. These axioms will be (re-)stated in COQ so they can be
used in proofs. The axioms are spread across the categories and
inherited using the same hierarchy as the category structure.
Thus Group inherits from Ring, etc.
Some categories provide default code. This will be the first
level of attack using COQ, trying to prove that the code conforms
to and correctly implements the axioms.
Machinery needs to be created to put these axioms into the
system in an effective way. For instance, )show should be able
to aggregate and display the inherited collection. The proof
extraction machine needs to be able to collect and assert the
axioms prior to proof.
Currently this proven code is automatically extracted at build time
and given to COQ to prove. COQ contains support for things like
integer arithmetic so this will help with the circular reference
issue.
"Other level" code
Axiom compiles to C using GCL. There is work based on LLVM that
supplies proof technology. C compiles to i86 machine code. I have
written a program which takes i86 binary code and produces
conditional-concurrent assignments (CCA) which define the machine
level semantics of each Intel instruction. The CCAs can be
combined to produce the semantics of blocks of code.
(see http://daly.axiom-developer.org/intel.pdf)
So there are the beginnings of "full stack" proof technologies
from Spad to machine code. In the near term we only care about
the Spad and Lisp code.
Expectations
This will be a learning experience. It is expected that the effort
will uncover bugs, misconceptions, and unprovable hypothesis cases.
THE MIDDLE TERM HORIZON
The near term proofs are "side-proofs" that sit alongside existing
code. However, we have complete control over the Spad-to-Lisp compiler
so it is possible to generate the proof code from the Spad code. We
also have complete control over the Lisp-to-C compiler so it is
possible to generate the proof code from the Lisp code. Even now some
ACL2 Lisp code is directly executable and I expect this trend to
continue.
This will certainly cause existing code to be reshaped, rewritten, and
reorganized. It will also make code even harder to write. But the
benefit is much higher confidence in the answers provided.
Since this will take a long time we can hope that the tools we use
will be much better. Quite a few things have changed since I used
NTHQM back in the distant past. I expect they will continue to change
for the better.
THE LONG TERM HORIZON
Computational mathematics is more constrained than general mathematics.
Proofs need to be constructive and need to account for more details.
That said, it is still mathematics. We can and should demand that
Axiom is "correct" for some provable version of "correct".
Already there are proofs of some algorithms. I have a proof of
Buchberger's algorithm. Ideally this proven code and its associated
proof can be directly inserted into Axiom.
This is a lot of work. Fortunately Axiom has a 30 year horizon so
there is plenty of time.
Tim
From MAILER-DAEMON Sat Jul 25 19:28:46 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZJ8s2-0004Vb-3B
for mharc-axiom-developer@gnu.org; Sat, 25 Jul 2015 19:28:46 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:60237)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJ8rz-0004U4-9K
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 19:28:45 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZJ8rw-0005Sr-0X
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 19:28:43 -0400
Received: from mail-qg0-x22f.google.com ([2607:f8b0:400d:c04::22f]:33601)
by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJ8rv-0005Sn-Ne
for axiom-developer@nongnu.org; Sat, 25 Jul 2015 19:28:39 -0400
Received: by qged69 with SMTP id d69so30523222qge.0
for ; Sat, 25 Jul 2015 16:28:39 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113;
h=message-id:date:from:user-agent:mime-version:to:cc:subject
:references:in-reply-to:content-type:content-transfer-encoding;
bh=IGKdXjCLIn7Pc2w5v2zc7/h0v8raJ4C/MifI+ZSaaqA=;
b=rrM7xmdn9Phk7RM+LISMvYlUCR+EjO/vKD5eO9uIvkl7CMcI2rMnzBjg4VNe8cqxnS
KF+i4tfsUZBrJhbc6ds2PrghSkcGtrmQXfdV7dKT1JMvOOAzm5D72nKFpiyBCD0xURgU
+i6/9r8DcxIDGs1rprChLCoYID+4wgg7cXSVPY60RDSIc0B8pbF2MCuun5/hA6pDfbIM
7AOJVlCGhySqrNkmSWpnL0Tyyr6MhggSu7WxEvD5VmSDvGCg2m0JXZWhrlcug3a/mU8K
T/7iYFpRB9Kl3NDgWfH81sA1oqicPjm7D9lTRRGFgbL5jsshQ4YmGQFuf+WuJfABUsJD
NDvw==
X-Received: by 10.140.35.200 with SMTP id n66mr17704632qgn.21.1437866919189;
Sat, 25 Jul 2015 16:28:39 -0700 (PDT)
Received: from [192.168.1.122] (c-69-139-19-89.hsd1.pa.comcast.net.
[69.139.19.89]) by smtp.googlemail.com with ESMTPSA id
z71sm6408118qkz.16.2015.07.25.16.28.38
(version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
Sat, 25 Jul 2015 16:28:38 -0700 (PDT)
Message-ID: <55B41BA6.9070102@gmail.com>
Date: Sat, 25 Jul 2015 19:28:38 -0400
From: Raymond Rogers
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
rv:31.0) Gecko/20100101 Thunderbird/31.8.0
MIME-Version: 1.0
To: daly@axiom-developer.org
References: <201507252140.t6PLersh008823@axiom-developer.org>
In-Reply-To: <201507252140.t6PLersh008823@axiom-developer.org>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address
(bad octet value).
X-Received-From: 2607:f8b0:400d:c04::22f
Cc: axiom-developer@nongnu.org
Subject: Re: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sat, 25 Jul 2015 23:28:45 -0000
Okay,
I looked at intel.pdf and brought to mind a crosscompiler I wrote way
back when. Convincing a PDP-8 compiler to generate object code for
something like a 6809. It's vague but I am convinced I was looking at
object code and outputting differrent object code. Or some such but
nevertheless there are resemblances.
Aside from the semantics you seem to be trying to convert one type of
code into another (of a mathematical syntax) or "decorate" existing
code for something else to agree with. or ??
Questions and comments inline:
On 07/25/2015 05:40 PM, daly@axiom-developer.org wrote:
> --------------------------------------------
> It depends on what horizon we're discussing. There are at least 3
> "in plan" at the moment, although like everything that isn't in
> running code, this is subject to change.
>
> THE NEAR TERM HORIZON
>
> The near-term goal is to get the "first turn of the crank".
> This first step in happening now.
>
> Lisp Level Code
>
> At the lisp level I've begun marking the code with two pieces of
> information, a haskell-like type signature and a "level" indicator.
> Lisp-level data structures will initially be used. These will get
> closer to the Spad-level types (e.g. constructors) as the code gets
> closer to Spad, which from the lisp viewpoint nothing more than a
> domain-specific language (DSL).
So when I feed SPAD a statement it will have been previously been
verified that the statement will be "correctly" interpreted and
excuted. "previously verified" means that it has been proven by a third
party that syntactically correct statements will result in results that
match some other description.
>
> The "level" indicator marks code with its "height" in the lisp
> hierarchy. Code which is pure common lisp is marked at level 0.
> Code implemented using only common lisp and level 0 code is level 1,
> etc. This allows us to crawl up the code from ground-level.
I really have doubts about relying on a single "level" indicator. My
experience is that more complex structures are necessary for effective
operation. Unless it's just used as a project management tool.
>
> Lisp-level code is being proven using ACL2 and side-level proofs.
> That is, the "proof" is a version of the code that fits within the
> ACL2 constraints (e.g. is not using floats). Some ACL2 code is
> directly executable Common Lisp and will be used verbatim.
I have to look ACL2 up and find out it's relationship to Lisp.
>
> Currently this proven code is automatically extracted at build time
> and given to ACL2 to prove.
So your saying that with a few additions no translation is needed?
That's good.
>
> Spad Level Code
>
> At the Spad level, it appears that COQ is the closest in spirit.
> COQ allows dependent types (e.g. arrays with fixed length) and
> executable primitives so properties can be defined by code.
>
> Here the game is to decorate the categories with mathematical
> axioms. These axioms will be (re-)stated in COQ so they can be
> used in proofs. The axioms are spread across the categories and
> inherited using the same hierarchy as the category structure.
> Thus Group inherits from Ring, etc.
re-stated? Is this to be contained in literate programming. What I
asking is why re-state? Is the input to be provided in CDQ format or is
some other program acting as an inter-mediator for both COQ and SPAD?
>
> Some categories provide default code. This will be the first
> level of attack using COQ, trying to prove that the code conforms
> to and correctly implements the axioms.
Okay, now we are on an internal code line and have stacked up a
data-structure with "history" (i.e. this term represents at least a
group) and we are asking some code A (SPAD or Axiom) to do something to
it; say provide an output. The fact that this code has been previously
checked by COQ will verify that code A will preform the modification as
described in some third format; presumably COQ.
>
> Machinery needs to be created to put these axioms into the
> system in an effective way. For instance, )show should be able
> to aggregate and display the inherited collection. The proof
> extraction machine needs to be able to collect and assert the
> axioms prior to proof.
Yes a hierarchy with clean goals would be nice. I have dug through some
of the background code in Axiom and some readability (literate
programming) would have been nice. But of course I have a simple mind
and limited knowledge.
>
> Currently this proven code is automatically extracted at build time
> and given to COQ to prove. COQ contains support for things like
> integer arithmetic so this will help with the circular reference
> issue.
I realize I am being lazy but a pointer to an example would be appreciated.
>
> "Other level" code
>
> Axiom compiles to C using GCL. There is work based on LLVM that
> supplies proof technology. C compiles to i86 machine code. I have
> written a program which takes i86 binary code and produces
> conditional-concurrent assignments (CCA) which define the machine
> level semantics of each Intel instruction. The CCAs can be
> combined to produce the semantics of blocks of code.
> (see http://daly.axiom-developer.org/intel.pdf)
>
> So there are the beginnings of "full stack" proof technologies
> from Spad to machine code. In the near term we only care about
> the Spad and Lisp code.
Now this has several levels, all of which seem to be related to
cross-compiling. I would feel much more secure if all of the
cross-compiling was handled by one agent; that can also be verified.
>
> Expectations
>
> This will be a learning experience. It is expected that the effort
> will uncover bugs, misconceptions, and unprovable hypothesis cases.
>
> THE MIDDLE TERM HORIZON
>
> The near term proofs are "side-proofs" that sit alongside existing
> code. However, we have complete control over the Spad-to-Lisp compiler
> so it is possible to generate the proof code from the Spad code. We
> also have complete control over the Lisp-to-C compiler so it is
> possible to generate the proof code from the Lisp code. Even now some
> ACL2 Lisp code is directly executable and I expect this trend to
> continue.
>
> This will certainly cause existing code to be reshaped, rewritten, and
> reorganized. It will also make code even harder to write. But the
> benefit is much higher confidence in the answers provided.
>
> Since this will take a long time we can hope that the tools we use
> will be much better. Quite a few things have changed since I used
> NTHQM back in the distant past. I expect they will continue to change
> for the better.
I can't remember or find NTHQM; I presume it's related to the history of
program verification (Sandia?).
>
> THE LONG TERM HORIZON
>
> Computational mathematics is more constrained than general mathematics.
> Proofs need to be constructive and need to account for more details.
> That said, it is still mathematics. We can and should demand that
> Axiom is "correct" for some provable version of "correct".
Oh yes: we would like to be "Standing on the shoulders of giants" not
being trampled underneath.
>
> Already there are proofs of some algorithms. I have a proof of
> Buchberger's algorithm. Ideally this proven code and its associated
> proof can be directly inserted into Axiom.
Sketch?
>
>
> This is a lot of work. Fortunately Axiom has a 30 year horizon so
> there is plenty of time.
>
> Tim
>
One further comment along the literate program lines. Unless the
organization and references are transparent, the project will be tower
of Babel with the same consequences. Although I think the world is
complex I do know that for human projects organization is key to continuity.
Euclid is my hero in math :):) Someone I appreciate more and more.
--
Two views on life:
life is an art not to be learned by observation.
George Santayana:Interpretations of Poetry and Religion
It's kinda nice to participate in your life
Raymond Rogers
From MAILER-DAEMON Sun Jul 26 12:53:37 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZJPBB-0007ap-De
for mharc-axiom-developer@gnu.org; Sun, 26 Jul 2015 12:53:37 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:45992)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJPB8-0007aP-Um
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 12:53:35 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZJPB4-0005hD-RS
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 12:53:34 -0400
Received: from mout.kundenserver.de ([212.227.17.13]:51574)
by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJPB4-0005gr-IH
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 12:53:30 -0400
Received: from [192.168.0.3] ([90.215.183.139]) by mrelayeu.kundenserver.de
(mreue102) with ESMTPSA (Nemesis) id 0Lgpny-1YWcRS2bPa-00oHxa for
; Sun, 26 Jul 2015 18:53:28 +0200
To: axiom-developer@nongnu.org
References: <201507251138.t6PBc2jr031082@axiom-developer.org>
From: Martin Baker
Organization: axiom
Message-ID: <55B51085.2040704@martinb.com>
Date: Sun, 26 Jul 2015 17:53:25 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101
Thunderbird/38.1.0
MIME-Version: 1.0
In-Reply-To: <201507251138.t6PBc2jr031082@axiom-developer.org>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-Provags-ID: V03:K0:ADrrX5HxGljsJHcysjDzHiDJoKNjEavt5G83FYO8bd0blEVPS4v
YpSfXRdUTkXzHQnK/Y0OqQNZ3Ip1KjaorvNqKT24Gjg58p+zThLuRW+9S9tXUV4ndOk4n/6
VUoMfVmAej0WcDCVkq0glJycOkQn2+Tb6YrfGfoFoeVq1TUP7QfdShMJ589ygAtyjyOPW4D
J0jafDX7X0sFi6gQz7Hnw==
X-UI-Out-Filterresults: notjunk:1;V01:K0:KQ55LFVIVac=:NZh3FcGYb48UX98Y62QFFx
qftJKkNKJgaFvaN39Oo85kNo+MQ34TssCgarmZ2P6Efce4rJvuM6aJ0/p4rWUs3MliIKPZLuj
Nlr5fII4uYpdvHCWRKsbUvKSnj3V0xGIdNDt49Pw4OLDAy9088KnpSAeuj23r+2QWBxqtWkG9
0CBZOXinXe9+Uk8OZ51b3otqKHhgMDxaH5YjwZnRrqAWHZXumgv4AYFxMb7NiW0UlVMPv0yb9
8QLlK6nMUznAU1+wydRb+Aj4/wL/oyZsUrcL4fCFNNo0OeKJT7sP4qIDUA/V1Qo3yahknPL3Q
hShxWuii6xHhTCMzPTts0R2humZj7nBlGfqfydPTqw/GKss0IO6ng7raq4xeM3eWL2W9OSFMC
6b/CeXEDQXiu+UvyhQaYiBH3N9tLbD8ArjkxT3j3j1bRt/bQ1cwAgUiR6eFqr1qzh7HREjKNl
3xfM5kawKC6yMjSpla7C8wMPggdAJDTXrcOB/p9eza84PyUlm3ka93TpHaepewBtb+9SECL6l
8nKOD1V/1U7tusfRc6Px4DKYC59Fs3d6ytdLgCn9HLJMyRJ1l0TVOk/aNCEvd9zZ8N60y9YMj
cWnU/hiQk0JHTGNwf1ZuxU6swgdAXCeUweghYmPuw9oDtYit3+x2zr7zDxmk2boXVK7dLG1Sx
tWBdCJr2FaewWDJnY+xVl5KnlvAHPT3Lo0CmsEAvsecvuCQ==
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x [generic]
X-Received-From: 212.227.17.13
Subject: Re: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 26 Jul 2015 16:53:35 -0000
On 25/07/15 12:38, daly@axiom-developer.org wrote:
> Axiom has moved into a new phase. The goal is to prove Axiom correct.
Tim,
Why not do the easy bit first and just mark up the operators, in
domains, with the following common Axioms/Identities?
Only for functions with signature: ($,$)->Boolean
reflexivity forall(x): x<=x
antisymmetry forall(x,y): x<=y and y<=x implies x=y
symmetry forall(x,y): x<=y and y<=x implies error
transitivity forall(x,y,z): x<=y and y<=z implies x<=z
Only for operators with signature: ($,$)->$
commutativity: forall(x,y): x o y=y o x
associativity: forall(x,y,z): (x o y) o z=y o (x o z)
unit: forall x: x o 1=x
idempotence: forall x: x o x=x
absorption1: forall(x,y): x o (x * y)=x
absorption2: forall(x,y): x * (x o y)=x
distribution1: forall(x,y,z): x o (y * z)=(x o y) * (x o z)
distribution2: forall(x,y,z): x * (y o z)=(x * y) o (x * z)
where 'o' and '*' are replaced with the actual operator symbol.
Perhaps you could translate the above to COQ syntax?
This might be the easy bit because you only need to check for the above
signatures and in most cases it is fairly well known if operators obey
these identities.
What would be very interesting would be to have a program which
generates these identities, wherever they occur in the Axiom library,
put random values into the variables and check for non-compliance.
Martin
From MAILER-DAEMON Sun Jul 26 13:35:44 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZJPpw-0006GV-5y
for mharc-axiom-developer@gnu.org; Sun, 26 Jul 2015 13:35:44 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:53410)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJPpu-0006GE-5y
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 13:35:43 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZJPpo-0000n7-G8
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 13:35:42 -0400
Received: from mail-qg0-x22b.google.com ([2607:f8b0:400d:c04::22b]:36301)
by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJPpo-0000mZ-9b
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 13:35:36 -0400
Received: by qgy5 with SMTP id 5so38328863qgy.3
for ; Sun, 26 Jul 2015 10:35:35 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113;
h=message-id:date:from:user-agent:mime-version:to:subject:references
:in-reply-to:content-type:content-transfer-encoding;
bh=vtuc1SIe8hLUrnA3SkhcInXxEz+8kPpkXrR68XM9DQU=;
b=m7FttznJk0dQxE5qcGGAX1MVPD4y7tUbKT4GJSe2EpdOQnDVdmOXDhUd4hZNgRl+cg
eQYWlQTEu+k+ai3y90egmaKzPitndPzp5WizYMpLND2ytzgHdtTS7D0ajdZ88kCKiZGd
zCuEse0pdQ4s+YGzE6hKU4OEw4UOxhXDPuFlSIxEV2PwF/11psIFQ9vOlWKWOi1aAItw
hkslQMj6yeplcw62aEjWylcW4Ssoe9FkN24ODqB2E86EQDNEmC0nXiFZJe0USLu9m4oS
wa/YHmz+Tlsy+GCeIiICknT9endTM5bhru6Tfql9Atvty3Ogl0CbKskuWheussnsPw6A
eVkA==
X-Received: by 10.140.29.202 with SMTP id b68mr34526479qgb.2.1437932135437;
Sun, 26 Jul 2015 10:35:35 -0700 (PDT)
Received: from [192.168.1.122] (c-69-139-19-89.hsd1.pa.comcast.net.
[69.139.19.89]) by smtp.googlemail.com with ESMTPSA id
e104sm7702403qgd.29.2015.07.26.10.35.34
for
(version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
Sun, 26 Jul 2015 10:35:34 -0700 (PDT)
Message-ID: <55B51A66.8040805@gmail.com>
Date: Sun, 26 Jul 2015 13:35:34 -0400
From: Raymond Rogers
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
rv:31.0) Gecko/20100101 Thunderbird/31.8.0
MIME-Version: 1.0
To: axiom-developer@nongnu.org
References: <201507251138.t6PBc2jr031082@axiom-developer.org>
<55B51085.2040704@martinb.com>
In-Reply-To: <55B51085.2040704@martinb.com>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address
(bad octet value).
X-Received-From: 2607:f8b0:400d:c04::22b
Subject: Re: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 26 Jul 2015 17:35:43 -0000
On 07/26/2015 12:53 PM, Martin Baker wrote:
> On 25/07/15 12:38, daly@axiom-developer.org wrote:
>> Axiom has moved into a new phase. The goal is to prove Axiom correct.
>
> Tim,
>
> Why not do the easy bit first and just mark up the operators, in
> domains, with the following common Axioms/Identities?
>
> Only for functions with signature: ($,$)->Boolean
>
> reflexivity forall(x): x<=x
> antisymmetry forall(x,y): x<=y and y<=x implies x=y
> symmetry forall(x,y): x<=y and y<=x implies error
> transitivity forall(x,y,z): x<=y and y<=z implies x<=z
I have problems with antisymmetry and symetry.
> Only for operators with signature: ($,$)->$
>
> commutativity: forall(x,y): x o y=y o x
> associativity: forall(x,y,z): (x o y) o z=y o (x o z)
> unit: forall x: x o 1=x
> idempotence: forall x: x o x=x
> absorption1: forall(x,y): x o (x * y)=x
> absorption2: forall(x,y): x * (x o y)=x
> distribution1: forall(x,y,z): x o (y * z)=(x o y) * (x o z)
> distribution2: forall(x,y,z): x * (y o z)=(x * y) o (x * z)
>
> where 'o' and '*' are replaced with the actual operator symbol.
>
> Perhaps you could translate the above to COQ syntax?
>
> This might be the easy bit because you only need to check for the
> above signatures and in most cases it is fairly well known if
> operators obey these identities.
>
> What would be very interesting would be to have a program which
> generates these identities, wherever they occur in the Axiom library,
> put random values into the variables and check for non-compliance.
I was also thinking along similar lines; but are the above assertions
that can be made x \in R or tests/validations of input variables/arguments?
These are of course simple cases; but I love simplicity.
Random variables? I wouldn't go there; for one thing "corner cases"
have to done if nothing else. As a matter of fact if you can find
"corners" and prove consistency between "corners" (say a convex hull in
function space) then proving corners is powerful in the sense we want.
That is not trying all possibilities. For instance equivalence
relations might be phrased as an assertion of convexity inside certain
things. If you like I might be able to rattle on about this; of course
it's probably my own eccentric terminology and I am studying Lie
Groups/Algebra so am inclined to apply the ideas to types of toothpaste :)
Ray
--
Two views on life:
life is an art not to be learned by observation.
George Santayana:Interpretations of Poetry and Religion
It's kinda nice to participate in your life
Raymond Rogers
From MAILER-DAEMON Sun Jul 26 15:26:39 2015
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ZJRZH-0007mU-E3
for mharc-axiom-developer@gnu.org; Sun, 26 Jul 2015 15:26:39 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:48765)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJRZF-0007mL-DB
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 15:26:38 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ZJRZC-0002hn-88
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 15:26:37 -0400
Received: from vs338.rosehosting.com ([209.135.140.38]:56069
helo=axiom-developer.org) by eggs.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1ZJRZC-0002hh-3Y
for axiom-developer@nongnu.org; Sun, 26 Jul 2015 15:26:34 -0400
Received: from axiom-developer.org (localhost.localdomain [127.0.0.1])
by axiom-developer.org (8.12.8/8.12.8) with ESMTP id t6QJQTFI019331;
Sun, 26 Jul 2015 14:26:29 -0500
From: daly@axiom-developer.org
Received: (from daly@localhost)
by axiom-developer.org (8.12.8/8.12.8/Submit) id t6QJQSXJ019328;
Sun, 26 Jul 2015 14:26:28 -0500
Date: Sun, 26 Jul 2015 14:26:28 -0500
Message-Id: <201507261926.t6QJQSXJ019328@axiom-developer.org>
To: Martin Baker
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x (barebone)
[generic]
X-Received-From: 209.135.140.38
Cc: axiom-developer@nongnu.org
Subject: Re: [Axiom-developer] Call for help
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive: