There has been a "great merger" of the idea=
s of Type Theory,

Category Theory, and Proof Theory. There is an =
interpretation

of a result in one in terms of the other two.

There has recently been a fundamentally new area of mathema=
tics

that merges ideas from those three areas with algebraic topology.<=
/div>

This area is called "Homotopy Type Theory". It appears =
to be a

"computable form of mathematics".=C2=A0

This represents, as near as I can understand, a new theor=
y

as fundamental as group theory. Axiom uses group theory as an) id 1cvwAI-000230-AB
for axiom-developer@nongnu.org; Wed, 05 Apr 2017 21:24:47 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1cvwAD-0007FA-9C
for axiom-developer@nongnu.org; Wed, 05 Apr 2017 21:24:46 -0400
Received: from nm27-vm3.bullet.mail.ne1.yahoo.com ([98.138.91.157]:46707)
by eggs.gnu.org with esmtps (TLS1.0:RSA_ARCFOUR_SHA1:16) (Exim 4.71)
(envelope-from ) id 1cvwAD-0007F4-2k
for axiom-developer@nongnu.org; Wed, 05 Apr 2017 21:24:41 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yahoo.com; s=s2048;
t=1491441880; bh=hrw1Tv8K2FqFYVu8Z7pjKJGGyAjZZEE/cbNsEua8QXM=;
h=Date:From:To:In-Reply-To:References:Subject:From:Subject;
b=Hm7oBghVuR+m2Yal6TP+3KylKlQOyBdR/t/IzvDUSMMt9xq6rxLhoCKQCHIaPF3A7C26xmBV9XW+VZj27bY70S3DQLJQwbCBirtVPeb85TRGkdVt/j8cFt0VFt6yYV5nriwW3nLBP3KhM5A/i88rD6rKx5GGpvHigXAjarPnGUEU0VsoBAHqjFRBZozE0ogd+qm/vnC/vfmpp5uTK6kj+TPp+PrYVkWmb9dsW1iH4GRUqhPrykZqsts5+UjvnqyZCBt3/OKudVpvDeMjAzxElN+WcbzZG+7Xm+dIb1Pu2C9ys2ZQh6lgkxG1zLCej6nBJDwjQsExL2hA8eIjtEo0Kg==
Received: from [98.138.226.179] by nm27.bullet.mail.ne1.yahoo.com with NNFMP;
06 Apr 2017 01:24:40 -0000
Received: from [98.138.89.250] by tm14.bullet.mail.ne1.yahoo.com with NNFMP;
06 Apr 2017 01:24:40 -0000
Received: from [127.0.0.1] by omp1042.mail.ne1.yahoo.com with NNFMP;
06 Apr 2017 01:24:40 -0000
X-Yahoo-Newman-Property: ymail-3
X-Yahoo-Newman-Id: 46516.13291.bm@omp1042.mail.ne1.yahoo.com
X-YMail-OSG: Wq_tnQsVM1nqKm7OeIfzzRMPHiGYqjw0fyYzxkqsTadfuH9ZOXB3Zdhw1lzXEuE
XysrSNaW2j.hCGTAe0lD7qu5f16yK_B2GAuCmmpvlXFtRVN.K5AYS_A93WOLY5CszN5ytIcT2tR2
Ejdz9DtveKOsJU_2gaObn.FaH3ZXDzbwd5gIVjkjn_OqWTQ6P_taa8noqXZCaIhzvMW2zxEFNNYd
MnP0yj0V0UAQgxz1Xa8puqpM5o7U4eHc0yIwUOtltYd7mYpDWQg6gS8CXUMT9pEZNsc9fPMVzFG6
2okxAPZ6FzuKdhMPL9HwS7qcgqPlVsGAQMEQsdNWNxRgi3SpmIXCLwO_p3Sbq7eECTC70_EfACaz
Im2PIHkL.xzboTEuOsFiIcf3T1.U.k7iNG8coszQ5SvR3qlTZDMxHBSEfyyxvhVgoxRSA5dJBt1c
0svKo6sV.IN6JNEtHcb.2Xkqvb9CvqSaaEHCw47RySXWAyEbtTCL_GbQLuuMHMJ_683cDwiy3Cyp
oxE0iyzJSPWSSdLVV2yOFSDQBONZ_ldX5X3YJCnEB_2GW
Received: from jws200184.mail.ne1.yahoo.com by
sendmailws147.mail.ne1.yahoo.com;
Thu, 06 Apr 2017 01:24:39 +0000; 1491441879.691
Date: Thu, 6 Apr 2017 01:24:39 +0000 (UTC)
From: C Y
To: Tim Daly , axiom-dev ,
Martin Baker , Tim Daly ,
Laurent Thery , Jeremy Avigad ,
Renaud Rioboo ,
Kurt Pagani , Frank Pfenning
Message-ID: <1908790900.1855510.1491441879517@mail.yahoo.com>
In-Reply-To:
References:
MIME-Version: 1.0
Content-Type: multipart/alternative;
boundary="----=_Part_1855509_604923384.1491441879516"
X-Mailer: WebService/1.1.9272 YMailNorrin Mozilla/5.0 (X11; Ubuntu;
Linux x86_64; rv:52.0) Gecko/20100101 Firefox/52.0
Content-Length: 2964
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x [fuzzy]
X-Received-From: 98.138.91.157
Subject: Re: [Axiom-developer] Proving Axiom Correct -- at the C level
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.21
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 06 Apr 2017 01:24:47 -0000
------=_Part_1855509_604923384.1491441879516
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
> On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly =
wrote:
> I previously mentioned the "proof tower" approach to the question
> of proving code at many different layers. Spad code proven in COQ,
> Lisp code in ACL2, and Intel code in CCAs. The missing step in the
> tower was C.
Rather than introduce another complex language and proof problem into the s=
tack, would it be possible to have Lisp implemented directly "on the metal"=
?=C2=A0 If SBCL isn't the preferred approach to such a system, maybe the fo=
llowing project could be used as a starting point to put together a purpose=
built LISP?
https://github.com/robert-strandh/SICL
Maybe some of the open source "LISP as OS" projects could offer lower level=
primitives from which to build the boot strapping code, or a basic set cou=
ld be defined in x86-64...=C2=A0 I suppose it's academic at this point, but=
I can't help wondering if there would be simplicity gains in the "expressi=
ng and defining proof stacks" department that would make it worthwhile in t=
he long run to hold the number of conceptual expression languages down to t=
he minimum necessary.
CY
------=_Part_1855509_604923384.1491441879516
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
) id 1cwF5P-0005Zw-Nq
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 17:37:00 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1cwF5O-00051p-IL
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 17:36:59 -0400
Received: from mail-wr0-x232.google.com ([2a00:1450:400c:c0c::232]:36019)
by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1cwF5O-00051L-91
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 17:36:58 -0400
Received: by mail-wr0-x232.google.com with SMTP id c55so8073884wrc.3
for ; Thu, 06 Apr 2017 14:36:58 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
h=mime-version:from:date:message-id:subject:to;
bh=BdvkeEuI3rTkduzcAqa7AofgNh9g71yQJJvM1no6XU8=;
b=pfVZfQOBenqHpZhli6Xt7VKkWVX+zJeMkcVhDFk3KauG/e6oHre0whzN0SJuUrmy3+
GC2jgco4W8NbFcxsXsB7ddGmQtlemQ1c/7s6p2lUu0Amn6CnJ5X1aYN2APShoNwjUSZF
dxq5sMEgP4ezdxd1hqjZplpGKJcCValzQxDAWNlC8qDlrnD6novFu6UoVkDNpb0YJwc9
geMHFhGG2J7oOe1u9QULJ8T5kxfu4azz2Yci8kQAn0HV/Jg0mFE13zoYSvx8FKECkgmL
94/5RcIXH8T/NwTI+pHDu9a23ALSPuGhib18n0eYZ8OmV6Zdgusidfggacflx+ZF4FDG
S6JQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:from:date:message-id:subject:to;
bh=BdvkeEuI3rTkduzcAqa7AofgNh9g71yQJJvM1no6XU8=;
b=QK0xIoeSDbLV7ikUDrcoF3WDGZlHAomjPoC7Jw9FjCDgQ1ufI35jJ8sy9LYZf9dUT2
gv1KI8gJZBv3G5LjDC5rbckubeCCUj9yH64qluUDUcQJhdTMaIwQc8a1KlRRDf8ZgqdS
R2SPMgOF5j1qL2APJkO6WbkpGQU+s8bVxwV54MTZ0NpvhpKBMk+8uqz6M9qy1jaCuqCP
lyCCK1K1JGzgU6iOGRcASktzH6UmIzRDyLuFXXgZkBN/K+wJXt22lTWzK5PZTF6Grj/D
TV4vU6bCeMoM0Q7F97Wf09r1kwMbDFrwbOPzGeUugBWWXYqrbs4oU9z25s2cshsVzHaU
j3hQ==
X-Gm-Message-State: AFeK/H2Nm3Nt2hs3cZ1UTso8HtpRu5LcWteJoRPMlG7a4tvSKmAqVj3GHID3JP3iDdnlfoDb9eqQMk+2xIe8sg==
X-Received: by 10.28.38.133 with SMTP id m127mr25521553wmm.41.1491514616815;
Thu, 06 Apr 2017 14:36:56 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.28.22.11 with HTTP; Thu, 6 Apr 2017 14:36:56 -0700 (PDT)
From: Tim Daly
Date: Thu, 6 Apr 2017 17:36:56 -0400
Message-ID:
To: Martin Baker , Tim Daly ,
axiom-dev
Content-Type: multipart/alternative; boundary=94eb2c03c314e9aad1054c864e35
X-detected-operating-system: by eggs.gnu.org: Genre and OS details not
recognized.
X-Received-From: 2a00:1450:400c:c0c::232
Subject: Re: [Axiom-developer] Small documentation problem
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.21
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 06 Apr 2017 21:37:01 -0000
--94eb2c03c314e9aad1054c864e35
Content-Type: text/plain; charset=UTF-8
I'll fix the duplicate line. Thanks for the bug report.
Any path that is convenient for reporting bugs is ok.
re: diagrams.
The diagrams in the Axiom pdf use .eps (which is
encapsulated postscript, i.e. postscript with size info).
The eps files live in books/ps with the convention that
books/ps/v103*
are images in volume 10.3. Your images are
books/ps/v103permgrpxx.eps
where xx is a sequential number.
If you tar up the .svg diagrams I can redo the images.
Alternatively, the pamphlet files are just raw latex. If you
cd to the books directory you should be able to just do
gcc -o tanglec tanglec.c
to get the tanglec program. You only need to do this once.
./tanglec bookvolbib.pamphlet axiom.bib >axiom.bib
latex bookvol10.3.pamphlet
makeindex bookvol10.3.idx
bibtex bookvol10.3.aux
latex bookvol10.3.pamphlet
latex bookvol10.3.pamphlet
dvipdfm bookvol10.3.dvi
evince bookvol10.3.pdf
Open a shell to run the above commands in a bash script.
If you leave the pdf viewer running it will update automatically
every time you remake the file. So you get a "hot loop' where
you change the pamphlet file, run the bash script, and see the
result immediately.
When you are happy with the changes you can do
git diff books/bookvol10.3.pamphlet >patchfile
and send me the patch file.
Tim
re: too much information
The target audience is students. I'm about to be a visiting
scholar at CMU and I hope to set up a seminar series to
attract students to working with Axiom. Since these are CS
students, not Math students, I assume they have very little
if any idea about group theory concepts.
Topics of a general nature would likely go into Volume 1, the
Axiom Tutorial. Topics specific to new algebra would modify
Volume 0, the Jenks book, in the appropriate algebra location,
in the help files, in hyperdoc, and in the (as yet unpublished)
web pages.
So there is a place somewhere in the system for documentation
at almost any level. Indeed, if all else seems inappropriate there
can always be a new volume.
Tim
--94eb2c03c314e9aad1054c864e35
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

