View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Equational Logic

Equational Logic as a Programming Language

I didn't pay as much attention around chapters 18-20 as I could have (I'm not so interested in implementation techniques.)

Lots of interesting side issues this brings up, but in some sense [Survey of the Equational Programming Project][] is better as it is more brief. The language is essentially sort of like Haskell (lazy functional). The implementation is outermost rewriting. See also [Programming with Equations][].

All in all, interesting to learn about this research program, but it's not nearly what I thought it would be like, going by the word "equational".

Canonical Equational Proofs

A book that came from a PhD thesis. It's short (105 pages once you exclude the frontmatter and bibliography). It's mostly about completion (Knuth-Bendix completion) really.

Convergent rewrite systems reduce terms to normal forms. Completion finds a convergent rewrite system from an equational system (when it can). Completion systems can themselves be analyzed as equational inference systems. So basically, they give some rules of inference for Knuth-Bendix completion. (Operational semantics...? Probably not.)

They keep saying that theorem provers can be viewed as proof transformers or proof normalizers. I don't get this bit yet. I think they mean automated theorem provers. Does Knuth-Bendix completion take an existing equational proof and return a transformed (or normalized) rewrite proof? The input is just a set of equations, not a proof (right?) So it would seem to be rewriting an entire theory, not just a proof (right?) So, this is difficult for me to see.

Anyway, this is an extension of the concept of completion, as introduced by Knuth and Bendix. In Dershowitz and Plaisted's chapter on term rewriting (Chapter 9) they mention this topic, as "ordered completion". I'm not hugely interested in completion. But there are a few nice equational theory examples in here.

Equational Logic and Abstract Algebra

Kind of a light, intro-survey-ish paper, but with a few nice insights.

The author expresses the interesting insight that the complexity of equational logic lies somewhere between that of propositional logic and that of first-order logic. They back it up by briefly describing all three of these logics.

On page 9, the author lists the rules of inference of equational logic, as can be found in many works, but with an interesting twist:

We can replace the two rules R1 (Symmetry) and R2 (Transitivity) by one rule R5. R5. From r=s and s=t, deduce t=r. (circularity rule)

Then, naturally, group theory is presented as an equational theory. And they characterize the limitations of "universal algebra" by pointing out they need a few more alphabet symbols than just "." in order to do it properly, summarizing this with

The vast majority of algebraic structures allows us to study their equational theories, although a little unorthodoxy may be involved in a few cases.

And in particular,

The theory of fields or division rings cannot, however, be cast as equational theories - unless you really go against normal practice.

(For one example of really going against normal practice in this direction, see [Meadows and the Equational Specification of Division][].)

Also, some interesting trivia about lattices and boolean algebras being one-based ("Neither of these proofs were easy and the single equations were not particularly revealing.")

The decision procedures part mentions the Robbins conjecture, which was proved by McCune using the prover EQP.

Equational logic, unification and term rewriting

.

Field Guide to Equational Logic

Covers results about equational logic as an object of study in itself.

The field guide lists many results in equational logic, but one of the most interesting to me is section 6, which describes Tarski's relation algebra and how formulae of first-order logic of up to 3 variables (but no more!) may be translated to it.

Equational Logic (Course Notes, USC, Spring 2017)

Rather denser than the encyclopedic entries on Equational logic, and covers the connection between equational logic and universal algebra in more depth.

Highlights worth mentioning here:

Euclid's Elements as an Equational Theory

.

Meadows and the Equational Specification of Division

.

Survey of the Equational Programming Project

The "Equational Logic Programming" language (no other name is given) is basically confluent outermost term rewriting. So, a lot like Haskell. I don't actually see what it could get you that Haskell doesn't. So isn't it mostly like functional programming?

"Subset Logic" instead of equational logic is slightly interesting since it is rather "inequational logic", if a → b then a ≤ b. (Propositional algebras also have this ordering property. In fact, the explanation of implication as meaning "b is at least as true as a", which has been used by several people in their explanations of implication, notably Terrence Tao, reveals this ordering property too.)

See also [Programming with Equations][].

Programming with Equations

Shows what is probably the roots of Maude... but in effect this is (lazy) functional programming!

It is "equational" but there is always an assumed direction in which we want to "simplify" the equations. Really, it is "inequational" in some sense; we have 2 + 2 ≽ 4, where x ≽ y means "x = y but y is simpler than x".

And they implement this simplification with (outermost) rewriting, and they have to go to some lengths to avoid overlap etc, and the result is not exactly efficient.

But the equations look just like a functional program with matching!

(Which is of course implemented with outermost rewriting, sort of, under the hood, when it's a lazy functional language)

They basically say this!

Given that equations are used as reduction rules, we might compile them into routines for matching the specific left-hand sides involved and for making the particular replacements given by the right-hand sides.

Later on, I realized it is even better to look at it this way: every rewriting theory implies an equational theory. The rewriting theory 2 + 2 -> 4 implies the equational theory 2 + 2 = 4, so indeed every time you see 2 + 2 -> 4 you can reason "backwards" over it, to say 4 = 2 + 2. They are really talking about rewriting theories, invoking the equational "quotient" implicitly when necessary, and calling it equational. Historically, it evolved into "rewriting logic".)

Equational Logic -- from Wolfram MathWorld

.

predicate logic - Give an equational proof \$ \vdash (\forall x)(A \rightarrow B) \equiv ((\exists x) A) \rightarrow B\$ - Mathematics Stack Exchange

.

elementary set theory - Can I deduce one set distributive law from the other? - Mathematics Stack Exchange

.

Robbins algebra - Wikipedia

.

lo.logic - Formal verification of simple equational proofs (as in Universal Algebra...)? - MathOverflow

.