Lome

Version 0.1 | See also: Eqthy

Work in progress

Lome is a markedly simple proof language (Footnote 1). It is a novel (Footnote 2) arrangement of several established ideas,

• calculational proof style (Footnote 3)
• fine-grained rewrite strategies (Footnote 4)
• decorators syntax (Footnote 5)

Traditional calculational proof style interleaves proof terms and rules; between any two steps of the proof, a justification for how the second was derived from the first must be shown. In Lome, the justification that is used to derive the next term is embedded in the proof term itself, in the form of a "decoration". The proof can thus be written more simply, as a list consisting only of decorated terms. As an example, here is a trivial theorem of a fragment of monoid theory, written in Lome:

rule right_id(mul(X, e)) => X
rule left_id(mul(e, X)) => X
proof
    mul(mul(a, e), mul(e, a))
    mul(*right_id(mul(a, e)), *left_id(mul(e, a)))
    mul(a, a)
qed

This arrangement also obviates the need for the proof checker to search for exactly where each rule is to be applied (which is often left unsaid in calculational proofs); the position of the decoration in the term unambiguously locates exactly where the rule is to be applied.

This arrangement also moves the focus of the proof checking mechanism away from term rewriting slightly, and aligns it more closely to the LCF architecture (Footnote 6). The rule that is named in a decoration is a function that maps valid proof terms to valid proof terms; these functions comprise a set of operations on an ADT, which supports only these operations, ensuring validity; and each decorator is an application of the function that implements its rule. At the same time, it complements the LCF achitecture, in that the Lome proof constitutes a proof certificate that would, in a "pure" LCF architecture, not be recorded.

For the full definition of the Lome language, see doc/Lome.md.

Future Work

1) The kinds of rules that can currently be defined in Lome are relatively simple ones, based on substitution of variables in terms. This is probably enough to express axioms and rules of inference for equational logic, but we may need to expand the set of mechanics that can be used in rule definitions if we want to support more general (implication-based) rules. (Note: I'm less convinced of this than when I wrote it - but it still does remain to be seen.)

2) We would like to embed Lome in a simple functional programming language, and allow writing Lome theorems about the functions defined in the program. That will probably be a distinct language with a different name, but when it exists, it will effectively be a superset of Lome. Note that this dovetails very well with decorators being applications of functions; in a functional language, decorators could be defined just as functions are.

3) Lome is hopefully simple enough that it could conceivably be implemented on an 8-bit home computer such as the Commodore 64, either in BASIC or in machine language.

Footnotes

Footnote 1

A "proof language" in this sense is a computer language in which theorems can be stated and mechanically checked by a computer. And a "computer language" in this sense is a rigorously-defined, machine-processable data format which can be read and written by humans using common text editing software.

Footnote 2

To the best of my knowledge. I have not seen a notation for proofs that arranges rules to be applied at each step, in this way, for the purpose of making proof checking simpler.

Footnote 3

Calculational proof style was developed by Dijkstra and others as part of research into programming methodology. For more background, see Ralph-Johan Back's article Structured Derivations as a Unifying Proof Format

Footnote 4

Term rewriting must necessarily use some strategy to pick the order in which terms are rewritten. Modern tools such as Stratego/XT and Maude allow fine-grained control over the strategy in use. Lome in some sense takes this idea to its logical extreme: the user specifies exactly which subterm should be rewritten at each step, relieving the rewriter from all burden of searching for possible rewrites.

Footnote 5

As used extensively in mainstream programming languages such as Python and JavaScript. A minor variation here is that decorators are applied to terms rather than function definitions.

Footnote 6

The LCF architecture refers to the idea of modelling a proof object as an instance of an ADT with operations that ensure its continuous validity, which originated with the Edinburgh LCF theorem prover. For more information, see the LCF architecture article at PLS Lab.