re=
: diagrams.

The diagrams in the Axiom pdf use .eps (which is <=
br>encapsulated postscript, i.e. postscript with size info).

If=
you tar up the .svg diagrams I can redo the images.

scholar at CMU and I hope to set up a seminar series to

attract students to working with Axiom. Since these are CS

stu=
dents, not Math students, I assume they have very little

if any id=
ea about group theory concepts.

Topics of a general nature wou=
ld likely go into Volume 1, the

Axiom Tutorial. Topics specific to=
new algebra would modify

organizing scaffold for the algebra, giving it a clean structure.<=
/div>

=

--94eb2c03c31422c1f2054c620987--
From MAILER-DAEMON Wed Apr 05 21:24:49 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1cvwAL-00023W-5m
for mharc-axiom-developer@gnu.org; Wed, 05 Apr 2017 21:24:49 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:41310)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from Homotopy Type Theory (HoTT) looks like it could gi=
ve Axiom a

second scaffold of Type Theory / Proof Theory for prov=
ing=C2=A0

computational mathematics correct.

In particular, it seems that this "second Axiom scaffold", w=
hen the=C2=A0

theorems and proofs are matched with the group theo=
ry scaffold,

will give Axiom a very firm foundation for computati=
onal

mathematics.

Like group theory, HoT=
T is a steep hill to climb. There is a book

