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 <w...@ccny.cuny.edu> 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=sci.ccny.cuny....@nongnu.org> on behalf of > Tim Daly <axiom...@gmail.com> > 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 <axiom...@gmail.com> 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 > Axiom-developer@nongnu.org > 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= _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer