Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings

[Tim Daly]

It is all rather confusing. There are well over 100 "logics".

Equational logic, or equational reasoning, is a very restricted
logic having only equality as an operation.

An alternative interpretation would be a substitution-style
logic where equals can be substituted for equals as one of
the operations.

The expression x = x + 0 isn't meaningful in isolation. In
Axiom it would have surrounding axioms (in the coming
Sane version), one of which is that in some cases, the
zero is a unit.

Note that this is not an assignment operation but one whose
target type is a Boolean.

But "x = x + 0" has the type EQUATION(POLY(INT)), not
Boolean. Axiom says:

x = x + 0
               Type: Equation(Polynomial(Integer))
%::Boolean
   True
               Type: Boolean

The "elegant way" that Martin is questioning is the problem
of combining a certain kind of logic operation (refl aka
"reflection" where both sides are equal) with the notion of
a mathematical unit.

This particular issue is simple compared with the many other
issues. In Axiom, the question would be what is the type of
x, of 0, of +, and of the whole equation. If x is a matrix, for
example, the 0 is coerced to a matrix. And now the question
is "Is this equality true for matrix operations?"

Tim

On 6/25/19, William Sit <address@hidden> wrote:
>
> Dear Martin and Tim:
>
> The expression  x = x + 0, whether treated as a type or an equation, can
> only make sense when x, =, + and 0 are clearly typed and defined. It makes
> little sense to me that this, as an equation, can be "proved" to be valid
> universally (that is, without the definition of, say +). For example, if we
> are in a domain where + is defined as max, or as min, or as the binary logic
> operator "and", then the expression is not an identity for all values x in
> the domain. If + is the usual addition, or the logic operatior "or", then
> the expression is a true identity and can be proved (more or less from
> definitions). In Axiom, if valid, these are simply stated as properties of
> the domain or category as in "has ...".
>
> I assume this is well-known and perhaps that is what Martin meant by "(I'm
> skipping over a lot of details)". I am ignorant of type theory and often
> confused by terms like type, equation (equation type?), identity, and even
> proposition (like x = x + 0 is an identity) as used in proof theories.
> Please ignore this message if the first paragraph is irrelevant to this
> thread.
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> ________________________________________
> From: Axiom-developer
> <axiom-developer-bounces+wyscc=address@hidden> on behalf of
> Tim Daly <address@hidden>
> Sent: Wednesday, June 19, 2019 1:02 PM
> To: axiom-dev; Tim Daly
> Subject: [EXTERNAL] Re: [Axiom-developer] Axiom's Sane redesign musings
>
> Martin,
>
>> Are there some fundamental compromises that have to be made when combining
>> computer > algebra and proof technology?
>
>> For instance in proof assistants, like Coq, equations are types for
>> instance:
>
>> x = x + 0
>
>> is a proposition which, by Curry-Howard, can be represented as a type. To
>> prove the
>> proposition we have to find an inhabitant of the type (Refl).
>
>> But in computer algebra I would have thought this equation would be an
>> element of
>> some Equation type (I'm skipping over a lot of details).
>
>> Do you think both of these approaches could be brought together in a
>> consistent and elegant way?
>
>> Also my (limited) understanding is that Coq prevents inconsistencies which
>> makes it not Turing complete and therefore cant do everything Axiom can
>> do?
>
> Martin,
>
> There are many problems with the marriage of logic and algebra. For
> instance,
> the logic systems want proof of termination which is usually not
> possible. Often,
> though, a partial proof that does not guarantee termination is interesting
> and
> sufficient. TLA provides some possible ideas in this direction.
>
> Another problem is that in the generality of dependent types, full
> type resolution
> is undecidable (hence, a lot of the heuristics built into Axiom's
> interpreter).
> Still there are interesting discussions of programs as proof objects ongoing
> at
> the moment on the Lean discussion thread
> https://urldefense.proofpoint.com/v2/url?u=https-3A__leanprover.zulipchat.com_-23&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=Bh77WgNdFtJTZCN46189mNhezS-_JXcBwUWxnNPRF_8&s=u7sojPwgc1fuWoQpKPwsjxjH98p64z3RQNZlwxBTLPQ&e=
>
> Still other problems arise in equational reasoning or probablistic
> algorithms.
> I have looked at (and not really understood well) logics for these.
>
> On the other hand, things like the Groebner Basis algorithm have been proven
> in Coq. The technology, and the basic axioms, are gathering greater power.
>
> In particular, since Axiom has a strong scaffolding of abstract algebra, it
> is
> better suited for proofs than other systems. The fact that Axiom's compiler
> insists on type information makes it somewhat more likely to be provable.
>
> I have a very limited project goal of proving just the GCD algorithms in
> Axiom.
>
> The idea is to create a "thin thread" through all of the issues so that they
> can
> be attacked in more detail by later work. I've been gathering bits and
> pieces
> of GCD related items from the literature. See Volume 13 for the current
> state
> (mostly research notes and snippets to be reviewed)
> https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_daly_PDFS_blob_master_bookvol13.pdf&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=Bh77WgNdFtJTZCN46189mNhezS-_JXcBwUWxnNPRF_8&s=maYsCHxZ4fjQEYua_1NfaxuO785JXAJlC4YRps-YFwQ&e=
>
> The idea is to decorate the categories with their respective axioms. Then to
> decorate the domains with their axioms. Next to write specifications for the
> function implementations. Then finding invariants, pre- and post-conditions,
> etc. Finally, to generate a proof that can be automatically checked. So each
> function has a deep pile of inheritated informaion to help the proof.
>
> For example, a GCD algorithm in NonNegativeInteger already has the
> ability to assume non-negative types. And it inherits all the axioms that
> come with being a GCDDomain.
>
> The fact that computer algebra really is a form of mathematics (as opposed
> to, say proving a compiler) gives me hope that progress is possible, even if
> difficult.
>
> Do I know how to cross the "x=x+0" type vs equation form? No, but
> this is research so I won't know until I know :-)
>
> Tim
>
> On 6/19/19, Tim Daly <address@hidden> wrote:
>> Sane: "rational, coherent, judicious, sound"
>>
>> Axiom is computational mathematics, of course. The effort to
>> Prove Axiom Sane involves merging computer algebra and proof
>> technology so Axiom's algorithms have associated proofs.
>>
>> The union of these two fields has made it obvious how far behind
>> Axiom has fallen. Mathematicians and some computer languages
>> (e.g. Haskell) have started to converge on some unifying ideas.
>>
>> As a result, the new Sane compiler and interpreter needs to
>> consider the current environment that mathematicians expect.
>> This falls into several areas.
>>
>> 1) SYNTAX
>>
>> It is clear that Axiom's syntax and user interface has not kept
>> up with the proof technology. A trivial example is a signature.
>> Axiom likes:
>>
>>    foo : (a,b) -> c
>>
>> whereas Lean / Coq / or even Haskell prefers
>>
>>    foo: a -> b -> c
>>
>> Given that many systems (e.g. Haskell) use the second syntax
>> we need to consider adopting this more widely accepted syntax.
>>
>> 2) PROOF and SPECIFICATIONS
>>
>> And, obviously, Axiom does not support 'axiom', 'lemma',
>> 'corollary', nor any specification language, or any language
>> for proof support (e.g. 'invariant').
>>
>> Mathematicians have these tools readily available in many
>> systems today.
>>
>> 3) USER INTERFACE
>>
>> Axiom's command line interface and hyperdoc were fine for its
>> time but Lean and Coq use a browser. For example, in Lean:
>>
>> https://urldefense.proofpoint.com/v2/url?u=https-3A__leanprover.github.io_tutorial_&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=Bh77WgNdFtJTZCN46189mNhezS-_JXcBwUWxnNPRF_8&s=EM0zfm6XLk9cSYEzwVYO2vVnvmksn6UcM0KkUGyu_Og&e=
>>
>> or in Coq:
>>
>> https://urldefense.proofpoint.com/v2/url?u=https-3A__jscoq.github.io_&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=Bh77WgNdFtJTZCN46189mNhezS-_JXcBwUWxnNPRF_8&s=vLHZcW4aiLGGw3-bGeVoO4TFa3CBy3qIAlOIbRSbwf8&e=
>>
>> The combination of a browser, interactive development, and
>> "immediate documentation" merges a lot of Axiom's goals.
>>
>> 4) CATEGORY STRUCTURE
>>
>> William Farmer and Jacques Carette (McMaster University)
>> have the notion of "tiny theories". The basic idea (in Axiom
>> speak) is that each Category should only introduce a single
>> signature or a single axiom (e.g. commutativity). It seems
>> possible to restructure the Category hierarchy to use this model
>> wilthout changing the end result.
>>
>> 5) BIFORM THEORIES
>>
>> Farmer and Carette also have the notion of a 'biform theory'
>> which is a combination of code and proof. This is obviously
>> the same idea behind the Sane effort.
>>
>> 6) INTERACTIVITY
>>
>> As mentioned in (3) above, the user interface needs to support
>> much more interactive program development. Error messages
>> ought to point at the suspected code. This involves rewriting
>> the compiler and interpreter to better interface with these tools.
>>
>> Axiom already talks to a browser front end (Volume 11)
>> interactively but the newer combination of documentation
>> and interaction needs to be supported.
>>
>> Sage provides interactivity for some things but does not
>> (as far as I know) support the Lean-style browser interface.
>>
>> 7) ALGORITHMS
>>
>> Axiom's key strength and its key contribution is its collection
>> of algorithms. The proof systems strive for proofs but can't
>> do simple computations fast.
>>
>> The proof systems also cannot trust "Oracle" systems, since
>> they remain unproven.
>>
>> When Axiom's algorithms are proven, they provide the Oracle.
>>
>> 8) THE Sane EFFORT
>>
>> Some of the changes above are cosmetic (e.g. syntax), some
>> are "additive" (e.g. lemma, corollary), some are just a restructure
>> (e.g. "tiny theory" categories).
>>
>> Some of the changes are 'just programming', such as using
>> the browser to merge the command line and hyperdoc. This
>> involves changing the interpreter and compiler to deliver better
>> and more focused feedback All of that is "just a matter of
>> programming".
>>
>> The fundamental changes like merging a specification
>> language and underlying proof machinery are a real challenge.
>> "Layering Axiom" onto a trusted core is a real challenge but
>> (glacial) progress is being made.
>>
>> The proof systems are getting better. They lack long-term
>> stability (so far) and they lack Axiom's programming ability
>> (so far). But merging computer algebra and proof systems
>> seems to me to be possible with a focused effort.
>>
>> Due to its design and structure, Axiom seems the perfect
>> platform for this merger.
>>
>> Work on each of these areas is "in process" (albeit slowly).
>> The new Sane compiler is "on the path" to support all of these
>> goals.
>>
>> 9) THE "30 Year Horizion"
>>
>> Axiom either converges with the future directions by becoming
>> a proven and trusted mathematical tool ... or it dies.
>>
>> Axiom dies? ... As they say in the Navy "not on my watch".
>>
>> Tim
>>
>
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> https://urldefense.proofpoint.com/v2/url?u=https-3A__lists.nongnu.org_mailman_listinfo_axiom-2Ddeveloper&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=Bh77WgNdFtJTZCN46189mNhezS-_JXcBwUWxnNPRF_8&s=071bx5Hfnags51BaZCergjN7ZxGQ0eQzcEsWvOJHG1s&e=