(available as a free =
PDF from HomotopyTypeTheory.org) called=C2=A0

Homotopy Type Theor=
y: Univalent Foundations of Mathematics.=C2=A0

It is the work of =
a large group of mathematician, published by the=C2=A0

Institute =
for Advanced Study.

The HoTT book is an intimidati=
ng piece of reading if you're not

familiar with all of the ar=
eas. A more gentle introduction would be

Pelayo and Warren, "=
;Homotopy Type Theory and Voevodsky's

Univalent Foundations&q=
uot; (https://arxiv.org/pdf=
/1210.5658.pdf)

This is the very bleeding edge=
of computational mathematics

and should put Axiom in the very he=
art of the developments.

A computer algebra system with proven so=
undness would change

the whole field.

Ti=
m

> On Friday, March 31, 2017, 7:16=
:32 PM EDT, Tim Daly <axiomcas@gmail.com> wrote:

> I previously= mentioned the "proof tower" approach to the question

> of proving co= de at many different layers. Spad code proven in COQ,

> Lisp code in = ACL2, and Intel code in CCAs. The missing step in the

> tower was C.<= br>

------=_Part_1855509_604923384.1491441879516--
From MAILER-DAEMON Thu Apr 06 06:41:28 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1cw4r2-0001Na-F9
for mharc-axiom-developer@gnu.org; Thu, 06 Apr 2017 06:41:28 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:34461)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1cw4r0-0001Mq-AW
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 06:41:27 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1cw4qw-0003Dg-EH
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 06:41:26 -0400
Received: from mout.kundenserver.de ([212.227.126.131]:55320)
by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1cw4qw-0003Br-2L
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 06:41:22 -0400
Received: from [192.168.1.160] ([86.180.113.209]) by mrelayeu.kundenserver.de
(mreue001 [212.227.15.167]) with ESMTPSA (Nemesis) id
0Ljz4s-1cOem41MTq-00c6Iv for ;
Thu, 06 Apr 2017 12:41:18 +0200
To: axiom-developer@nongnu.org
From: Martin Baker
Message-ID: <0a4101f9-b91e-1190-e963-09d40e05f96b@martinb.com>
Date: Thu, 6 Apr 2017 11:41:17 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
Thunderbird/45.8.0
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Provags-ID: V03:K0:Ng7qnbRhsLLkzMt2fP1QZQzQiss07lWevTiA4Hijkk0CqcEsdmH
mJpqBEYKRpqbJNLZV3bS5IgAgcZ0lO2Mpzv8Il+HBzeOZegUxo108AlRGAA3e4UWxXNjNVD
/Pi37ysR3QwqnnlNWXniH14ZJ+hrwMu1qwmFghWEKE+WcFGMI/rZVqmaSu+h9jbq4pEmONe
wb2XL7VinV55ABSIjUfAA==
X-UI-Out-Filterresults: notjunk:1;V01:K0:z+W2Oko4Y34=:bk7soTsqk9dGhP2O0eaw8F
E71Tued/EoUNkcIueTd3dHoX+y97JVe3laBRmnULI4jjrTT9lNroZiXdOyj4jwD4sU+uOTGRo
XRr8uxmCo3Ombd5LDYY5gidxqYdiMS6FcmkBPzJ6Vc8YKvIPMU732QImUkckQMMfjwuAEiJAm
Z/Se/U0C9QbojwMwhLWdNnR1lWGr74SDOrr4byslpmyKOtsMfi307y2FV3yC4jUMizyUnM0FW
TESQaGFbKGZkpntaYb6n0/08KhBiLJkQPwAqEasHpua8JLJ4JdC7ec3byrO2P/i0A60qJFOl7
5KCU8Icjk9+rxcZiJBAH34DyYsV15Bz3HY7vw2KTd9pa8YeV/fyjZlNSipSJ6B8eA655jy4y9
E0/NS7B31LTDAHuvuVPEGkG6ldl+zQcRwW4jjYIa0fo1vmDBDyh0nivQDW8WCIQTQSGkluUMP
+sdOPZcdzTn3BDGWwlSwVym5qJoCRBnZReONEi6bBSk/FXFvfH2Xsg/3M5CxVHcledDVcdEo+
q+3e8dEoCs4+QIUP3aLRX++suIjvG2ZUufKiZC48XTTysoNUGSdc0+WDrbH+h6FsMDPYeUa5O
guh1MwERdJCUFPraia3lxZ9p/XYb+JX9jrp1OWElSfhZscLrHOzkTQlGodIR/KZUDgDkalDCh
OT1tbuWiQsSHfaPJGX4cwhHSnECVh3UEmgCnXNwPdQVoIahj95eQPH2tXrh8M8nTmaHSY4U8l
NMCKffc6mvPCttng
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic]
[fuzzy]
X-Received-From: 212.227.126.131
Subject: [Axiom-developer] Small documentation issue
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.21
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 06 Apr 2017 10:41:27 -0000
Tim,
Just a small documentation issue.
This line appears to be duplicated in the PDF:
"Permutation is a domain which can be used to compute permutations. It
is also an implementation of Group category."
In books/bookvol10.3.pamphlet its at line 145509.
I assume you would prefer me to let you know about this by email, like
this, rather than cloning github and sending you a pull request?
One other thing:
Some of the diagrams have been expanded making them look blocky. the
original diagrams are in scalable (.svg) form so its easy to export
them, at other sizes, to .png or .gif (not .eps). However I think the
document would be more readable if the diagrams were not larger than
necessary. To my eye, a lot of skipping over big diagrams makes reading
harder (it would be even better if text flowed around diagrams). This is
a very minor thought and not worth spending much time on.
More generally, on the topic of documentation. It would be possible to
write a lot more about the group theory around these domains. For
instance, explanations of concepts like 'generators' and so on. The
information added here was intended to be the aspects that are not
easily found in maths textbooks. I do agree with some of your earlier
posts that you made about the potential benefit that Axiom could bring
to mathematics education, just the discipline it brings to having a
consistent notation across the whole subject seems enormously valuable
to me. However cramming an explanation of the whole of mathematics into
bookvol10.3.pamphlet seems a bit over ambitious to me so perhaps its
best not to try to explain everything?
Martin
From MAILER-DAEMON Thu Apr 06 07:08:52 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1cw5HY-0002cJ-1K
for mharc-axiom-developer@gnu.org; Thu, 06 Apr 2017 07:08:52 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:41538)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1cw5HV-0002cB-BY
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 07:08:50 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1cw5HT-0006it-7d
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 07:08:49 -0400
Received: from mail-wr0-x22f.google.com ([2a00:1450:400c:c0c::22f]:34716)
by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1cw5HS-0006ib-Tf
for axiom-developer@nongnu.org; Thu, 06 Apr 2017 07:08:47 -0400
Received: by mail-wr0-x22f.google.com with SMTP id t20so56154255wra.1
for ; Thu, 06 Apr 2017 04:08:46 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
h=mime-version:in-reply-to:references:from:date:message-id:subject:to
:cc; bh=UtNdX+UeVxLoJ4CsfG2fNS+RZd2YbTVnM9Td6XXx/oA=;
b=Cxjr+YoYq23Um0DwCtUPhYlDyQ4NJtufb3oJVcELhKUaEILd1LiVQBAMJF7B3E/gtB
0/eV/EU+73rM2WnrJoZSHjLv8Xq49gwxNU4odmKpri2zima1oh6WIbJSWGtypTMZc/dg
OLHl3akx3gBNjsJJF/5zFVE4XXCMVE/K5DKwcSlCgHuWskwghXCBzzUqnxIh//trg+A6
g/ZAOh9/l1O/+1hw/R8PIoz56a+IiVsa0c7i+peOvkYj6J4t5FhEXXEaevkqzgr7eZkH
VWbahz3dJIT3U5gSLdCTEYunkYM5n3BH4ZWKnJUQQ6u31kaH4WQ3cP7cKJL3B41fd5yw
qElg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:in-reply-to:references:from:date
:message-id:subject:to:cc;
bh=UtNdX+UeVxLoJ4CsfG2fNS+RZd2YbTVnM9Td6XXx/oA=;
b=iY6ICYSxkrlDaycIirdtLYCD1gP/+r3UN35KvBfS4hjZtoQZ7R7m4z4BjPfXhGfzqO
VZAbxtdS4WWjFqS2oZ5suUlB5sLy35BzbhmApVgomgpMPC/A6knwtyLBoBvHRAvBUDeJ
dxBJk6+xH0MzWaOVqh2jVaa3mzxZmHI4Bq2eGHZrep5lyzsm2hAXuolClT/+ss6mrU3O
Fiz2DNe1Hn3zs4SkIi1+DjgMlHMNXMQKKu4NLIAbDRJ/Xc5WRoRBeOlzipvWFMjdIMPh
+ls+Zmlys1lmV+nyDK2vYO846CQopTpwnb5o8XYa31B72YmK10cljkssrxc8jFlfYfZJ
TqCg==
X-Gm-Message-State: AFeK/H3vm4KQtoA5+RgNLMHdyVyklaCF2LQ7jrzUxF4FI5adGERURxGuFDBDXBvVXyGlmy4z31Xzga3+IjHtaw==
X-Received: by 10.28.87.6 with SMTP id l6mr23467494wmb.109.1491476925357; Thu,
06 Apr 2017 04:08:45 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.28.151.195 with HTTP; Thu, 6 Apr 2017 04:08:44 -0700 (PDT)
In-Reply-To: <1908790900.1855510.1491441879517@mail.yahoo.com>
References:
<1908790900.1855510.1491441879517@mail.yahoo.com>
From: Tim Daly
Date: Thu, 6 Apr 2017 07:08:44 -0400
Message-ID:
To: C Y ,
=?UTF-8?Q?Andr=C3=A9_Platzer?=
Cc: axiom-dev , Martin Baker ,
Tim Daly ,
Laurent Thery ,
Jeremy Avigad , Renaud Rioboo ,
Kurt Pagani , Frank Pfenning
Content-Type: multipart/alternative; boundary=001a1144222c53a6dc054c7d88cf
X-detected-operating-system: by eggs.gnu.org: Genre and OS details not
recognized.
X-Received-From: 2a00:1450:400c:c0c::22f
Subject: Re: [Axiom-developer] Proving Axiom Correct -- at the C level
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.21
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 06 Apr 2017 11:08:51 -0000
--001a1144222c53a6dc054c7d88cf
Content-Type: text/plain; charset=UTF-8
Yes, I'd like to have a solid "floor" to the proofs and the fewer layers,
the better.
An issue arises when looking to prove the propositions for the Domain
NonNegativeInteger (NNI). This is closely related to the 'nat' domain in
proof
systems. However, NNI relies on calls to Lisp for things like defining
equality. Lisp equality is a much-discussed question involving EQ, EQUAL,
etc. which eventually gets resolved down to the machione level. So no
matter which lisp is used, the machine gets involved it seems.
If I "misunderstand" Homotopy Type Theory there is an axiom of
"Univalence" which states that equality is equivalence. Given that,
it might be possible to establish a "floor" at the Spad level so we
do not even have to provide proofs of lisp and below. For me this
is an open research question.
I am still studying the HoTT work. I haven't seen it used for algorithms
like Groeber basis. There is some interesting work by Andre Platzer
which uses substituion as the basis of sound reasoning.
http://dx.doi.org/10.1007/s10817-016-9385-1
>From my limited understanding so far it appears to be similar to
Hoare triples on steroids. This might prove very useful for handling
imperative programs. Again, for me this is an open research question.
Here's some things he's been doing in the realm of real arithmetic
http://www.cs.cmu.edu/~aplatzer/pub/rwv.pdf
Generally, rigorously proving valid facts of first-order real arithmetic /
unsatisfiability
of a set of polynomial inequalities is quite important for his work. He
does some
nice things with Groeber basis.
I've collected the "category tower" in Axiom for NNI along with their
associated propositions. I'm trying to do something trivial by hand so
I can understand the research questions better. When I get an example
I'll post the results here.
Tim
On Wed, Apr 5, 2017 at 9:24 PM, C Y wrote:
> > On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly
> wrote:
> > I previously mentioned the "proof tower" approach to the question
> > of proving code at many different layers. Spad code proven in COQ,
> > Lisp code in ACL2, and Intel code in CCAs. The missing step in the
> > tower was C.
>
> Rather than introduce another complex language and proof problem into the
> stack, would it be possible to have Lisp implemented directly "on the
> metal"? If SBCL isn't the preferred approach to such a system, maybe the
> following project could be used as a starting point to put together a
> purpose built LISP?
>
> https://github.com/robert-strandh/SICL
>
> Maybe some of the open source "LISP as OS" projects could offer lower
> level primitives from which to build the boot strapping code, or a basic
> set could be defined in x86-64... I suppose it's academic at this point,
> but I can't help wondering if there would be simplicity gains in the
> "expressing and defining proof stacks" department that would make it
> worthwhile in the long run to hold the number of conceptual expression
> languages down to the minimum necessary.
>
> CY
>
--001a1144222c53a6dc054c7d88cf
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Yes, I'd like to have a solid "floor" to the proofs and the=
fewer layers, the better.

