## Tree @master (Download .tar.gz)

# Eqthy

*Version 0.4* | *See also:* Philomath
∘ LCF-style-ND

**Eqthy** is a formal language for equational proofs. Its design attempts to
reconcile *simplicity of implementation on a machine* with *potential for*
*usability by a human* (more on this below). It
supports an elementary linear style, where each line gives a step which is
derived from the step on the previous line, and may optionally state the
justification for the derivation in that step.

Here is a simple example: a proof that, in a monoid, the identity element commutes with any element.

```
axiom (idright) mul(A, e) = A
axiom (idleft) mul(e, A) = A
axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
theorem (idcomm)
mul(A, e) = mul(e, A)
proof
A = A
mul(A, e) = A [by idright]
mul(A, e) = mul(e, A) [by idleft]
qed
```

For improved human usability, Eqthy is usually embedded within Markdown documents. This allows proofs to be written in a more "literate" style, with interspersed explanatory prose and references in the form of hyperlinks.

For a fuller description of the language, including a set of Falderal
tests, see **doc/Eqthy.md**.

A number of proofs have been written in Eqthy to date. These can be found in
the **eg/** directory. In particular, there are worked-out proofs:

- in Group Theory, including:
- some simple theorems about the inverse element;
- the Socks and Shoes theorem;

- in Boolean Algebra, including:
- De Morgan's laws;
- the Absorption laws in an alternate axiomatization;
- some properties of set difference;

- in Interior Algebra (building on Boolean algebra);
- in Propositional Algebra;
- in Combinatory Logic;

with hopefully more to come in the future.

The Eqthy language is still at an early stage and is subject to change. However, since the idea is to accumulate a database of proofs which can be built upon, it is unlikely that the format of the language will change radically.

### Design Principles

Probably the language that Eqthy most resembles, in spirit, is Metamath; but its underlying mechanics are rather different. Eqthy is based on equational logic, so each step is an equation.

Eqthy's design attempts to reconcile simplicity of implementation on a machine with human usability. It should be understood that this is a balancing act; adding features to the language which improve usability will generally be detrimental to simplicity, and vice versa.

It has been implemented in Python 3 in about 760 lines of code; the core (term manipulation and verifier modules) is about 340 lines of code. For more details, see the Implementations section below.

It is also possible for a human to write Eqthy documents by hand, and to read them, without much specialized knowledge. The base logic is equational logic, which has only 5 rules of inference, and these rules are particularly widely understood; "replace equals with equals" is a standard part of the high-school algebra cirriculum.

In comparison, mmverify.py, a Python implementation of a Metamath checker, is about 630 lines of code; and while it is undoubtedly simple, the Metamath language is not widely regarded as being easy to write or read.

In fairness it should not go unstated that equational logic, lacking as it does implication and existential quantifiers, is widely regarded as more awkward to use than first-order predicate logic as a formal language for proofs.

### Implementations

While the language does not prescribe any specific application for proofs written in Eqthy, it is reasonable to expect that one of the main reasons one would want a computer to read one would be for it to check it for validity.

This distribution contains such a proof checker, written in Python 3.
The source code for it can be found in the **src/** directory.

The core module that does proof checking,
**eqthy.verifier**, is less than 200 lines in length,
despite having many logging statements (which both act as comments, and provide a
trace to help the user understand the execution of the verifier on any given
document).

The desire is to make reading the code and understanding its behaviour as un-intimidating as possible.

## TODO

### Small Items

- Handle "on LHS", "on RHS" in hints.
- Allow the first line of a proof to be an axiom.
- Scanner should report correct line number in errors when Eqthy document is embedded in Markdown.
- Arity checking in parser would prevent some silly errors in axioms.
- Test for error if naming a theorem or axiom with a name already in context.

### Desired Examples

- Relation algebra
- Johnson's 1892 axiom system given in Meredith and Prior's 1967 paper Equational Logic
- The theorem of ring theory given in Equational Logic, Spring 2017 by George McNulty (but it's a bit of a monster all right)

### Aspirational Items

#### Preprocessor

It would make some sense to split off the code that parses an Eqthy document into its own program, which the main program calls when reading in an Eqthy document, much in the same vein as the C preprocessor does. This would necessitate defining a simple intermediate format (S-expressions or JSON) by which the preprocessor communicates the parsed document to the main prover.

This would allow the syntax to become more sophisticated (for example, supporting infix syntax for operators) while the core proof checker is unchanged. And would allow re-implementing the core proof checker in another language without necessitating rewriting the entire parser too.

#### AC-unification

Or rather, AC-matching. An awful lot of a typical Eqthy proof involves merely rearranging things around operators that are associative and/or commutative. If Eqthy can be taught that

```
add(add(1, 2), X)
```

matches

```
add(2, add(3, 1))
```

with the unifier `X=3`

because it has been informed that `add`

is an associative and commutative operator, then many proof steps
can be omitted. The trick would be to have a simple syntax that
indicates this, and a simple implementation of matching that supports
it without adding too many lines of code to the proof checker.

#### Embedding in a Functional Programming Language

This may by its nature be a seperate project, as it would involve creating a functional programming language of which Eqthy is a subset.

The idea is that we would introduce a special form of axiom with some additional connotations. For example,

```
def add(X, 0) => X
```

would be in all respects the same as

```
axiom add(X, 0) = X
```

but with the additional connotation that when a term such as
`add(5, 0)`

is "evaluated" it should "reduce" to `5`

. There
is no connotation from this that "evaluating" 5 should "reduce"
to anything however, but it would still be possible to appeal
to the equality `add(5, 0) = 5`

in both directions in a proof
written in this language.

The practical upshot being that you could write small functional
programs and *also* proofs of some of their properties, in this
one language, which is only a modest superset of Eqthy.

##
Commit History
@master
`git clone https://git.catseye.tc/Eqthy/`

- These are theorems in the Boolean algebra document. Chris Pressey 4 months ago
- On the command line, call the input format `bare-eqthy`. Chris Pressey 4 months ago
- Final (maybe) edits to README before 0.4. Chris Pressey 4 months ago
- Factor Group Theory out into its own document. Chris Pressey 4 months ago
- Convert Algebra of Sets document to Absorption Laws proof. Chris Pressey 4 months ago
- Fix up testing infrastructure. Chris Pressey 4 months ago
- Add provisional logo for Eqthy. Chris Pressey 4 months ago
- Use Boolean algebra as basis for set difference, interior algebra. Chris Pressey 4 months ago
- Allow Eqthy documents in Markdown to include other Eqthy documents. Chris Pressey 4 months ago
- Use one Verifier object, have it keep the context. Chris Pressey 4 months ago