Ebfer

This document describes Ebfer, a simple pure functional programming language which has a simple proof language embedded within it.

When examples are given in this document, they are actually runnable test cases 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.

The proof language that is embedded in Ebfer is called Lome and it is defined prescriptively in its own repository.

This description of Ebfer will for the most part refer to that description when necessary, rather than repeating it here.

Modules

An Ebfer module consists of a number of function definitions.

Alongside these function definitions may appear all the components of a Lome development: proof transformer rules, proofs, and theorems.

In addition, these developments are extended in their scope, so that they may refer to, and thus prove properties of, the Ebfer functions in the same module.

Functions

-> Tests for functionality "Parse Ebfer Module"

-> Functionality "Parse Ebfer Module" is implemented by
-> shell command
-> "python3 bin/ebfer --no-check --no-eval %(test-body-file) && echo 'ok'"

An Ebfer function looks a lot like a Lome rule, but is introduced with the keyword fun.

fun perim(W, L) => add(mul(W, 2), mul(L, 2))
===> ok

Syntax is of course checked when parsing functions.

fun perim(W, L) => ()
???> Expected identifier

Evaluation

-> Tests for functionality "Evaluate Ebfer Module"

-> Functionality "Evaluate Ebfer Module" is implemented by
-> shell command
-> "python3 bin/ebfer --no-check %(test-body-file)"

When an Ebfer module is evaluated, the function main in that module is evaluated.

fun main() => add(mul(5,2), mul(6,2))
===> 22

When main is evaluated it is not given any arguments.

fun main(X) => add(X, X)
???>

There should be a unique main function in the module, in order for it to be evaluated.

fun perim(W, L) => add(mul(W, 2), mul(L, 2))
???> No unique main function

fun perim(W, L) => add(mul(W, 2), mul(L, 2))
fun main() => perim(6,5)
fun main() => perim(6,7)
???> No unique main function

Functions (including main, of course) can call other functions in the module.

fun perim(W, L) => add(mul(W, 2), mul(L, 2))
fun main() => perim(6,5)
===> 22

Evaluating an atom (a term without subterms) in a context where that atom is bound to a value (such as when the atom is a formal parameter of the called function being evaluates), evaluates to the value that the atom is bound to.

fun blain(X) => X
fun main() => blain(23)
===> 23

In a context where the atom is not bound, however, it evaluates to the atom.

fun blain(Y) => X
fun main() => blain(23)
===> X

Proof-checking

-> Tests for functionality "Check Ebfer Module"

-> Functionality "Check Ebfer Module" is implemented by
-> shell command
-> "python3 bin/ebfer --no-eval %(test-body-file)"

An Ebfer module may contain a Lome development, independent of any Ebfer code.

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

But the real advantage of embedding Lome in Ebfer, is that Lome proofs about Ebfer functions can be written.

For every function in the program, one or more rules are made available. A rule named after the function, suffixed with _expand, can be applied, to expand the function to its definition.

fun double(X) => mul(2, X)
rule mul_nihil_right(mul(X, 0)) => 0
theorem
    double(0) => 0
proof
    *double_expand(double(0))
    mul(2, 0)
    *mul_nihil_right(mul(2, 0))
    0
qed
===> 1/1 proofs verified.

Providing a concrete value as in the above example results in a theorem that looks a lot like a unit test. The advantage over unit tests is that we don't need to write these proofs on concrete values.

fun mulzero(X) => mul(X, 0)
rule mul_nihil_right(mul(X, 0)) => 0
theorem
    mulzero(X) => 0
proof
    *mulzero_expand(mulzero(X))
    mul(X, 0)
    *mul_nihil_right(mul(X, 0))
    0
qed
===> 1/1 proofs verified.

In addition to _expand, a rule named after the function, suffixed with _contract, is available to make the reverse transformation.

fun perim(W, L) => add(mul(W, 2), mul(L, 2))
rule mul_comm(mul(A, B)) => mul(B, A)
rule add_comm(add(A, B)) => add(B, A)
theorem
    perim_comm(perim(W, L)) => perim(L, W)
proof
    *perim_expand(perim(W, L))
    add(mul(W, 2), mul(L, 2))
    *add_comm(add(mul(W, 2), mul(L, 2)))
    add(mul(L, 2), mul(W, 2))
    *perim_contract(add(mul(L, 2), mul(W, 2)))
    perim(L, W)
qed
===> 1/1 proofs verified.