An issue arises when looking to pro=
ve the propositions for the Domain

NonNegativeInteger (NNI). This=
is closely related to the 'nat' domain in proof

systems. =
However, NNI relies on calls to Lisp for things like defining

equ=
ality. Lisp equality is a much-discussed question involving EQ, EQUAL,

<= /div>etc. which eventually gets resolved down to the machione level. So no =

matter which lisp is used, the machine gets involved it seems.

If I "misunderstand" Homotopy Type Theory there is an =
axiom of

"Univalence" which states that equality is equi=
valence. Given that,

it might be possible to establish a "flo=
or" at the Spad level so we

do not even have to provide proof=
s of lisp and below. For me this

I am still studying the HoTT work. I haven't =
seen it used for algorithms

like Groeber basis. There is some interesti= ng work by Andre Platzer

which uses substituion as the basis of sound r= easoning.

http://dx.doi.org/10.1007/s10817-016-93=
85-1

Here's some things he&#= 39;s been doing in the realm of real arithmetic

http://www.cs.cmu.e= du/~aplatzer/pub/rwv.pdf

Generally, rigorously proving valid facts of first-order real arithmetic / unsatisfiability

of a set of polynomial inequalities is quite=20 important for his work. He does some

--001a1144222c53a6dc054c7d88cf--
From MAILER-DAEMON Thu Apr 06 17:37:01 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1cwF5R-0005a7-GH
for mharc-axiom-developer@gnu.org; Thu, 06 Apr 2017 17:37:01 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:57807)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from > I previously= mentioned the "proof tower" approach to the question

