From MAILER-DAEMON Thu Dec 03 02:06:22 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kkih2-0000hG-Ob
for mharc-axiom-developer@gnu.org; Thu, 03 Dec 2020 02:06:22 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:51558)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kkigy-0000gh-9F
for axiom-developer@nongnu.org; Thu, 03 Dec 2020 02:06:17 -0500
Received: from mail-qt1-x82a.google.com ([2607:f8b0:4864:20::82a]:38236)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kkigw-0005FW-91
for axiom-developer@nongnu.org; Thu, 03 Dec 2020 02:06:15 -0500
Received: by mail-qt1-x82a.google.com with SMTP id o1so703204qtp.5
for ; Wed, 02 Dec 2020 23:06:13 -0800 (PST)
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
:content-transfer-encoding;
bh=cpIsmANJpIxNR6A4pZ8Pn4bimXXtXucCneYSaCawUIo=;
b=fm83cEpZbeU7Nr96fNHNtJiBYvp9bUiOZVWs6Bt6KEMhOYr2xMm1US+n6BFL/n4ZeR
OWhTuXTB57joOcU71zVQIynFE/siprp4gva7NfdkEnnIhzePbvrwtDPfQFsZonRHJXTq
45BGEBGUwNwf4CCxxIHRWqKIWolEkd1LwPkBgIySo0LumKf+Zp+hlLhqLzwJ5GeB627/
ISbOYQqcQisTrCP11/aDZDNIqnjzPzv+34x6Bi+YoK/zlf+mhN3T5tQQeaUrsSCfanQu
1MVNONhjgqQOpnm/ltsNQBxliZdCDsyrdH1VWaDkTWtiJg5N2QStDSTdfAjBYqnvZZL/
MBxg==
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:content-transfer-encoding;
bh=cpIsmANJpIxNR6A4pZ8Pn4bimXXtXucCneYSaCawUIo=;
b=Nup6K9/sdkbvL758rdOHnUmN/vboyViP3lsrvhw7UpHK2RTYMQSQoe8lK0+/1Ni6pY
U8M7IT+NSMpe0eYKJawCHVTF0GsqzdRJkSm7dumUH5HEZooLDMafL/oE9HGluJrw3Omy
4XvLD9wtgNSNmGA0Ev0ABbclMOqi00d0fAeo4zzw0dS5vPEZqviq8lN3CRSU5FW9gLmv
KU6kp/eJMSTC5ubjNSwhnjGiIPbNBwurSlInmQ/ex6ZtSInyJd+yaKZN4NPX8GItBMBp
9JCAxuPYh8qkmdvr5RuhLQFVAOdmSAkYMyc1NmLgWRQp7zQymqq4qc+/hjRKAH/sVlip
afZA==
X-Gm-Message-State: AOAM532mFd2lYBlRAvrsnb3jLTViDh6UycJMWlJX0MxqmlNZSZFdBgl5
oEGjTSaWDI5VJlS6L1Jxdh+PT9vyoGRxk6kdUVILW/OmxaM=
X-Google-Smtp-Source: ABdhPJwWvODaCt8A+ubYwD22mnK26jRVNqFx/ST0l7hQl5anUVTg8AJqx9JDIPMR7Ad/ItQkgwyNbJUV7TGRJdyRHN8=
X-Received: by 2002:ac8:6994:: with SMTP id o20mr2020707qtq.188.1606979172303;
Wed, 02 Dec 2020 23:06:12 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:b6d2:0:0:0:0:0 with HTTP;
Wed, 2 Dec 2020 23:06:11 -0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
From: Tim Daly
Date: Thu, 3 Dec 2020 02:06:11 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , axiomcas@gmail.com
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Received-SPF: pass client-ip=2607:f8b0:4864:20::82a;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x82a.google.com
X-Spam_score_int: 0
X-Spam_score: -0.1
X-Spam_bar: /
X-Spam_report: (-0.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001,
URI_DOTEDU=1.999 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 03 Dec 2020 07:06:18 -0000
I just ran across an interesting example about the difference
between testing and proving (not that I need to be convinced).
http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.p=
df
(page 10):
On day one, our mathematician finds out using a formal computation software
that
\int{\sin(t)/t}{dt} =3D \pt/2
On day two, he tries to play around a bit with such formulas and finds out =
that
\int{(\sin(t)/t) (\sin(t/101)/(t/101)}{dt} =3D \p2/2
On day three, he thinks maybe a pattern could emerge and discovers that
\int{(\sin(t)/t) (\sin(t/101)/(t/101) (\sin(t/201)/(t/201))}{dt} =3D \p2/2
On day four, he gets quite confident and conjectures that, for every n=E2=
=88=88N,
\int{\prod{ /sin(t/(100n+1)) / (t/(100n+1))}{dt} =3D \pi/2
In fact, the conjecture breaks starting at
n=3D 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889
and none of the usual tests would have found this out.
Tim
On 11/29/20, Tim Daly wrote:
> Axiom, as it was released to me long ago, is being
> overtaken by current technology.
>
> I'm taking an MIT course on "Underactuated Robots" [0]
> (I spent a large portion of my life doing robotics).
>
> The instructor is using Jupyter notebooks to illustrate
> control algorithms. He is doing computation and
> showing the graphics in a single notebook. Axiom
> could "almost" do that in the 1980s.
>
> It is clear that, with a sufficiently rich set of algorithms,
> such as one finds in CoCalc, Axiom is showing its age.
>
> This is the primary reason why I consider the SANE
> research effort vital. An Axiom system that has
> proven algorithms, follows knowledge from leading
> mathematics (e.g. Category Theory), and pushes the
> state of the art will keep Axiom alive and relevant.
>
> Axiom was, and is, research software. Just doing
> "more of the same" goes nowhere slowly. Following
> that path leads to the dustbin of history.
>
> Tim
>
> [0]
> https://www.youtube.com/watch?v=3DGPvw92IKO44&list=3DUUhfUOAhz7ynELF-s_1L=
PpWg&index=3D28
>
>
>
> On 11/27/20, Tim Daly wrote:
>> The current mental struggle involves properly re-constructing
>> Axiom so Category Theory (e.g. objects, morphisms, identity,
>> and composition) is respected between the domains. Done
>> properly, this should make resolving type coercion and
>> conversion less ad-hoc. This is especially important when
>> dealing with first-class dependent types.
>>
>> Axiom categories and domains, in the SANE model, compile
>> to lisp classes. These classes are "objects" in the Category
>> Theory sense. Within a given category or domain, the
>> representation (aka, the "carrier" in type theory) is an
>> "object" (in Category Theory) and most functions are
>> morphisms from Rep to Rep. Coercions are functors,
>> which need to conform to the Category Theory properties.
>>
>> It also raises the interesting question of making Rep
>> be its own class. This allows, for example, constructing
>> the polynomial domain with the Rep as a parameter.
>> Thus you get sparse, recursive, or dense polynomials
>> by specifying different Rep classes. This is even more
>> interesting when playing with Rep for things like
>> Clifford algebras.
>>
>> It is quite a struggle to unify Category Theory, Type
>> Theory, Programming, Computer Algebra, and Proof
>> Theory so "it all just works as expected". Progress is
>> being made, although not quickly.
>>
>> For those who want to play along I can recommend the
>> MIT course in Category Theory [0] and the paper on
>> The Type Theory of Lean [1]. For the programming
>> aspects, look at The Art of the Metaobject Protocol [2].
>>
>> [0] https://www.youtube.com/user/youdsp/playlists
>> [1]
>> https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.=
pdf
>> [2] https://mitpress.mit.edu/books/art-metaobject-protocol
>>
>> Tim
>>
>>
>> On 11/10/20, Tim Daly wrote:
>>> Another area that is taking a great deal of time and effort
>>> is choosing a code architecture that has a solid background
>>> in research.
>>>
>>> Axiom used CLU and Group Theory as two scaffolds to
>>> guide design choices, making it possible to argue whether
>>> and where a domain should be structured and where it
>>> should occur in the system.
>>>
>>> Axiom uses a Pratt-parser scheme. This allows the
>>> ability to define and change syntax by playing with the
>>> LED and NUD numeric values. It works but it is not
>>> very clear or easy to maintain.
>>>
>>> An alternative under consideration is Hutton and Meijer's
>>> Monadic Parser Combinators. This constructs parser
>>> functions and combines them in higher order functions.
>>> It is strongly typed. It provides a hierarchy of functions
>>> that would allow the parser to be abstracted at many
>>> levels, making explanations clearer.
>>>
>>> Ideally the structure of the new parser should be clear,
>>> easy to maintain, and robust under changes. Since SANE
>>> is a research effort, maximum flexibility is ideal.
>>>
>>> Since SANE is intended to be easily maintained, it is
>>> important that the compiler / interpreter structure be
>>> clear and consistent. This is especially important as
>>> questions of which proof language syntax and a
>>> specification language syntax is not yet decided.
>>>
>>> Tim
>>>
>>>
>>>
>>>
>>> On 10/9/20, Tim Daly wrote:
>>>> A great deal of thought has gone into the representation
>>>> of functions in the SANE version.
>>>>
>>>> It is important that a function lives within an environment.
>>>> There are no "stand alone" functions. Given a function
>>>> its environment contains the representation which itself
>>>> is a function type with accessor functions. Wrapped
>>>> around these is the domain type containing other
>>>> functions. The domain type lives within several
>>>> preorders of environments, some dictated by the
>>>> structure of group theory, some dictated by the structure
>>>> of the logic.
>>>>
>>>> Lisp has the ability to construct arbitrary structures
>>>> which can be nested or non-nested, and even potentially
>>>> circular.
>>>>
>>>> Even more interesting is that these structures can be
>>>> "self modified" so that one could have a domain (e.g.
>>>> genetic algorithms) that self-adapt, based on input.
>>>> Or "AI" domains, representated as weight matrices,
>>>> that self-adapt to input by changing weights.
>>>>
>>>> Ultimately the goal of the representation should be that,
>>>> given a function, it should be possible to traverse the
>>>> whole of the environment using a small, well-defined
>>>> set of well-typed structure walkers.
>>>>
>>>> All of this is easy to write down in Lisp.
>>>> The puzzle is how to reflect these ideas in Spad.
>>>>
>>>> Currently the compiler translates all of the Spad
>>>> code to Lisp objects so the Spad->Lisp conversion
>>>> is easy. Lisp->Spad is also easy for things that have
>>>> a surface representation in Spad. But, in general,
>>>> Lisp->Spad is only a partial function, and somewhat
>>>> limited at that.
>>>>
>>>> I suspect that the solution will allow some domains
>>>> to be pure Lisp and others will allow in-line Lisp.
>>>>
>>>> Most of these ideas are nearly impossible to even
>>>> think about in other languages or, if attempted,
>>>> fall afoul of Greenspun's Tenth Rule, to wit:
>>>>
>>>> "Any sufficiently complicated C or Fortran program
>>>> contains an ad hoc, informally-specified, bug-ridden,
>>>> slow implementation of half of Common Lisp."
>>>>
>>>> Fortunately Spad is only a domain specific language
>>>> on top of Lisp. Once past the syntax level it is Lisp
>>>> all the way down.
>>>>
>>>> Tim
>>>>
>>>
>>
>
From MAILER-DAEMON Thu Dec 03 02:49:19 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kkjMd-0001Pa-Rt
for mharc-axiom-developer@gnu.org; Thu, 03 Dec 2020 02:49:19 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:60660)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kkjMc-0001PR-G2
for axiom-developer@nongnu.org; Thu, 03 Dec 2020 02:49:18 -0500
Received: from mail-qk1-x72f.google.com ([2607:f8b0:4864:20::72f]:40636)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kkjMX-00039y-10
for axiom-developer@nongnu.org; Thu, 03 Dec 2020 02:49:14 -0500
Received: by mail-qk1-x72f.google.com with SMTP id y197so1305749qkb.7
for ; Wed, 02 Dec 2020 23:49:12 -0800 (PST)
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
:content-transfer-encoding;
bh=OekpRRvQ2HvyFaaaGcussyA3Jya0mlp0GYZG5oBmL/Q=;
b=Id1hXOlW5JG2ZrZSbu77MfG+a2QE/JHmZMw1eXiCeuV/6PUqvIU8SUfjtChSqXhmPw
rzkbU322ZrElezzVpth6VynlOs/QWmwl0APcVqnY/f7Lb3mGbBC3HTK2rnMeSirNnqaD
RWzpKXM/V5NIYOj/CRmgXbP6y+7KTiC71p/E2R7dKtEsEtckrJa8NfIhjuPXMqRFzX5A
EpdgooIS9zJAsDri1wpN5UAuyrVHJsjeqgmOseOSIhFyiWqa9g328a5XrWXdZAPBozWJ
vypZK1vdbBRpHt1YOrBJqMYJAdWtrPxyQRoVFWuwd0z/CQgkCVKbhSGRrAIEFfpdEfh0
QT6w==
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:content-transfer-encoding;
bh=OekpRRvQ2HvyFaaaGcussyA3Jya0mlp0GYZG5oBmL/Q=;
b=eW30N7gknVxoCeLTvoJ5OZNPmSAnVXZHmUuZxpjlgf9CxsQAq5RSg8cxO6ViA8dMHm
GrmNSbLV174R3Mh37o31Jf8KLvpBU//slQfXnExRUWYlHuGcWFcsGzrxYyaO+Z6ptO0h
SBd9GP+zXc3bt8b+zWCMquUdzNy4uQ9OHsTkvdQaJQmXiXHIPoU4s+5PimCdO88dva7P
0y/hBLjd+2Nljbc3P/YYdqdVijKIJO750drAYAeg6uJ33O2O1oqrmMarEyRZDF/mAtgB
UQT9/n1A77vSMkKYrETcqonCYcOQKh9vUJ6cZebEB/EdOMuQ7zskS72ARls5vvQJuW4E
KoKg==
X-Gm-Message-State: AOAM532wIdTYr0fRU3XMyhGdH99rccXEo9C5n3UMfUE9eRWyP9SNrP5D
6pt3VTIDO4Ljeu0L5khM5ihKeeAXj2DZ7gLj/XdOekDmBe0=
X-Google-Smtp-Source: ABdhPJzRS1si3/0Ydrb+i8ydz+jdoIRafY6ZRhBJ0a9V9EK8CM2UygwtgJOt7yaWl/UscGRH8EurQJ2V+i4xRfWV0nE=
X-Received: by 2002:a05:620a:40d6:: with SMTP id
g22mr1710747qko.232.1606981751755;
Wed, 02 Dec 2020 23:49:11 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:b6d2:0:0:0:0:0 with HTTP;
Wed, 2 Dec 2020 23:49:10 -0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
From: Tim Daly
Date: Thu, 3 Dec 2020 02:49:10 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , axiomcas@gmail.com
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Received-SPF: pass client-ip=2607:f8b0:4864:20::72f;
envelope-from=axiomcas@gmail.com; helo=mail-qk1-x72f.google.com
X-Spam_score_int: 0
X-Spam_score: -0.1
X-Spam_bar: /
X-Spam_report: (-0.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001,
URI_DOTEDU=1.999 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 03 Dec 2020 07:49:18 -0000
HILL CLIMBING
I really encourage you to read the slides:
Vladimir Voevodsky. Univalent foundations, March 2014. Presentation at
IAS,http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/201=
4_IAS.pdf
The mathematical references likely won't make sense but the
most important point of the article will. He found mistakes in
work he and others did. Since these people were famous their
work was never really checked (fortunately that's not my issue).
quoting from the slide 28:
I now do my mathematics with a proof assistant and do not have to worry
all the time about mistakes in my arguments or about how to convince
others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with the
program remains. Sooner or later computer proof assistants will become
the norm, but the longer this process takes the more misery associated
with mistakes and with unnecessary self-verification the practitioners of t=
he
field will have to endure.
Of all of the software created, computer algebra seems like the most
reasonable place to apply proof techniques. My feeling is that computer
algebra is still 19th century, pre-formal mathematics. We can do better.
We must. And as a consequence we elevate "computer algebra" to
"computational mathematics", surely a worthwhile research goal.
Tim
On 12/3/20, Tim Daly wrote:
> I just ran across an interesting example about the difference
> between testing and proving (not that I need to be convinced).
> http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course=
.pdf
> (page 10):
>
>
> On day one, our mathematician finds out using a formal computation softwa=
re
> that
>
> \int{\sin(t)/t}{dt} =3D \pt/2
>
> On day two, he tries to play around a bit with such formulas and finds ou=
t
> that
>
> \int{(\sin(t)/t) (\sin(t/101)/(t/101)}{dt} =3D \p2/2
>
> On day three, he thinks maybe a pattern could emerge and discovers that
>
> \int{(\sin(t)/t) (\sin(t/101)/(t/101) (\sin(t/201)/(t/201))}{dt} =3D \p2/=
2
>
> On day four, he gets quite confident and conjectures that, for every n=E2=
=88=88N,
>
> \int{\prod{ /sin(t/(100n+1)) / (t/(100n+1))}{dt} =3D \pi/2
>
>
> In fact, the conjecture breaks starting at
>
> n=3D 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889
>
> and none of the usual tests would have found this out.
>
> Tim
>
>
>
> On 11/29/20, Tim Daly wrote:
>> Axiom, as it was released to me long ago, is being
>> overtaken by current technology.
>>
>> I'm taking an MIT course on "Underactuated Robots" [0]
>> (I spent a large portion of my life doing robotics).
>>
>> The instructor is using Jupyter notebooks to illustrate
>> control algorithms. He is doing computation and
>> showing the graphics in a single notebook. Axiom
>> could "almost" do that in the 1980s.
>>
>> It is clear that, with a sufficiently rich set of algorithms,
>> such as one finds in CoCalc, Axiom is showing its age.
>>
>> This is the primary reason why I consider the SANE
>> research effort vital. An Axiom system that has
>> proven algorithms, follows knowledge from leading
>> mathematics (e.g. Category Theory), and pushes the
>> state of the art will keep Axiom alive and relevant.
>>
>> Axiom was, and is, research software. Just doing
>> "more of the same" goes nowhere slowly. Following
>> that path leads to the dustbin of history.
>>
>> Tim
>>
>> [0]
>> https://www.youtube.com/watch?v=3DGPvw92IKO44&list=3DUUhfUOAhz7ynELF-s_1=
LPpWg&index=3D28
>>
>>
>>
>> On 11/27/20, Tim Daly wrote:
>>> The current mental struggle involves properly re-constructing
>>> Axiom so Category Theory (e.g. objects, morphisms, identity,
>>> and composition) is respected between the domains. Done
>>> properly, this should make resolving type coercion and
>>> conversion less ad-hoc. This is especially important when
>>> dealing with first-class dependent types.
>>>
>>> Axiom categories and domains, in the SANE model, compile
>>> to lisp classes. These classes are "objects" in the Category
>>> Theory sense. Within a given category or domain, the
>>> representation (aka, the "carrier" in type theory) is an
>>> "object" (in Category Theory) and most functions are
>>> morphisms from Rep to Rep. Coercions are functors,
>>> which need to conform to the Category Theory properties.
>>>
>>> It also raises the interesting question of making Rep
>>> be its own class. This allows, for example, constructing
>>> the polynomial domain with the Rep as a parameter.
>>> Thus you get sparse, recursive, or dense polynomials
>>> by specifying different Rep classes. This is even more
>>> interesting when playing with Rep for things like
>>> Clifford algebras.
>>>
>>> It is quite a struggle to unify Category Theory, Type
>>> Theory, Programming, Computer Algebra, and Proof
>>> Theory so "it all just works as expected". Progress is
>>> being made, although not quickly.
>>>
>>> For those who want to play along I can recommend the
>>> MIT course in Category Theory [0] and the paper on
>>> The Type Theory of Lean [1]. For the programming
>>> aspects, look at The Art of the Metaobject Protocol [2].
>>>
>>> [0] https://www.youtube.com/user/youdsp/playlists
>>> [1]
>>> https://github.com/digama0/lean-type-theory/releases/download/v1.0/main=
.pdf
>>> [2] https://mitpress.mit.edu/books/art-metaobject-protocol
>>>
>>> Tim
>>>
>>>
>>> On 11/10/20, Tim Daly wrote:
>>>> Another area that is taking a great deal of time and effort
>>>> is choosing a code architecture that has a solid background
>>>> in research.
>>>>
>>>> Axiom used CLU and Group Theory as two scaffolds to
>>>> guide design choices, making it possible to argue whether
>>>> and where a domain should be structured and where it
>>>> should occur in the system.
>>>>
>>>> Axiom uses a Pratt-parser scheme. This allows the
>>>> ability to define and change syntax by playing with the
>>>> LED and NUD numeric values. It works but it is not
>>>> very clear or easy to maintain.
>>>>
>>>> An alternative under consideration is Hutton and Meijer's
>>>> Monadic Parser Combinators. This constructs parser
>>>> functions and combines them in higher order functions.
>>>> It is strongly typed. It provides a hierarchy of functions
>>>> that would allow the parser to be abstracted at many
>>>> levels, making explanations clearer.
>>>>
>>>> Ideally the structure of the new parser should be clear,
>>>> easy to maintain, and robust under changes. Since SANE
>>>> is a research effort, maximum flexibility is ideal.
>>>>
>>>> Since SANE is intended to be easily maintained, it is
>>>> important that the compiler / interpreter structure be
>>>> clear and consistent. This is especially important as
>>>> questions of which proof language syntax and a
>>>> specification language syntax is not yet decided.
>>>>
>>>> Tim
>>>>
>>>>
>>>>
>>>>
>>>> On 10/9/20, Tim Daly wrote:
>>>>> A great deal of thought has gone into the representation
>>>>> of functions in the SANE version.
>>>>>
>>>>> It is important that a function lives within an environment.
>>>>> There are no "stand alone" functions. Given a function
>>>>> its environment contains the representation which itself
>>>>> is a function type with accessor functions. Wrapped
>>>>> around these is the domain type containing other
>>>>> functions. The domain type lives within several
>>>>> preorders of environments, some dictated by the
>>>>> structure of group theory, some dictated by the structure
>>>>> of the logic.
>>>>>
>>>>> Lisp has the ability to construct arbitrary structures
>>>>> which can be nested or non-nested, and even potentially
>>>>> circular.
>>>>>
>>>>> Even more interesting is that these structures can be
>>>>> "self modified" so that one could have a domain (e.g.
>>>>> genetic algorithms) that self-adapt, based on input.
>>>>> Or "AI" domains, representated as weight matrices,
>>>>> that self-adapt to input by changing weights.
>>>>>
>>>>> Ultimately the goal of the representation should be that,
>>>>> given a function, it should be possible to traverse the
>>>>> whole of the environment using a small, well-defined
>>>>> set of well-typed structure walkers.
>>>>>
>>>>> All of this is easy to write down in Lisp.
>>>>> The puzzle is how to reflect these ideas in Spad.
>>>>>
>>>>> Currently the compiler translates all of the Spad
>>>>> code to Lisp objects so the Spad->Lisp conversion
>>>>> is easy. Lisp->Spad is also easy for things that have
>>>>> a surface representation in Spad. But, in general,
>>>>> Lisp->Spad is only a partial function, and somewhat
>>>>> limited at that.
>>>>>
>>>>> I suspect that the solution will allow some domains
>>>>> to be pure Lisp and others will allow in-line Lisp.
>>>>>
>>>>> Most of these ideas are nearly impossible to even
>>>>> think about in other languages or, if attempted,
>>>>> fall afoul of Greenspun's Tenth Rule, to wit:
>>>>>
>>>>> "Any sufficiently complicated C or Fortran program
>>>>> contains an ad hoc, informally-specified, bug-ridden,
>>>>> slow implementation of half of Common Lisp."
>>>>>
>>>>> Fortunately Spad is only a domain specific language
>>>>> on top of Lisp. Once past the syntax level it is Lisp
>>>>> all the way down.
>>>>>
>>>>> Tim
>>>>>
>>>>
>>>
>>
>
From MAILER-DAEMON Fri Dec 04 10:05:12 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1klCdz-0006Dt-VT
for mharc-axiom-developer@gnu.org; Fri, 04 Dec 2020 10:05:11 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:35140)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1klCdy-0006DQ-Da
for axiom-developer@nongnu.org; Fri, 04 Dec 2020 10:05:10 -0500
Received: from cs2.eticomm.net ([199.254.123.10]:51533
helo=mail.host.eticomm.net)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_CBC_SHA1:256)
(Exim 4.90_1) (envelope-from )
id 1klCdw-00016Q-Vh
for axiom-developer@nongnu.org; Fri, 04 Dec 2020 10:05:10 -0500
Received: from steadfastness ([96.248.111.8]) by cs2.eticomm.net with
MailEnable ESMTPA; Fri, 4 Dec 2020 09:54:58 -0500
Received: from camm by steadfastness with local (Exim 4.92)
(envelope-from )
id 1klCU6-0000eV-TM; Fri, 04 Dec 2020 09:54:58 -0500
From: Camm Maguire
To: Tim Daly ,camm@maguirefamily.org
Cc: axiom-developer@nongnu.org
Subject: Re: GCL failure to build
References:
Date: Fri, 04 Dec 2020 09:54:58 -0500
In-Reply-To:
(Tim Daly's message of "Fri, 2 Oct 2020 20:52:18 -0400")
Message-ID: <87v9dhsjst.fsf@maguirefamily.org>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain
Received-SPF: none client-ip=199.254.123.10;
envelope-from=camm@maguirefamily.org; helo=mail.host.eticomm.net
X-Spam_score_int: -14
X-Spam_score: -1.5
X-Spam_bar: -
X-Spam_report: (-1.5 / 5.0 requ) BAYES_00=-1.9, KHOP_HELO_FCRDNS=0.399,
SPF_HELO_NONE=0.001, SPF_NONE=0.001 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Fri, 04 Dec 2020 15:05:10 -0000
Greetings! Thanks for your report!
Please disregard my earlier advice to install readline. You seem to
have one, though it appears unusual.
A quick workaround for you instead should be to add --disable-readline
to ./configure
As a more permanent fix, please refresh Version_2_6_13pre from git and
please tell me if the problem persists.
Take care,
Tim Daly writes:
> I did a git clone git://git.sv.gnu.org/gcl.git
> cd gcl/gcl
> ./configure
> make
>
> ... and it failed on Ubuntu 1404 and 2020.04
>
> The failing console is attached.
>
> Tim
>
>
--
Camm Maguire camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
From MAILER-DAEMON Wed Dec 09 22:36:45 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1knCl3-0006AC-6Q
for mharc-axiom-developer@gnu.org; Wed, 09 Dec 2020 22:36:45 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:35176)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1knCl1-00069X-Lz
for axiom-developer@nongnu.org; Wed, 09 Dec 2020 22:36:43 -0500
Received: from mail-qt1-x836.google.com ([2607:f8b0:4864:20::836]:43642)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1knCkz-0003Fb-DM
for axiom-developer@nongnu.org; Wed, 09 Dec 2020 22:36:43 -0500
Received: by mail-qt1-x836.google.com with SMTP id k4so2737096qtj.10
for ; Wed, 09 Dec 2020 19:36:40 -0800 (PST)
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
:content-transfer-encoding;
bh=88vpWFar7NKNWAUarBvfvu9c5xEVj4JG1lY2NsM0kzE=;
b=pwHBCu9Mu3rlWOYgvotjWXycwV2PhdgB0AOWxGuNFO05RhNnO7PQ2aiIUX9HHjyWKu
Tv4nXhTFbN9kievf4Cj1LFxTTPlnnq1xfYRmGXBUDX7asVZJ+JK0wvXRfNaiME+Vx9tO
UvODgeQFRJJvXieAnDDl0B9ZVQoM9S/7MzinRBhk8xFOnVmUu3HKcFPsd8HC9A+X6PXN
qhaZ3kyxCZD10I7TCjvt9yODP72qIxrZCqZI/8LR4KbKGtTKacdxlIMicaD+Y44tWBTI
CLbAczr1vQSRgDL8Yl+6naBD4uDDp9V7251RtBiK8WxwnM+Mh49v2cod7jXvBaiAv77p
0f5w==
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:content-transfer-encoding;
bh=88vpWFar7NKNWAUarBvfvu9c5xEVj4JG1lY2NsM0kzE=;
b=jru12Gel1c4naHRml5OdcUGdms5ACvVdydmahMa9m8gNY8dP80LJGgAChEKfUn7swk
0cqGZEV5XcGp+ZGtseF0Brx3ItY3yReg9CPtP7NG7cV+mgh32uipqZITPynC3m3016rI
h//V1g4SzHuLPdhXUjXFR4voS6LfxdleZISkYwz9o/w7fmmo4w61PhUNRUIu2Tp2xrDd
5irQVB5u0ONPGPCEpAq1jjSJCiRvYsUndLv602om1OnDtPKQoSiptNBJxrVTYbw5BZhc
2vwCqpzMgsisPoD+k0CURUMfpM/Fp5q3skUWKG0Qq0HQv03gg635XnaDFDVG328baCXh
Undw==
X-Gm-Message-State: AOAM5304ODBqCfevBUK1bsPCkAVyeMH9J31ybxksZZrSWOXKPEAuYRq/
btyYD/OGNjv8oNyqNtVsXyVPTF8G9e9KfUocebra3EaC2ho=
X-Google-Smtp-Source: ABdhPJzcWlZi1c7VyQq2kDDueK3ErjF05HWdjaRGIz530WNyxQB7QTPVVBRk98A+7o6MUZI1XB7Vz4c9MYZhvmfAHBw=
X-Received: by 2002:ac8:5450:: with SMTP id d16mr6560836qtq.33.1607571399655;
Wed, 09 Dec 2020 19:36:39 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:b6d2:0:0:0:0:0 with HTTP;
Wed, 9 Dec 2020 19:36:38 -0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
From: Tim Daly
Date: Wed, 9 Dec 2020 22:36:38 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , axiomcas@gmail.com,
Prof Robert Harper
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Received-SPF: pass client-ip=2607:f8b0:4864:20::836;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x836.google.com
X-Spam_score_int: 0
X-Spam_score: -0.1
X-Spam_bar: /
X-Spam_report: (-0.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001,
URI_DOTEDU=1.999 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 10 Dec 2020 03:36:43 -0000
Robert Harper's "Holy Trinity" of Computer Science
(aka "Computational Trinitarianism")
Proof Theory
(Logic)
/ \
/ \
Category Theory ---- Type Theory
(Mathematics) (Programming)
There is a correspondence between Proof Theory,
Category Theory, and Type Theory or equivalently
a correspondence of Logic, Mathematics, and
Programming.
A concept may arise in, say, programming or
the same concept can arise in mathematics or
logic.
"You don't know what you are talking about until
you understand it all three ways."
(https://www.cs.uoregon.edu/research/summerschool/summer12/videos/Harper1_0=
.mp4)
This is essentially the research goal of the SANE version
of Axiom. The goal is to unify computational mathematics
in one system. The current effort is cleaning up things like
proper functors (category theory), adding proofs for
programs (proof theory) and implementing fully-first
class dependent types (type theory).
Harper's Holy Trinity gives a sound way of thinking about
various design decisions in the SANE version of Axiom.
Progress, albeit glacial, is being made.
Tim
On 12/3/20, Tim Daly wrote:
> HILL CLIMBING
>
> I really encourage you to read the slides:
> Vladimir Voevodsky. Univalent foundations, March 2014. Presentation at
> IAS,http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2=
014_IAS.pdf
>
> The mathematical references likely won't make sense but the
> most important point of the article will. He found mistakes in
> work he and others did. Since these people were famous their
> work was never really checked (fortunately that's not my issue).
>
> quoting from the slide 28:
>
> I now do my mathematics with a proof assistant and do not have to worry
> all the time about mistakes in my arguments or about how to convince
> others that my arguments are correct.
>
> But I think that the sense of urgency that pushed me to hurry with the
> program remains. Sooner or later computer proof assistants will become
> the norm, but the longer this process takes the more misery associated
> with mistakes and with unnecessary self-verification the practitioners of
> the
> field will have to endure.
>
>
>
>
> Of all of the software created, computer algebra seems like the most
> reasonable place to apply proof techniques. My feeling is that computer
> algebra is still 19th century, pre-formal mathematics. We can do better.
> We must. And as a consequence we elevate "computer algebra" to
> "computational mathematics", surely a worthwhile research goal.
>
> Tim
>
>
> On 12/3/20, Tim Daly wrote:
>> I just ran across an interesting example about the difference
>> between testing and proving (not that I need to be convinced).
>> http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/cours=
e.pdf
>> (page 10):
>>
>>
>> On day one, our mathematician finds out using a formal computation
>> software
>> that
>>
>> \int{\sin(t)/t}{dt} =3D \pt/2
>>
>> On day two, he tries to play around a bit with such formulas and finds
>> out
>> that
>>
>> \int{(\sin(t)/t) (\sin(t/101)/(t/101)}{dt} =3D \p2/2
>>
>> On day three, he thinks maybe a pattern could emerge and discovers that
>>
>> \int{(\sin(t)/t) (\sin(t/101)/(t/101) (\sin(t/201)/(t/201))}{dt} =3D \p2=
/2
>>
>> On day four, he gets quite confident and conjectures that, for every n=
=E2=88=88N,
>>
>> \int{\prod{ /sin(t/(100n+1)) / (t/(100n+1))}{dt} =3D \pi/2
>>
>>
>> In fact, the conjecture breaks starting at
>>
>> n=3D 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889
>>
>> and none of the usual tests would have found this out.
>>
>> Tim
>>
>>
>>
>> On 11/29/20, Tim Daly wrote:
>>> Axiom, as it was released to me long ago, is being
>>> overtaken by current technology.
>>>
>>> I'm taking an MIT course on "Underactuated Robots" [0]
>>> (I spent a large portion of my life doing robotics).
>>>
>>> The instructor is using Jupyter notebooks to illustrate
>>> control algorithms. He is doing computation and
>>> showing the graphics in a single notebook. Axiom
>>> could "almost" do that in the 1980s.
>>>
>>> It is clear that, with a sufficiently rich set of algorithms,
>>> such as one finds in CoCalc, Axiom is showing its age.
>>>
>>> This is the primary reason why I consider the SANE
>>> research effort vital. An Axiom system that has
>>> proven algorithms, follows knowledge from leading
>>> mathematics (e.g. Category Theory), and pushes the
>>> state of the art will keep Axiom alive and relevant.
>>>
>>> Axiom was, and is, research software. Just doing
>>> "more of the same" goes nowhere slowly. Following
>>> that path leads to the dustbin of history.
>>>
>>> Tim
>>>
>>> [0]
>>> https://www.youtube.com/watch?v=3DGPvw92IKO44&list=3DUUhfUOAhz7ynELF-s_=
1LPpWg&index=3D28
>>>
>>>
>>>
>>> On 11/27/20, Tim Daly wrote:
>>>> The current mental struggle involves properly re-constructing
>>>> Axiom so Category Theory (e.g. objects, morphisms, identity,
>>>> and composition) is respected between the domains. Done
>>>> properly, this should make resolving type coercion and
>>>> conversion less ad-hoc. This is especially important when
>>>> dealing with first-class dependent types.
>>>>
>>>> Axiom categories and domains, in the SANE model, compile
>>>> to lisp classes. These classes are "objects" in the Category
>>>> Theory sense. Within a given category or domain, the
>>>> representation (aka, the "carrier" in type theory) is an
>>>> "object" (in Category Theory) and most functions are
>>>> morphisms from Rep to Rep. Coercions are functors,
>>>> which need to conform to the Category Theory properties.
>>>>
>>>> It also raises the interesting question of making Rep
>>>> be its own class. This allows, for example, constructing
>>>> the polynomial domain with the Rep as a parameter.
>>>> Thus you get sparse, recursive, or dense polynomials
>>>> by specifying different Rep classes. This is even more
>>>> interesting when playing with Rep for things like
>>>> Clifford algebras.
>>>>
>>>> It is quite a struggle to unify Category Theory, Type
>>>> Theory, Programming, Computer Algebra, and Proof
>>>> Theory so "it all just works as expected". Progress is
>>>> being made, although not quickly.
>>>>
>>>> For those who want to play along I can recommend the
>>>> MIT course in Category Theory [0] and the paper on
>>>> The Type Theory of Lean [1]. For the programming
>>>> aspects, look at The Art of the Metaobject Protocol [2].
>>>>
>>>> [0] https://www.youtube.com/user/youdsp/playlists
>>>> [1]
>>>> https://github.com/digama0/lean-type-theory/releases/download/v1.0/mai=
n.pdf
>>>> [2] https://mitpress.mit.edu/books/art-metaobject-protocol
>>>>
>>>> Tim
>>>>
>>>>
>>>> On 11/10/20, Tim Daly wrote:
>>>>> Another area that is taking a great deal of time and effort
>>>>> is choosing a code architecture that has a solid background
>>>>> in research.
>>>>>
>>>>> Axiom used CLU and Group Theory as two scaffolds to
>>>>> guide design choices, making it possible to argue whether
>>>>> and where a domain should be structured and where it
>>>>> should occur in the system.
>>>>>
>>>>> Axiom uses a Pratt-parser scheme. This allows the
>>>>> ability to define and change syntax by playing with the
>>>>> LED and NUD numeric values. It works but it is not
>>>>> very clear or easy to maintain.
>>>>>
>>>>> An alternative under consideration is Hutton and Meijer's
>>>>> Monadic Parser Combinators. This constructs parser
>>>>> functions and combines them in higher order functions.
>>>>> It is strongly typed. It provides a hierarchy of functions
>>>>> that would allow the parser to be abstracted at many
>>>>> levels, making explanations clearer.
>>>>>
>>>>> Ideally the structure of the new parser should be clear,
>>>>> easy to maintain, and robust under changes. Since SANE
>>>>> is a research effort, maximum flexibility is ideal.
>>>>>
>>>>> Since SANE is intended to be easily maintained, it is
>>>>> important that the compiler / interpreter structure be
>>>>> clear and consistent. This is especially important as
>>>>> questions of which proof language syntax and a
>>>>> specification language syntax is not yet decided.
>>>>>
>>>>> Tim
>>>>>
>>>>>
>>>>>
>>>>>
>>>>> On 10/9/20, Tim Daly wrote:
>>>>>> A great deal of thought has gone into the representation
>>>>>> of functions in the SANE version.
>>>>>>
>>>>>> It is important that a function lives within an environment.
>>>>>> There are no "stand alone" functions. Given a function
>>>>>> its environment contains the representation which itself
>>>>>> is a function type with accessor functions. Wrapped
>>>>>> around these is the domain type containing other
>>>>>> functions. The domain type lives within several
>>>>>> preorders of environments, some dictated by the
>>>>>> structure of group theory, some dictated by the structure
>>>>>> of the logic.
>>>>>>
>>>>>> Lisp has the ability to construct arbitrary structures
>>>>>> which can be nested or non-nested, and even potentially
>>>>>> circular.
>>>>>>
>>>>>> Even more interesting is that these structures can be
>>>>>> "self modified" so that one could have a domain (e.g.
>>>>>> genetic algorithms) that self-adapt, based on input.
>>>>>> Or "AI" domains, representated as weight matrices,
>>>>>> that self-adapt to input by changing weights.
>>>>>>
>>>>>> Ultimately the goal of the representation should be that,
>>>>>> given a function, it should be possible to traverse the
>>>>>> whole of the environment using a small, well-defined
>>>>>> set of well-typed structure walkers.
>>>>>>
>>>>>> All of this is easy to write down in Lisp.
>>>>>> The puzzle is how to reflect these ideas in Spad.
>>>>>>
>>>>>> Currently the compiler translates all of the Spad
>>>>>> code to Lisp objects so the Spad->Lisp conversion
>>>>>> is easy. Lisp->Spad is also easy for things that have
>>>>>> a surface representation in Spad. But, in general,
>>>>>> Lisp->Spad is only a partial function, and somewhat
>>>>>> limited at that.
>>>>>>
>>>>>> I suspect that the solution will allow some domains
>>>>>> to be pure Lisp and others will allow in-line Lisp.
>>>>>>
>>>>>> Most of these ideas are nearly impossible to even
>>>>>> think about in other languages or, if attempted,
>>>>>> fall afoul of Greenspun's Tenth Rule, to wit:
>>>>>>
>>>>>> "Any sufficiently complicated C or Fortran program
>>>>>> contains an ad hoc, informally-specified, bug-ridden,
>>>>>> slow implementation of half of Common Lisp."
>>>>>>
>>>>>> Fortunately Spad is only a domain specific language
>>>>>> on top of Lisp. Once past the syntax level it is Lisp
>>>>>> all the way down.
>>>>>>
>>>>>> Tim
>>>>>>
>>>>>
>>>>
>>>
>>
>
From MAILER-DAEMON Fri Dec 18 02:59:58 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kqAgA-00026z-QY
for mharc-axiom-developer@gnu.org; Fri, 18 Dec 2020 02:59:58 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:42482)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kqAg9-00025U-9J
for axiom-developer@nongnu.org; Fri, 18 Dec 2020 02:59:57 -0500
Received: from mail-qk1-x733.google.com ([2607:f8b0:4864:20::733]:34830)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kqAg7-0007CN-PA
for axiom-developer@nongnu.org; Fri, 18 Dec 2020 02:59:57 -0500
Received: by mail-qk1-x733.google.com with SMTP id n142so1302884qkn.2
for ; Thu, 17 Dec 2020 23:59:54 -0800 (PST)
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;
bh=asUwa3LuyPXdeQjya1hC3ThE6NxiWHCz+V8vZYFkeIE=;
b=jY7vDim4guv8HXIuO6rvwZC6HbHf37BSWyDf+khNxvCnvMzahbD2f3cC/tOv7mdksI
YlJETPVZZ0syhnpz5q3x8yQtrf/ER0hWeNsAsWpnq7kxZJOdZrF/ky/QI2Bty+ejma+l
cPnqfkvJcv06UQQ/46+Z2E6n1BAF4SSg64eSe//MPVO50e+UYGSA73TkFcsaq6uTQHA9
XVxgkD3UBTfTb2fw3HMNVPsFSKJiIqHBKuolx6/cD756AhA8lb2Zl+5zfJPStwFyltJD
LMukzMPYJ0m+WstUNSjdFNw4j1DbHwd+nsc1aQpnvOjMW+1wfjAwmdqs8gXvxPZ4AfE0
Hgew==
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;
bh=asUwa3LuyPXdeQjya1hC3ThE6NxiWHCz+V8vZYFkeIE=;
b=YMdCpOhiowh8qeKZgzN8DWo8RSSyaEOtxljGQ7Op3YOhLtHd5t0F59/K1jlOY6751n
0QldUC0PMU6jPMngXnxZ4P/9souYb7tTT7+3CihlUfpNSfRDlHwdndqAqGApUpjbSaQh
XuhvjWR+j9xvi/+LOIFa3eKKny5ymhx0E0jQdU8aGrgPs0Q1ULi0zGs6pY4Gu055RbV+
rx71B8tluc8RPsJfGSxR+8iiEPhN4Z0DgJmnUJFuTQ3snYM2rBy+moyvGrRAJlVlIP3z
h2jpGwvlAu1zVz2VlNqH4I9ywUG7N0tQWufmUC7SUeRCx+PWmp9DpP42kc05LoDmMThx
bpag==
X-Gm-Message-State: AOAM531SVuyMEicJs8vsAP1y84lyS+Wt9rNL6NBzaYRgZLtPVCyoLash
ko8icj3dHbKUTe+El/8BzYbq56qeLTi+I+osKz9KuufsTgs=
X-Google-Smtp-Source: ABdhPJzMumfMvO+SMv44ELlLgKTeB+4a7kw5qETnDAi7hOeKyS1HbflG9CWEHYaBaAiNZXXFbMDjEkB8mNyrID2q8WU=
X-Received: by 2002:a05:620a:40d6:: with SMTP id
g22mr3353981qko.232.1608278394149;
Thu, 17 Dec 2020 23:59:54 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:ad4:568d:0:0:0:0:0 with HTTP; Thu, 17 Dec 2020 23:59:53
-0800 (PST)
In-Reply-To: <1607845528644.76141@ccny.cuny.edu>
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
<1607842080069.93596@ccny.cuny.edu> <1607845528644.76141@ccny.cuny.edu>
From: Tim Daly
Date: Fri, 18 Dec 2020 02:59:53 -0500
Message-ID:
Subject: Re: [EXTERNAL] Re: Axiom musings...
To: axiom-developer@nongnu.org, axiomcas@gmail.com
Content-Type: text/plain; charset="UTF-8"
Received-SPF: pass client-ip=2607:f8b0:4864:20::733;
envelope-from=axiomcas@gmail.com; helo=mail-qk1-x733.google.com
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Fri, 18 Dec 2020 07:59:57 -0000
I occasionally get grief because Axiom is implemented
in Common Lisp. People don't seem to like that for some
odd reason. Lisp, one of the easiest languages to learn,
seems to be difficult to accept.
I'm working with John Harrison's book "Practical Logic
and Automated Reasoning" from 2009. It uses OCaml
to implement the programs.
I've downloaded the OCaml sources from the website.
Apparently OCaml has changed significantly from 2009
since the code no longer compiles, spitting out "Alert
deprecated" all over the place and simply failing in places.
C++ code has a "standard", well, several "standards".
When someone asks "Do you know C++" you really
need to qualify that question. What you knew about
"standard C++" seems to change every 2 years.
I recently pulled out my KROPS code, used as the
basis for IBM's Expert System FAME. It was written
in Common Lisp (on a Symbolics machine). It still runs
unmodified despite being written about 40 years ago
on hardware and a software stack that no longer exists.
Axiom, written in the last century, still compiles and
runs. Say what you want about Lisp code, it still is the
most portable and long-lasting language I've ever used.
Tim
From MAILER-DAEMON Fri Dec 18 03:24:03 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kqB3T-000884-KB
for mharc-axiom-developer@gnu.org; Fri, 18 Dec 2020 03:24:03 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:47456)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kqB3S-00087q-CG
for axiom-developer@nongnu.org; Fri, 18 Dec 2020 03:24:02 -0500
Received: from mail-qv1-xf34.google.com ([2607:f8b0:4864:20::f34]:39879)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kqB3Q-0007BW-Ps
for axiom-developer@nongnu.org; Fri, 18 Dec 2020 03:24:02 -0500
Received: by mail-qv1-xf34.google.com with SMTP id s6so531762qvn.6
for ; Fri, 18 Dec 2020 00:24:00 -0800 (PST)
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;
bh=j1FnhP3wGoaxaZLXXY2i3CoJDqHtOtj8GKdH896Bfl0=;
b=ocif9BZNaqNqCWNYEx30MP3dan3ozS0zSrcs/hM6Gf6t1+dlpYfQKRkY7qCPJpPFyY
pcSaLWwz9odNSRCak13dFc3tRHFxuf0ztFeXGax/dKNRpSv1IGA0DOw6XlEzVVD7hVXI
5WBp5rJ6HpjzJJtxnbqLyHrawjqaF98suVcZIoc0YBj/H1Klj+gpgk9hUd0EwIpOgCT3
LZmJLKATfBirKIoGZVuZxEIdt+YASwfmzrcgqrBso3BOCA1vyZaWMiTWyT7vmBCDhuD6
VcLeHj6J6DMjLx2qqYAPNltXEfqqcFCaD7RGvdGeMn6GiiOLQSbBhcwVwPfBcYagC7ns
rFow==
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;
bh=j1FnhP3wGoaxaZLXXY2i3CoJDqHtOtj8GKdH896Bfl0=;
b=nc5IV0TGWYc3Vt3y+C6IgOQ2u7K9Fa2BIKKOaxUsigv93XmrdPD9g9K/BA7ZTwfsT8
ETVnA6C1odktG7X91X2eh+gj7EPyav4TFFHElaSIOQ02EjWsI70o0PHswKy4xkOza+0n
stekODAeZF9L0u4BM1EtFEl3jmO02HB7JaONUl1JxBru3k56YfRS+eZYw0KhLRdpOsit
cmSzTkR2vmDLxx7171XALhgUoeWaTqCF6LpP2AyZoUS0tSFAIrmMYVbFrta9yHxHC5D+
3oHNj3JlJSsb47s9W3t1ZBdyY78hPGCj+WRDdWv3cwEuN2N3ciIdEPg8sNh80NfD0+fI
7Vag==
X-Gm-Message-State: AOAM530VeerjSn3uGzFLSjSqv09U26+1Zcv58sgh0QPTcvGdkG9+MX79
1NrBvS3UFAZjtncMp1ShkZp5nbWNE9i5ufrEXRdfGgwjY+s=
X-Google-Smtp-Source: ABdhPJyhWqXtECPixy5U8qfZ7TJ3aZtRtThdV2F4QFlvPltP89xVDifAxRYwXAwgX6qY5sknWc5AYkbKGlGAqaMr7Ag=
X-Received: by 2002:a05:6214:2b2:: with SMTP id
m18mr3108978qvv.40.1608279839620;
Fri, 18 Dec 2020 00:23:59 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:ad4:568d:0:0:0:0:0 with HTTP; Fri, 18 Dec 2020 00:23:59
-0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
<1607842080069.93596@ccny.cuny.edu> <1607845528644.76141@ccny.cuny.edu>
From: Tim Daly
Date: Fri, 18 Dec 2020 03:23:59 -0500
Message-ID:
Subject: Re: [EXTERNAL] Re: Axiom musings...
To: axiom-developer@nongnu.org, axiomcas@gmail.com
Content-Type: text/plain; charset="UTF-8"
Received-SPF: pass client-ip=2607:f8b0:4864:20::f34;
envelope-from=axiomcas@gmail.com; helo=mail-qv1-xf34.google.com
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Fri, 18 Dec 2020 08:24:02 -0000
Quoting Dijkstra (1988, EWD1036):
... a program is no more than half a conjecture. The other
half of a conjecture is the functional specification the
program is supposed to satisfy. The programmer's task
is to present such complete conjectures as proven theorems.
Axiom's SANE research project is trying to build a system
where such "complete conjectures as proven theorems"
can be implemented, at least for mathematical algorithms.
After 50 years of programming it is humbling to realize
that I've neglected the most important half of programming.
The amount of effort and progress in proof theory, category
theory, and interactive theorem proving is amazing; most
of it only occuring in this century. I've spent the last 8 years
trying to "catch up" with what future programmers will take
as normal and expected.
Imagine a Google whiteboard interview where you are
asked to provide an algorithm and an associated proof.
Will you get hired?
Dijkstra saw this in 1988 and it's taken me decades to
hear and understand.
Tim
On 12/18/20, Tim Daly wrote:
> I occasionally get grief because Axiom is implemented
> in Common Lisp. People don't seem to like that for some
> odd reason. Lisp, one of the easiest languages to learn,
> seems to be difficult to accept.
>
> I'm working with John Harrison's book "Practical Logic
> and Automated Reasoning" from 2009. It uses OCaml
> to implement the programs.
>
> I've downloaded the OCaml sources from the website.
> Apparently OCaml has changed significantly from 2009
> since the code no longer compiles, spitting out "Alert
> deprecated" all over the place and simply failing in places.
>
> C++ code has a "standard", well, several "standards".
> When someone asks "Do you know C++" you really
> need to qualify that question. What you knew about
> "standard C++" seems to change every 2 years.
>
> I recently pulled out my KROPS code, used as the
> basis for IBM's Expert System FAME. It was written
> in Common Lisp (on a Symbolics machine). It still runs
> unmodified despite being written about 40 years ago
> on hardware and a software stack that no longer exists.
>
> Axiom, written in the last century, still compiles and
> runs. Say what you want about Lisp code, it still is the
> most portable and long-lasting language I've ever used.
>
> Tim
>
From MAILER-DAEMON Mon Dec 21 07:10:10 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1krK0w-0006Yj-Bb
for mharc-axiom-developer@gnu.org; Mon, 21 Dec 2020 07:10:10 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:37876)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1krK0u-0006XL-Hm
for axiom-developer@nongnu.org; Mon, 21 Dec 2020 07:10:08 -0500
Received: from mail-qt1-x830.google.com ([2607:f8b0:4864:20::830]:40075)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1krK0r-0003Hr-5D
for axiom-developer@nongnu.org; Mon, 21 Dec 2020 07:10:08 -0500
Received: by mail-qt1-x830.google.com with SMTP id v5so6361679qtv.7
for ; Mon, 21 Dec 2020 04:10:04 -0800 (PST)
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=FHoYEfdCEYWPq6o7TcyTPjcZjAVi7xZdBSuCe+BNouY=;
b=HmxmisbWuiTEA8RxsW/gohiyRKx+/MFRGPzJ2SHuRXf5O4nH60jL3RZu2Zm+XcbOGc
tulxgyZlOz9PKJJXX/2eqen20BTLkghWpAENzmjp1Q6uKBjAR0Zekfonc2bWBqns4T00
ObWSxTW3xLaTkcEY8/uh5xsliQNaqwFyWDnJTNRTZytN9T/7SYVPxlYQLVVZrzt7tvCn
nyNQoi7OGyYh2AJcmlUc1H55W8+CIFqWP5sSMh09rZmTbziHL3dLeQnD/My4rQfykk7G
5BQ6bPF+AEOQ7XcEh6KgeTRVytXvDeiuLAYD9JIUaB4xoI/T7sd1ud9ywuALRYdY/U15
/ySw==
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=FHoYEfdCEYWPq6o7TcyTPjcZjAVi7xZdBSuCe+BNouY=;
b=LPGFW6d+2XWvLdGqI45nZW5yEqakPkMa/qwBBEwRkQ814Ts1hKOBLqRipqNB8RsPla
qARpo8BRdJ/M3UpRXLu6M50z0W47DLkvXZl4js5YoeSnsXl+EoK+gf1E+XNBO6G9p3Uk
pAsmoX1lYHkqXPGxXkhwhXALwoVMF3NNyXkkG5SjwkADpSnYJqLy/UYot61YFjHYvwxA
CzwyhgQBmrfpAipI7fc8UJiBwLEVSwdbAeE/WGM1LZjuot2o1nM1bWgwQvZGWSLVYNGt
RA7DdijXyjPzBVpnW6vAbFZ42QO0ACxX3WK4UNzonat9HoL2IN58FJAmSoGOSvBG9Xr4
MxUA==
X-Gm-Message-State: AOAM532dC1VMqaFpD4cZWyx2HF7Fuu7qDR0pYIhiR/HODSER95nxglL/
7dEYbS1gILFjsRlzbGJN32oN7gEufZTLYLuAUPSw4VUR/+s=
X-Google-Smtp-Source: ABdhPJyGMUeHvfjAW1tMZtKiZMEy9+qvDwCATu9FKizcSts7iG43CS7PlqnXc6x72G1RVm443gZRre+/Uc4Ups5iEAA=
X-Received: by 2002:ac8:5359:: with SMTP id d25mr16396307qto.132.1608552603172;
Mon, 21 Dec 2020 04:10:03 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:ad4:568d:0:0:0:0:0 with HTTP; Mon, 21 Dec 2020 04:10:02
-0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
<1607842080069.93596@ccny.cuny.edu> <1607845528644.76141@ccny.cuny.edu>
From: Tim Daly
Date: Mon, 21 Dec 2020 07:10:02 -0500
Message-ID:
Subject: Re: [EXTERNAL] Re: Axiom musings...
To: axiom-developer@nongnu.org, axiomcas@gmail.com
Cc: Frank Pfenning , Jeremy Avigad ,
rwh@cs.cmu.edu
Content-Type: text/plain; charset="UTF-8"
Received-SPF: pass client-ip=2607:f8b0:4864:20::830;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x830.google.com
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Mon, 21 Dec 2020 12:10:08 -0000
The goal is to prove Axiom algorithms, such as the GCD
over the natural numbers, correct using something like Lean.
I've studied traditional approaches like Hoare triples
but I think there might be a different approach. It depends
on Harper's Trinity.
Suppose I had a set of verification conditions V.
Suppose I had a functor that carries V to a program P.
Suppose I had a functor that carries V to a proof Q.
By the category definition of functors this implies a
natural transformation between P and Q ... and I'm done.
Except for some annoying details, of course.
1) What is a functor from V to P? Well, I have all of
group theory already available because of the way
Axiom is constructed. So the "elements" of the functor
requires things like "carrying identity". Exactly what
this implies in the constructed program P needs to
be worked out in detail.
2) What is the functor from V to Q? Well, if I construct
a sequent calculus version of Lean's Type Theory then
I have a "complete" set of low-level tactics. It isn't clear
how those tactics can be applied to construct the functor
(at least not yet).
3) The two functors require certain constraints on the
verification conditions V. In dealing with the GCD over
the natural numbers (known as NonNegativeInteger or
NNI in Axiom) we need to make sure that V contains
all of the conditions that the correct program requires
(such as deriving the recursive call).
4) V also needs constraints in dealing with the GCD
so that the proof can use the Lean sequent rules
to derive a proof of the GCD. So I'd have to construct
a sequent proof of the GCD from the sequent-derived
tactics.
5) I don't know of a languge V that covers both the
needs of the functors for P and Q so that will take
some omphaloskepsis. I might have to write a
"linter" program.
This category theory approach, using Harper's Trinity,
has the potential of proving programs correct without
dealing with things like Hoare triples.
This all works in theory but there is a lot of practical
work, such as deriving a sequent form of Lean's Type
Theory, deriving functors that fulfill all the definitions
using things like Axiom's group theory structure, and
inventing the verification language V rich enough
for both needs.
It's gonna be a long winter :-)
Tim
.
On 12/18/20, Tim Daly wrote:
> Quoting Dijkstra (1988, EWD1036):
>
> ... a program is no more than half a conjecture. The other
> half of a conjecture is the functional specification the
> program is supposed to satisfy. The programmer's task
> is to present such complete conjectures as proven theorems.
>
>
> Axiom's SANE research project is trying to build a system
> where such "complete conjectures as proven theorems"
> can be implemented, at least for mathematical algorithms.
>
> After 50 years of programming it is humbling to realize
> that I've neglected the most important half of programming.
>
> The amount of effort and progress in proof theory, category
> theory, and interactive theorem proving is amazing; most
> of it only occuring in this century. I've spent the last 8 years
> trying to "catch up" with what future programmers will take
> as normal and expected.
>
> Imagine a Google whiteboard interview where you are
> asked to provide an algorithm and an associated proof.
> Will you get hired?
>
> Dijkstra saw this in 1988 and it's taken me decades to
> hear and understand.
>
> Tim
>
>
> On 12/18/20, Tim Daly wrote:
>> I occasionally get grief because Axiom is implemented
>> in Common Lisp. People don't seem to like that for some
>> odd reason. Lisp, one of the easiest languages to learn,
>> seems to be difficult to accept.
>>
>> I'm working with John Harrison's book "Practical Logic
>> and Automated Reasoning" from 2009. It uses OCaml
>> to implement the programs.
>>
>> I've downloaded the OCaml sources from the website.
>> Apparently OCaml has changed significantly from 2009
>> since the code no longer compiles, spitting out "Alert
>> deprecated" all over the place and simply failing in places.
>>
>> C++ code has a "standard", well, several "standards".
>> When someone asks "Do you know C++" you really
>> need to qualify that question. What you knew about
>> "standard C++" seems to change every 2 years.
>>
>> I recently pulled out my KROPS code, used as the
>> basis for IBM's Expert System FAME. It was written
>> in Common Lisp (on a Symbolics machine). It still runs
>> unmodified despite being written about 40 years ago
>> on hardware and a software stack that no longer exists.
>>
>> Axiom, written in the last century, still compiles and
>> runs. Say what you want about Lisp code, it still is the
>> most portable and long-lasting language I've ever used.
>>
>> Tim
>>
>
From MAILER-DAEMON Thu Dec 31 09:05:51 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kuyaN-0006ul-LB
for mharc-axiom-developer@gnu.org; Thu, 31 Dec 2020 09:05:51 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:40394)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kuyaM-0006ub-5v
for axiom-developer@nongnu.org; Thu, 31 Dec 2020 09:05:50 -0500
Received: from mail-qv1-xf2f.google.com ([2607:f8b0:4864:20::f2f]:37226)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kuyaK-0005i5-LC
for axiom-developer@nongnu.org; Thu, 31 Dec 2020 09:05:49 -0500
Received: by mail-qv1-xf2f.google.com with SMTP id l7so9010465qvt.4
for ; Thu, 31 Dec 2020 06:05:47 -0800 (PST)
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;
bh=DFR5e8bqG3yx/NWsMt9oC8tYo1UMRcSyFVYi13eZ7dk=;
b=JxOT85vPDfGGl7HJsFhA2XDzqusTjFw5g/+f/5H8CBTufjYbKdbfAkZE0vMj+7YRmh
bXgDiuSeO04BhERE0xlbmuyGl8yjjoM2hGbJ7H8+TNSMCCLd8LbLFW4BsIK2pH0S9G9P
5Od3xyF7l9PpsaNoDFEpqsLaReXOhQ8TJ/C+zjnBYnwbcx39ZAvUcxqJlBGSCnz7LQ0O
hX1wCPnRgtZ9+EhPE4drie+UqF9901nR45m57Ykx0MFsvh4tLiSCW1JvdmzWptWVeuem
HroCbOiPLAsHRBczNkaW0Lv8XFc7ooL+8ACDuud67NXntfH5OywL7dQoS9q/akxfZ2vq
IUkg==
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;
bh=DFR5e8bqG3yx/NWsMt9oC8tYo1UMRcSyFVYi13eZ7dk=;
b=iBV2BFevyTxS7TrPNrdZRouClmez2PmQ+dMyuG+eUY6KockaNiTsVoj8mNVXIhBzez
OlzB8KwhDGeWxkDYPfH1189FlYoMPHEu6FRozXH7BRlJX0LeuUnqhtBG/8qQlwECM3Yg
JOh5Ntb/zbIyy1T2WrNtd1/++7zyiJ2G4XS0NmL7AX/U/TlPchQHEOyVKFSXIWfuPJ5n
CqmFBy+ThtVMLKZAhYtH4AgSTn7/lKncomEJfMV8IaQnQDsRB8YSy2LsjTfWsQtZYCnx
Fo0xA7Az5liK+LfxREBSpY5+G4+bdnPuslGVyPXIWdoep3Lx2jabVqF97OXNdJMpNO5E
lnMA==
X-Gm-Message-State: AOAM532vtJn5QVYLEZh3Wmsl3517sZ/iPW5BBuiz9WXbbzircH4G5BF/
0yMO2+LsoO43uoNXWkHjfbnVjDEv/9fe6uzbjOjv3X6/fOY=
X-Google-Smtp-Source: ABdhPJz8/U+tX5Eu+P1VhuYH8VZvHYDh1r912fNoVo7C8qjW2iUQ7M7xKzzT0nYOlVIHZAmlw7MTdA0IEiiKidCb4po=
X-Received: by 2002:ad4:5491:: with SMTP id q17mr61641288qvy.62.1609423547024;
Thu, 31 Dec 2020 06:05:47 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:ad4:568d:0:0:0:0:0 with HTTP; Thu, 31 Dec 2020 06:05:46
-0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
<1607842080069.93596@ccny.cuny.edu> <1607845528644.76141@ccny.cuny.edu>
From: Tim Daly
Date: Thu, 31 Dec 2020 09:05:46 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , axiomcas@gmail.com
Content-Type: text/plain; charset="UTF-8"
Received-SPF: pass client-ip=2607:f8b0:4864:20::f2f;
envelope-from=axiomcas@gmail.com; helo=mail-qv1-xf2f.google.com
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 31 Dec 2020 14:05:50 -0000
It's been a long, slow effort to "get up to speed" (or more
accurately "a slow crawl") on the various subjects one needs
to know to work on "computational mathematics" aka SANE.
A reading knowledge of a lot of areas is needed, including
things like
abstract algebra (to understand Axiom's category/domain)
type theory (to understand first-order dependent types)
proof theory (to understand Gentzen, sequents, etc.)
category theory (to understand catamorphs, functors, etc.)
metaobject protocol (to understand CLOS extensions)
number theory (to understand finite fields)
calculus (to understand field extensions for integration)
programming (to understand typeclasses, CLOS, etc)
philosophy (to understand polymorphic sets, etc)
CPU hardware (to understand "down to the metal", FPGA, etc.)
Specification (to understand consistancy, completness, etc)
Verification (to understand decision procedures, etc)
Proof tools (like Coq, Lean, etc.)
and a few other subjects that won't come to mind at the
moment.
The usual academic approach, that creates a special
"course of study", requiring classes in areas is probably
best. There are a lot of good online courses, such as
the UOregon summer school, that introduce the basic
ideas clearly. There are some good introductory books
like Troelstra and Schwichtenberg's "Basic Proof Theory"
that cover Gentsen, Hilbert, and Natural Deduction ideas.
It seems worthwhile to put together a full course of study
with links to videos and books, so one can get up to speed
on required knowledge. I'll start an outline with links to
these on the axiom-developer.org website in the coming
weeks. It's sort-of an "Axiom University" major in
computational mathematics.
(There are no degrees :-) But one does mathematics and
programming for the joy of it anyway so who cares?)
I welcome suggestions and online links.
Tim