Eqthy TODO

Small Items

• Allow the first line of a proof to be an axiom.
• Arity checking in parser would prevent some silly errors in axioms.
• Improve unnamed theorem and axiom support (unique names across files.)

Desired Examples

• Relation algebraᵂᴾ
• A parsing logic, where S = NP VP, NP = Adj N, N = book, and so forth.
  • Could that be extended to Lambek calculus?
• Action algebra
• 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, for example

add{1, 2, X} = add{2, 3, 1}

and a simple implementation of matching that supports it without adding too many lines of code to the proof checker.

Rename Constructors when Requiring

My experience with writing the Ring Theory axioms and basic theorems suggests that it would be useful in Eqthy's ability to "Require" another Eqthy document, to treat it more like a "module", where the constructors could be renamed upon import.

That is, it would have been handy, when defining rings, to be able to "Require" the Group Theory axioms, renaming mul as add, and then ideally "Require" the definition of Monoid for the remaining axioms (perhaps renaming those constructors appropriately too.)

Embedding in a Functional Programming Language

There was previously an item here about embedding Eqthy in a functional programming language. This line of inquiry was taken up in the experimental Ebfer language, which embeds the Lome equational proof language, which is similar to Eqthy.