> of proving co= de at many different layers. Spad code proven in COQ,

> Lisp code in = ACL2, and Intel code in CCAs. The missing step in the

> tower was C.<= br>

Rather than introduce another complex language and p=
roof problem into the stack, would it be possible to have Lisp implemented =
directly "on the metal"? If SBCL isn't the preferred approach to such=
a system, maybe the following project could be used as a starting point to=
put together a purpose built LISP?

Maybe some of the open source "LISP as OS=
" projects could offer lower level primitives from which to build the boot =
strapping code, or a basic set could be defined in x86-64... I suppos=
e it's academic at this point, but I can't help wondering if there would be=
simplicity gains in the "expressing and defining proof stacks" department =
that would make it worthwhile in the long run to hold the number of concept=
ual expression languages down to the minimum necessary.

CY

<= /div>etc. which eventually gets resolved down to the machione level. So no =

is an open research question=
.

like Groeber basis. There is some interesti= ng work by Andre Platzer

which uses substituion as the basis of sound r= easoning.

http://dx.doi.org/10.1007/s108

From my limited understanding so far it appears to b=
e similar to

Hoare triples on steroids. This might prove very=
useful for handling

imperative programs. Again, for me this =
is an open research question.

Here's some things he&#= 39;s been doing in the realm of real arithmetic

