Lome

This document describes Lome, a simple proof language.

Developments

A Lome development consists of a number of proof transformer definitions and a number of theorems. Proof transformers, which we will also call "transformers" for brevity, are sometimes also called "axioms" or "rules of inference", depending on how they're applied.

A Lome theorem consists of a proof and optionally a proof transformer definition, whose validity is justified by the proof.

A Lome proof consists of a sequence of decorated ground terms, also called "proof terms".

A ground term consists of a constructor and zero or more ground subterms. A constructor is an atomic symbol consisting of one or more alphabetic characters. The subterms are given as a comma-seperated list enclosed in parentheses. If there are zero subterms, the parentheses may be omitted.

A decorated term is a term associated with a defined transformer and accompanied by zero or more additional decoration terms which influence the transformation.

In any proof term, multiple subterms may be decorated. The set of decorations on a term describes the specific way in which the term is intended to be transformed.

Decoration terms may not themselves be decorated (TODO: confirm this.)

A step in an Lome proof is a pair of adjacent proof terms in the sequence.

A step is valid if and only if the decorations in the first term of the step describe a transformation on that term that results in a term that is equal to the second term of the step with its decorations stripped out.

A proof is valid if every step in the proof is valid.

If a valid proof is accompanied by a proof transformer which relates the terms that the proof establishes, that transformer can be used in subsequent proofs, as its validity is justified by the proof.

Transformers

Transformers are pure functions which map terms (and zero or more additional arguments) to terms.

We write transformer defintions in a commonplace pattern-matching syntax, where uppercase letters indicate variables.

For example,

rule mul_comm(mul(A, B)) => mul(B, A)

A transformer may be defined to take additional decoration terms as arguments; these terms may influence how the transformation occurs.

For example,

rule mul_annhil_reverse(e, X) => mul(e, X)

Decorations

Decorations are applications of transformers.

In a proof term, a decoration is indicated by a leading asterisk. (NOTE: this syntax is provisional and is subject to change.)

For example, consider this step of an Lome proof:

*mul_comm(mul(7, add(2, 3)))
mul(add(2, 3), 7)

It is a valid step, because applying mul_comm (as defined in the previous section) to mul(7, add(2, 3)) does indeed result in mul(add(2, 3), 7).

Note that steps of a proof overlap. Thus the second term in a step may have decorations that will be meaningful when it appears as the first term in the next step. But in the current step, they are not meaningful. Thus, they are stripped out.

For example, the following step is, like the above step, also valid:

*mul_comm(mul(7, add(2, 3)))
mul(*add_comm(add(2, 3)), 7)

Decorations may also provide decoration terms, if the transformer supports them.

When a decoration is stripped out, all of the decoration terms are stripped out with it, leaving only the term which is the source of the transformation.

Examples

These examples are actually runnable test cases.

These tests are written in Falderal format. Each indented code block (generally preceded by a description) represents a test. All the lines of the code block up until the ===> line give the input to be tested; the text after ===> gives the expected output. ???> gives an expected error message, which is permitted to be a partial (substring) match.

-> Tests for functionality "Check Lome Development"

-> Functionality "Check Lome Development" is implemented by
-> shell command
-> "python3 bin/lome %(test-body-file)"

A simple development showing a single rule definition and a single proof.

rule right_id(mul(X, e)) => X
proof
    mul(a, e)
    *right_id(mul(a, e))
    a
qed
===> 1/1 proofs verified.

Multiple proofs can occur in a development.

rule right_id(mul(X, e)) => X
proof
    mul(a, e)
    *right_id(mul(a, e))
    a
qed
proof
    mul(mul(a, e), e)
    mul(*right_id(mul(a, e)), e)
    *right_id(mul(a, e))
    a
qed
===> 2/2 proofs verified.

A more involved proof, using several rules of inference, defined as proof transformers.

rule right_id(mul(X, e)) => X
rule left_id(mul(e, X)) => X
rule assoc_left(mul(mul(A, B), C)) => mul(A, mul(B, C))
rule left_inv(mul(inv(X), X)) => e
proof
    mul(mul(a, inv(b)), b)
    *assoc_left(mul(mul(a, inv(b)), b))
    mul(a, mul(inv(b), b))
    mul(a, *left_inv(mul(inv(b), b)))
    mul(a, e)
    *right_id(mul(a, e))
    a
qed
===> 1/1 proofs verified.

More than one proof transformer can be applied in a single step.

rule right_id(mul(X, e)) => X
rule left_id(mul(e, X)) => X
rule assoc_left(mul(mul(A, B), C)) => mul(A, mul(B, C))
rule left_inv(mul(inv(X), X)) => e
proof
    mul(mul(a, e), mul(e, a))
    mul(*right_id(mul(a, e)), *left_id(mul(e, a)))
    mul(a, a)
qed
===> 1/1 proofs verified.

Capitalized barewords indicate variables. When these variable symbols are used in rules, matching and substitution occur. However, variable symbols may be used in the bodies of proofs just as well as non-variable symbols can.

rule right_id(mul(X, e)) => X
proof
    mul(A, e)
    *right_id(mul(A, e))
    A
qed
===> 1/1 proofs verified.

