From MAILER-DAEMON Tue Nov 10 02:14:30 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kcNrK-0006Q6-FA
for mharc-axiom-developer@gnu.org; Tue, 10 Nov 2020 02:14:30 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:51948)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kcNrJ-0006Nc-9H
for axiom-developer@nongnu.org; Tue, 10 Nov 2020 02:14:29 -0500
Received: from mail-qk1-x733.google.com ([2607:f8b0:4864:20::733]:45246)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kcNrH-00066k-FV
for axiom-developer@nongnu.org; Tue, 10 Nov 2020 02:14:28 -0500
Received: by mail-qk1-x733.google.com with SMTP id q5so6372866qkc.12
for ; Mon, 09 Nov 2020 23:14:26 -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=GrOYlaIVwcyNSxl050CJVHS/vOD2FEEKL5s5DyFscHQ=;
b=keTwAilGV+cYgHjaGtelKoQS3cEc4PQWeRxHDBfPFEnpLgIOIj3FNAQ7eDPS1wROIk
SMysMmM8eIU9zB5Nk44ZfpVlfzkqgvJjGNbZGQS01ewXrhOnPha+POjAX2FZXHz/ngY/
Og5hcrS4IvT/j/oSMJ2ZWSJOPEe2ax9kS7evmWLgmVhFPvmC/XX/JF+8dfRrKH38bZkA
VRsgKxfzqR5BBDeFd/RasiW8gZw5hsXbgmfcBqjGR7Y1RqdAkSL0hOPkzLDABEwXk8uh
wO4ZcSiooyKCDf8Jh/ETW56mWpQtocrQIYb9gPv+YuEm8lpT/x2Cqofu+/yBCEKEFCFX
8gDg==
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=GrOYlaIVwcyNSxl050CJVHS/vOD2FEEKL5s5DyFscHQ=;
b=YV8vsH0Ij/5uRtf83+/2vzojxVkrnIOCP5Gpz5XPeQ2T3WvP3u2sayA4RqU9eNlo+m
bWVnG64qJjwt/ImqZb4xh3pusxjvYHPQK0rw49qh0qZ7uKMVoOZVtNpUHqHtdnhBk4cE
Bz4eNwrc/dHxbS+FdvJWm6BC8TxE17fG3FsZywHQcIzXhGd/e9b1JyKPLnRWSba43HGZ
1Lew8AE64nNsye3DHiXCktFbVObrOJck3NMswi9ST6z9d276b7aBoq4NeayZXod0YpFj
gm/EM8jplBNgY45ut5t3HI4pAYPGyAq5/Z46TT7Md+dzvLbyMRLGdfRp8CEHaFe+t1tr
0Kag==
X-Gm-Message-State: AOAM530e6sDLPisMTbAukJaljNNsonCCZVQrAwgVhBeNeZoC4ki7P63G
DgBNbi19ur/Fzoh2fM7cgGHooXaxfPp/i6yZZMS1mtv3fbk=
X-Google-Smtp-Source: ABdhPJxP0slfyI/q7/ZvVh9CmMy63jE8mK7PsdKhniYSyIdIWn+b0oZlVefEl8/9GKqcrNKX0yq/0SBQrP4QKcJ05o0=
X-Received: by 2002:a37:56c3:: with SMTP id
k186mr13723423qkb.232.1604992465785;
Mon, 09 Nov 2020 23:14:25 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a05:6214:1c2:0:0:0:0 with HTTP; Mon, 9 Nov 2020 23:14:24
-0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
From: Tim Daly
Date: Tue, 10 Nov 2020 02:14:24 -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::733;
envelope-from=axiomcas@gmail.com; helo=mail-qk1-x733.google.com
X-detected-operating-system: by eggs.gnu.org: No matching host in p0f cache.
That's all we know.
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: Tue, 10 Nov 2020 07:14:29 -0000
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 Nov 27 07:57:44 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kidJo-0005Wt-J7
for mharc-axiom-developer@gnu.org; Fri, 27 Nov 2020 07:57:44 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:36130)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kidJn-0005Wh-Ao
for axiom-developer@nongnu.org; Fri, 27 Nov 2020 07:57:43 -0500
Received: from mail-qt1-x829.google.com ([2607:f8b0:4864:20::829]:43026)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kidJl-000677-Lw
for axiom-developer@nongnu.org; Fri, 27 Nov 2020 07:57:43 -0500
Received: by mail-qt1-x829.google.com with SMTP id f93so3131101qtb.10
for ; Fri, 27 Nov 2020 04:57: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;
bh=MGTFCAvgFpLa15bhFUhWWEg9epHB8hSQw0Hag4jTTL4=;
b=ECFtUCG4k4kb2mxUWlXr1r3s98WcIALRUHKCbp3efkIliugficQUx3xqXgu8ffZgt+
nGjNM8jMmNEIcDo0o2beLpL0psyGzRqJm9pugLsLsPVIFeFrvbcavgDoW/IH14y4Fq0T
r8YKg4CavszNUi0jp1rB6F6WV99BGe2bc3p+8KOFwIAVGlqSBzcvUaHCNcssLFMk1KVB
vGwiKRdzAh6BNBrZ+hnjK0ogZNhSb9Lqy0Y5cocnqfmhfjTC798zKNiOCfVODO11HC3S
D57e4j5IpNJA/lswTd/9OPYL7iYrhc5p5+oUlvBAUdZhGkOc28bG6ZQG8ea6J8JCAn9p
1lMg==
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=MGTFCAvgFpLa15bhFUhWWEg9epHB8hSQw0Hag4jTTL4=;
b=SjbSB8h6YFnjofJbWr5DmbFX82ftoHlzdSC2mOr6kbxbA5d1UNjEp/oV4/9P2jZwsE
BgoAwlOFaAQFzaqs7uUJANPk8Pn0DO/fONLP6dPegrHW7k+vA4VvHQ6FNhyRxcK+ztc2
xVvk6xvscc5jYPfWLL817rHhXqgG/nc1mAdqTmjSDIT+5SFJOaZiJ3FaJ4Zt5y+d+tI3
Dy8mOWHOHLCJnpgfiJgHm4twJUNTK1eDm6CgP0bgRJFfOwNY3NAFm1Asq1RhqWDR5q6C
2Ya7NMvq1kGJnExrUZBJwrLprsjRhHHdovc6ULiAgFr7whWoorih7exEfjnbpy7OwYd4
tttQ==
X-Gm-Message-State: AOAM532eHDiSKi5sajmpaN373IKnx1B421HzPm0l4laq7aUYoofOVpUT
gPVfaUHmjtl+IZQ/Vb4dF6TqyGgbOHVOJD61/FGXNThWg2U=
X-Google-Smtp-Source: ABdhPJzR2x8SbgMO2aYtq8fIjoUD746pO0SjylZKQ/bg/pdGTEgYmBB8WTgiFKZnhgipJZnsCQPccO38OI0y5tUapds=
X-Received: by 2002:ac8:46cf:: with SMTP id h15mr7738275qto.99.1606481860038;
Fri, 27 Nov 2020 04:57:40 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:b6d2:0:0:0:0:0 with HTTP; Fri, 27 Nov 2020 04:57:39
-0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
From: Tim Daly
Date: Fri, 27 Nov 2020 07:57:39 -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::829;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x829.google.com
X-Spam_score_int: -10
X-Spam_score: -1.1
X-Spam_bar: -
X-Spam_report: (-1.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 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, 27 Nov 2020 12:57:43 -0000
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 Sun Nov 29 02:29:42 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kjH9S-0003VZ-40
for mharc-axiom-developer@gnu.org; Sun, 29 Nov 2020 02:29:42 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:52296)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kjH9P-0003VO-VU
for axiom-developer@nongnu.org; Sun, 29 Nov 2020 02:29:39 -0500
Received: from mail-qt1-x82a.google.com ([2607:f8b0:4864:20::82a]:41861)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kjH9O-0003Pj-2V
for axiom-developer@nongnu.org; Sun, 29 Nov 2020 02:29:39 -0500
Received: by mail-qt1-x82a.google.com with SMTP id l7so6120436qtp.8
for ; Sat, 28 Nov 2020 23:29:37 -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=sDDjckzWCzk9SxuMVlY00wsTHM7Ju0lyN5lcHEMxEtE=;
b=h8noj/nNDs3/PqgXOqx70gJJCnyEpJxjXs0ffP5kSvdhxaPemFarm2A0YTKLW7sd+n
GQEuIIJ6ZQpKu8WXI3D4LkkzcHGlzC7iglhFNVK///m5ZSg1/trqGqvPW2GM135O3DH8
Z4i4cmPt8mICCjn6TBuj43qhnl07gNcRK3sBNxBl8nGVY2pqVH6QxC3vYtmK3PEETF5L
3wEdNKI8/orbWFmt2LgtYh7WwB+sEcg+AB6yt76LHHU2D+najI/nrRYLQBy7yydRZOda
Ly0THayuuAw9ZVis8282aQA3b/ZTQWQ4QpUnBpWYB8rVyMJmSjWCuqTZ5wG2OYJLWAoF
f5kA==
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=sDDjckzWCzk9SxuMVlY00wsTHM7Ju0lyN5lcHEMxEtE=;
b=oC5L3VrL5gPio5h2f1lzall0cMuPrHaqkDKTelhgMESFa1ivZKUp7k3UdRVQmPiRdJ
N0HGEptTeMa5+Lw9xIb8VeFraGqgCNMhI2d0reg2k7F0AGAncV2OFP551cAYAKYLQVQv
DlayXfqfToP2qrCeWBzOTshazI78Rz0kzcShZE0aw3ZXQ7KQl3URxkz1ft3/hLPVqsSz
d9PBbOp7lZChO9vYVXEwMD0IkfTlMhgae4UckOprK39ulYZYrVWt6GnqxaB4bydeeoup
QIiQcwpcwC6+1qRK5I5ImHF2KHekCFXwTTWMpidQRaSeYPEjLvdHEbyizrFo6ykabDrb
JOyg==
X-Gm-Message-State: AOAM5307Ck0mcZBRVI80vgChHgkR+XbCP+xkaRMe/RdIrgBG5NYpDOOi
3kgdFbWLUUe6sO9HJD1MnWzGIUd5+LeidD3AODmg5g4K5+o=
X-Google-Smtp-Source: ABdhPJzbQ2S+mXvVWqI9m7ogzvBxfxwSsxoKs3c6Arbk0WBSHX6dJksIZBG30cxCeNc/0v2gaH0HFC5PL891GmWUa8k=
X-Received: by 2002:aed:31a4:: with SMTP id 33mr15922718qth.132.1606634976189;
Sat, 28 Nov 2020 23:29:36 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:b6d2:0:0:0:0:0 with HTTP; Sat, 28 Nov 2020 23:29:35
-0800 (PST)
In-Reply-To:
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
From: Tim Daly
Date: Sun, 29 Nov 2020 02:29:35 -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::82a;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x82a.google.com
X-Spam_score_int: -10
X-Spam_score: -1.1
X-Spam_bar: -
X-Spam_report: (-1.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 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: Sun, 29 Nov 2020 07:29:40 -0000
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=GPvw92IKO44&list=UUhfUOAhz7ynELF-s_1LPpWg&index=28
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 Mon Nov 30 00:14:40 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kjbWK-0005mY-2O
for mharc-axiom-developer@gnu.org; Mon, 30 Nov 2020 00:14:40 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:57224)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1kjbWI-0005mN-G6
for axiom-developer@nongnu.org; Mon, 30 Nov 2020 00:14:38 -0500
Received: from mail-qt1-x831.google.com ([2607:f8b0:4864:20::831]:34796)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1kjbWG-0007lm-Aw
for axiom-developer@nongnu.org; Mon, 30 Nov 2020 00:14:38 -0500
Received: by mail-qt1-x831.google.com with SMTP id 7so7403404qtp.1
for ; Sun, 29 Nov 2020 21:14:36 -0800 (PST)
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=hPG47nm6749+AylXdfxY2pF7MH4QTOfmuORS6gtHkuQ=;
b=gVQR1Frml8dGxRcumuWQnmulpwURZVwmWizA9ZuutsB5V55iWpTMf7XqBIyLmhSl3I
mv0+bj2I5238BYhAhxCMeLY5euavsDKzVhs8caYkj4KwApYi5jNZy7edcLSbrjChmiAi
PhHWIQWmDY0x0MJWsgdeCFH1zmwYPCyAER+elhcw8v7cpioC+FEMk+RL4srP+3zw0Tdy
5eVYvfFGHjuPLsNrRGUnKMA/UsIR0EIJTGA87hXfFujdle6k6Ff1mUXa+JxLHf1J50WD
lNXrxnOSFHiibVuHZ8goa86VxEO/t/QBk6CXUvrP1k5loglYdMl8JEvAKQzA4E6NDvTR
ywnA==
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=hPG47nm6749+AylXdfxY2pF7MH4QTOfmuORS6gtHkuQ=;
b=cbPoRBCmcaf7YVTuhJAp8Sz4CiAuPnDI7VB0xSGhOHKzqXdO15uohyZusq1yQZd/pC
t/4yZDH8qWy0PY8QEgLXK19/uQAOXFwrBlI64jRwJ7TjMwAu2qWrXJkEvkbKqFdTaY3U
ZENA5YDVqfBCDyv9IPJQe/BioVAFT9KpZrnMS6iEH6FqsQ6X5x6sy7ueM6zFSo22y3rT
95AExb37OwlJspjYNtfF9XIWp6XBV7aqvdmNLyAMBGPyw0XodIvDzOaut+vr0URfSa/c
IIYTqREG/ZmkeGTOUhvFcU1FFurxFCfwL+qhXPKUPIAXMa0enzYsRg4H4Pg9Wx6ms0u4
7npw==
X-Gm-Message-State: AOAM532E+2a3UpQxBFMHL6/UMjxYqYhBwNnJCCQ8kREpfqhtQrZDZ/0a
A0UFSQ550/p0zVFAeoPCBs7YRMYhwwhm4yWA7EE=
X-Google-Smtp-Source: ABdhPJyBrcWJ/2ThBUzUlsEON0V++eeR6VPHsCRXXgLIUXbCId038iM9Sa9MsQnC6jzJn0flBChNh11Ya3xB1eZjK8Y=
X-Received: by 2002:aed:2863:: with SMTP id r90mr20086679qtd.188.1606713275203;
Sun, 29 Nov 2020 21:14:35 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:b6d2:0:0:0:0:0 with HTTP; Sun, 29 Nov 2020 21:14:34
-0800 (PST)
From: Tim Daly
Date: Mon, 30 Nov 2020 00:14:34 -0500
Message-ID:
Subject: Proving Theorems with Computers
To: k.buzzard@imperial.ac.uk, axiom-dev ,
Tim Daly
Content-Type: text/plain; charset="UTF-8"
Received-SPF: pass client-ip=2607:f8b0:4864:20::831;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x831.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, 30 Nov 2020 05:14:38 -0000
I'm leading the Axiom Computer Algebra open source
project. I've (tried to) interact with the Lean community.
I have a couple comments about your article.
https://www.ams.org/journals/notices/202011/rnoti-p1791.pdf
I wholeheartedly approve of what you are doing.
Have you video'ed any of your courses? I would
really like to take your course.
In section 3 you write
"...I would like to discuss the possibility of teaching
a computer pure mathematics..."
This is certainly a worthwhile goal. The current Axiom
system, however, falls into "applied mathematics" using,
as you say, "the intuition" that mathematicians develop.
It lives firmly in the "post-rigorous" stage of mathematics
despite being software.
I am trying to change that. The SANE (rational, coherent,
judicious, sound) project within Axiom has the goal of
unifying computer algebra and proof theory into a full
programming environment. Algorithms need proofs.
These proofs are "carried with them", always available
for further application.
I really wish you would write more about your comment
that "Lean is a functional programming language."
A note on the "puzzle" approach. You write
"It is my experience that certain undergraduates
enjoy solving puzzles like this in Lean..."
and certain of us don't. You lose the portion that
don't enjoy puzzles when they are trying to learn a
subject. Time is the only resource that is truly limited.
I, as one of the non-puzzle solvers, simply skip the
"exercise!". I'm trying to reach understanding as fast
as possible. Getting hung up because I don't know
the magic syntax and vast, inscrutable library just
wastes time.
Teaching styles differ, of course. But, unlike other
areas of mathematics, there is no other resource to
turn to when you get stuck. This is new territory.
The fact that you consider something trivial as an
"exercise!" hearkens back to your section on "intuition".
It seems to me that you're encouraging the philosophy
you seek to undermine. Save it for the graduate level.
Axiom is also "painfully obvious" to me. It is trivial to
coerce from a Polynomial(Fraction(Integer)), which is
a polynomial with fraction coefficients, to
Fraction(Polynomial(Integer)), which is a fraction with
numerator and denominator which are polynomials
with integer coefficients. Axiom can do this in one line,
which I leave you to solve as an "exercise!".
Unfortunately, Axiom suffers from the "steep learning curve"
disease. It never caught on because the language is very
strongly typed. If you get the types wrong you'll never get
anywhere.
The point is that while you think your definition of group
in Lean is obvious (and it is, as I can "read" it), the
actual "writing" of that definition presumes a HUGE
amount of knowledge, such as type theory (Type),
class inheritance (class..extends), logic (forall),
and a deep knowledge of the libraries (has_mul,
has_one, has_inv). Further, it assume knowing where
the colons go and how to type inverse superscripts.
It also presumes knowledge about class versus theorem
as it applies to Lean.
I've been programming for 50 years and paid to program
in 60 languages. I've authored 4 commercial languages.
I can learn a "standard language" in a day. But not Lean.
"Just" getting up to speed on Type Theory costs me
8 classes with Frank Pfenning, Bob Harper, and Karl
Crary. This despite Axiom being based on types.
All of the above "presumed knowledge" to write what
appears to be something trivial that is understandable
by "any mathematician" completely ignores the huge
"learning curve", which killed Axiom. Beware.
Sure, students can solve problems that involve deeper
mathematics. I could say the same thing when I started
using the HP and TI calculators. That hardly implied
that I knew about numerical integration by false position.
Lean suffers from a lack of documentation, especially
in the library. Where would I find a section on
perfectoid rings? What is the Arzela-Ascoli theorem?
I have suggested many times (and was essentially kicked
out of the Lean forum) because I believe documentation
is vital. Indeed, I think that all of the Lean libraries ought
to be literate programs. Lean should be readable as a
textbook, with the code as "equations".
Take any math(s) textbook, delete all of the text, leaving
just the equations. Try to learn from that. That is what
Lean is doing now. Equations in textbooks are just
"pictures". All of the real knowledge is in the paragraphs.
Lean has few paragraphs. At best you get a comment.
You write Lean contains "over a quarter million lines of code".
Axiom contains 1.2 million lines of code. Axiom is
still the best implementation of the Risch Integration
algorithm. The learning curve you have to climb to
even read the integration code is a PhD degree. Oh,
and there are no comments in the code. Good luck.
It isn't obvious now but if Lean continues on this path
it will fail, just like Axiom is failing. The problem is that
once the authors leave, such as you and Mario, no-one
will be able to maintain the system. Almost all of the life
of a system is spent in maintenance. At ABSOLUTE
minimum, EVERYTHING should have a literature
bibliographic link.
You comment
"Later on,we will ask whether proving profound results
results like this is even the right thing to be doing"
Bruno Buchberger implemented the Groebner basis
algorithm in Axiom. Nearly 30 years later it was proven
in Coq. I applaud this effort and think it is very valuable.
However, proving the algorithm did NOT prove the
implementation. If you want to be proof theory then
"just proving" something is useful. If you want to do
computer algebra then "just implementing" something
is useful. But if you want to do "computational
mathematics", then you need to unite the two in a
deep way.
You're running hard in proof theory but you're missing
half the game.
The use of "external solvers" is close to the goal of
using computer algebra in a proof system. It would
be a great help if, for instance, you wanted a Groebner
basis solution and Axiom could provide an "answer". It would
be SO much better if the computer algebra algorithm
came back with the associated proof.
We seem to be working toward a common goal, that
of "computational mathematics". Hopefully we will
"meet in the middle".
Please, please, please video your courses.
Stay healthy. Keep up the good fight.
Tim Daly