Lome

Version 0.2 | 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.

Expressive power

The kinds of rules that can currently be defined in Lome are relatively simple ones. At the core they are based on substitution of variables in terms, which is enough to express axioms and rules of inference for equational logic.

Lome's facility for defining rules that can "parameterized" with an arbitrary term apparently allows it to go a little further, apparently allowing such things as constructing a context such as found in the sequent calculus.

This is however a very low-level manipulation of proof terms, in the manner of substructural logics, and quite tedious. (Who wants to spend half their proof solving a Rubik's Cube as a side quest?)

So the equational reasoning is extended to conditional equational reasoning: we can substitute equals for equals, but only in certain contexts, i.e. only in subterms of parent terms that match expected forms. When that form is the form of an assumption, for example, this lets us model proof under an assumption.

Related Work

Lome is being embedded in a WIP toy functional language, Ebfer, which allows to write Lome theorems about the functions defined in the program.

Future Work

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. A first, less ambitious step towards this would be to implement it in ANSI C and run it on a 16-bit system such as the Amiga 500.

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.