In particular, there shall be no confusion when it comes to substitution.

rule right_id(mul(X, e)) => X
proof
    mul(X, mul(A, e))
    mul(X, *right_id(mul(A, e)))
    mul(X, A)
qed
===> 1/1 proofs verified.

rule mul_comm(mul(A, B)) => mul(B, A)
proof
    mul(B, A)
    *mul_comm(mul(B, A))
    mul(A, B)
    *mul_comm(mul(A, B))
    mul(B, A)
qed
===> 1/1 proofs verified.

If applying the rules referenced in the decorators in a step do not result in a term that matches the (undecorated) next step, the proof does not check. A trivial instance of this is if there are no decorators on a step, but the next step is not identical.

proof
    mul(a, mul(e, a))
    mul(a, a)
qed
???> 0/1 proofs verified.
???> Step 2 is invalid

If a rule is referenced in a decorator which has not been defined, the proof will fail to check.

proof
    mul(a, mul(e, a))
    mul(a, *right_id(mul(e, a)))
    mul(a, a)
qed
???> 0/1 proofs verified.
???> Unknown transformer: right_id

Here a rule is given to transform mul(e, a) to a, but the pattern in the rule does not match the term it's applied to in the decoration, and the proof fails to check.

rule right_id(mul(X, e)) => X
proof
    mul(a, mul(e, a))
    mul(a, *right_id(mul(e, a)))
    mul(a, a)
qed
???> 0/1 proofs verified.
???> Cannot apply right_id to mul(e, a): pattern right_id(mul(X, e)) does not match it

Here is another invalid proof. A rule is given to transform mul(e, a) to a, but that's not what the rule does.

rule right_foo(mul(e, X)) => e
proof
    mul(a, mul(e, a))
    mul(a, *right_foo(mul(e, a)))
    mul(a, a)
qed
???> 0/1 proofs verified.
???> Step 3 is invalid: mul(a, *right_foo(mul(e, a))) does not lead to mul(a, a)

A proof transformer may have two arguments instead of one. When it does, an arbitary term may be passed in as the second argument when it is applied in a proof.

rule mul_annhil_rev(e, X) => mul(e, X)
rule left_inv_rev(e, X) => mul(inv(X), X)
proof
    e
    *mul_annhil_rev(e, b)
    mul(e, b)
    mul(*left_inv_rev(e, b), b)
    mul(mul(inv(b), b), b)
qed
===> 1/1 proofs verified.

If a proof transformer is defined with two arguments, the second argument must be a variable. (NOTE: this constraint may be loosened in the future)

rule mul_foo_rev(e, mul(a, X)) => mul(e, X)
proof
    e
    *mul_foo_rev(e, mul(a, b))
    mul(e, b)
qed
???> 0/1 proofs verified.
???> Proof transformer mul_foo_rev(e, mul(a, X)) has a parameter that is not a variable

If a proof transformer is defined with two arguments, but some decoration does not include the second argument, the proof will not check.

rule mul_annhil_rev(e, X) => mul(e, X)
proof
    e
    *mul_annhil_rev(e)
    mul(e, b)
qed
???> 0/1 proofs verified.
???> Proof transformer mul_annhil_rev(e, X) has a parameter but no parameter given in term decoration *mul_annhil_rev(e)

Theorems

The rule form we've seen so far introduces a rule axiomatically. No proof is required, the system simply "admits" its existence. We can also establish theorems, which do require justification; we give this by means of writing out a proof.

A theorem that identity commutes, for example, might look like

rule mul_id_right(mul(X, e)) => X
rule mul_id_left(mul(e, X)) => X
rule mul_id_intro_right(X) => mul(X, e)
rule mul_id_intro_left(X) => mul(e, X)
theorem
    idcomm_right(mul(A, e)) => mul(e, A)
proof
    *mul_id_right(mul(A, e))
    *mul_id_intro_left(A)
    mul(e, A)
qed
===> 1/1 proofs verified.

We do need to write a second theorem if we want to go in the other direction.

rule mul_id_right(mul(X, e)) => X
rule mul_id_left(mul(e, X)) => X
rule mul_id_intro_right(X) => mul(X, e)
rule mul_id_intro_left(X) => mul(e, X)
theorem
    idcomm_right(mul(A, e)) => mul(e, A)
proof
    *mul_id_right(mul(A, e))
    *mul_id_intro_left(A)
    mul(e, A)
qed
theorem
    idcomm_left(mul(e, A)) => mul(A, e)
proof
    *mul_id_left(mul(e, A))
    *mul_id_intro_right(A)
    mul(A, e)
qed
===> 2/2 proofs verified.

After a theorem has properly justified a rule, it may be used in further proofs.

rule mul_id_right(mul(X, e)) => X
rule mul_id_left(mul(e, X)) => X
rule mul_id_intro_right(X) => mul(X, e)
rule mul_id_intro_left(X) => mul(e, X)
theorem
    idcomm_right(mul(A, e)) => mul(e, A)
proof
    *mul_id_right(mul(A, e))
    *mul_id_intro_left(A)
    mul(e, A)
qed
proof
    mul(f, e)
    *idcomm_right(mul(f, e))
    mul(e, f)
qed
===> 2/2 proofs verified.