http://www.cs.cmu.e= du/~aplatzer/pub/rwv.pdf

Generally, rigorously proving valid facts of first-order real arithmetic / unsatisfiability

of a set of polynomial inequalities is quite=20 important for his work. He does some

nice things with Groeber=
basis.

I've collected the "category tower"=
in Axiom for NNI along with their

associated propositions. =
I'm trying to do something trivial by hand so

I can under=
stand the research questions better. When I get an example

I&=
#39;ll post the results here.

Tim

On Wed, Apr 5, 2017 at 9:24 PM, C Y <smustudent1@yahoo.com><=
/span> wrote:

> On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly <<= a href=3D"mailto:axiomcas@gmail.com" target=3D"_blank">axiomcas@gmail.com> wrote:

> I previously mentioned the "proof tower" ap= proach to the question

> of proving code at many different layers. Sp= ad code proven in COQ,

> Lisp code in ACL2, and Intel code in CCAs. T= he missing step in the

> tower was C.R= ather than introduce another complex language and proof problem into the st= ack, would it be possible to have Lisp implemented directly "on the me= tal"?=C2=A0 If SBCL isn't the preferred approach to such a system,= maybe the following project could be used as a starting point to put toget= her a purpose built LISP?Maybe some of the open sourc= e "LISP as OS" projects could offer lower level primitives from w= hich to build the boot strapping code, or a basic set could be defined in x= 86-64...=C2=A0 I suppose it's academic at this point, but I can't h= elp wondering if there would be simplicity gains in the "expressing an= d defining proof stacks" department that would make it worthwhile in t= he long run to hold the number of conceptual expression languages down to t= he minimum necessary.CY

I'll fix the duplicate line. Thanks for the bug report.

=

Any path that is convenient for reporting bugs is ok.=

The eps files live in books/ps with the convention that

=C2=A0=C2=A0=C2=A0 books/ps/v103*

are images in volume 10.3.=
Your images are

=C2=A0=C2=A0=C2=A0 books/ps/v103permgrpxx.ep=
s

where xx is a sequential number.

Alte=
rnatively, the pamphlet files are just raw latex. If you

cd t=
o the books directory you should be able to just do

=C2=A0=C2=
=A0 gcc -o tanglec tanglec.c

to get the tanglec program. You =
only need to do this once.

=C2=A0

=C2=A0=C2=A0=
./tanglec bookvolbib.pamphlet axiom.bib >axiom.bib

=C2=A0=
=C2=A0 latex bookvol10.3.pamphlet

=C2=A0=C2=A0 makeindex book=
vol10.3.idx

=C2=A0=C2=A0 bibtex bookvol10.3.aux

=C2=A0=C2=A0 latex bookvol10.3.pamphlet

=C2=A0=C2=A0 latex b=
ookvol10.3.pamphlet

=C2=A0=C2=A0 dvipdfm bookvol10.3.dvi

<= /div>

<= /div>

=C2=A0=C2=A0 evince bookvol10.3.pdf

Open a shel=
l to run the above commands in a bash script.

If you leave th=
e pdf viewer running it will update automatically

every time =
you remake the file. So you get a "hot loop' where

y=
ou change the pamphlet file, run the bash script, and see the

result immediately.

When you are happy with the changes =
you can do

=C2=A0=C2=A0 git diff books/bookvol10.3.pamphl=
et >patchfile

and send me the patch file.

re: too much informati=
on

The target audience is students. I'm about to be a visi=
tingTim

attract students to working with Axiom. Since these are CS

Volume 0, the Jenks book, in the ap=
propriate algebra location,

in the help files, in hyperdoc, a=
nd in the (as yet unpublished)

web pages.

S=
o there is a place somewhere in the system for documentation

=
at almost any level. Indeed, if all else seems inappropriate there

--94eb2c03c314e9aad1054c864e35--
can always be a new volume.

Tim