git @ Cat's Eye Technologies Maxixe / master doc / Design.md
master

Tree @master (Download .tar.gz)

Design.md @master — view rendered · raw · history · blame 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
Maxixe: Design
==============

Design Goals
------------

Maxixe's design goals are:

*   **Simplicity**: the implementation should be simple.  Re-implementing Maxixe in a
    different host language should be a conceivable weekend project.

*   **Familiarity**: proofs should look more or less like "classical" proofs which
    consist of a list of steps and the justification for each step.

*   **Explicitness**: the supplied proof must be written out completely explicitly;
    the implementation must not be made to search for any information that is not
    stated.

*   **Generality**: the proof language itself should make as few assumptions about
    the object language as possible.  It shouldn't be tied to any particular system
    of logic — as far as possible, it should be purely a [proof calculus][].

*   **Predicate Logic**: on the other hand, the proof language should, when given
    the rules of predicate logic, be powerful enough to allow one to check proofs
    using predicate logic (a.k.a. first-order logic).

*   **Correctness**: the proof-checking capability of the language must not
    claim that an incorrect proof is correct for the given rules.  It would also
    be nice if it does not claim that a correct proof is incorrect.

Here are some things which are *not* goals of Maxixe:

*   **Theorem proving**.  Maxixe need only check that a proof supplied to it is a valid
    proof.  It need not search for a proof given a theorem.

*   **Efficiency**.

### How well are these goals met? ###

*   **Simplicity**: as of this writing, the reference implementation of Maxixe, in Python, is
    less than 700 lines of code.  About 250 lines of that is the parser and scanner.  The AST
    AST and term (matching, replacing) infrastructure occupy around another 250 lines.

*   **Familiarity**: aside from the term language (meaning, you have to say `impl(A,B)` instead
    of `A→B`), the layout of a proof is fairly classical.  A proof consists of a set of
    rules of inference (which includes axioms and premises), the goal to be proved, and a
    list of steps.  Each step includes a phrase "by [rule] with [previous steps]" as its
    justification.  The last step must equal the goal to be proved.

*   **Explicitness**: virtually everything must be spelled out.  Maxixe will not even search
    for what previous proof steps were used in a step.

*   **Generality**: instead of coding the rules for Existential Instantiation (etc) in
    the proof language, we have coded constraints on hypotheses and conclusions which
    allow rules like EI to be written.  It's basically a [natural deduction][]-like system
    in which propositional logic, predicate logic, and other logics (ones that
    don't rely too heavily on side conditions for their rules) can be captured.

*   **Predicate Logic**: see the Generality point above.  I believe the examples show
    that a significant portion, but perhaps not yet all, of first-order logic, can be coded
    in Maxixe.

*   **Correctness**: see the Disclaimer in the README.  It's probably very close, but I
    wouldn't put money on it quite yet.  Bugs are always possible.

Related Work
------------

The most proximal influence on Maxixe is certainly [The Incredible Proof Machine][], which
displays proof steps graphically as a network of nodes, and lets you hook them up to form
a valid proof.  I learned a lot from it and have had a lot of fun with it.  You should
check it out too.

But I've been interested in writing a proof checker since reading (I think) an example in
one of Emil Post's early papers on [Post canonical systems][].  I don't remember the
exact example, but this was part of the research on effective computation, and he was
showing that what a mathematician or logicial does when checking a proof is essentially
a string-rewriting process.  Symbol manipulation.  Replacing equals with equals.

My interest was further piqued by a few mentions of this in the book
Advanced Topics in Term Rewriting.

And there is a proof in ML for the Working Programmer that I've always wanted to
mechanize (forthcoming in Maxixe, hopefully.)

I looked into Agda and while the Howard-Curry Isomorphism is really cool, I have to say
it also makes it possible to conflate two concepts, computing and proving, which are
in many respects _different_.  And for whatever reason, proofs written as computations
look just terribly pained to me.  I wanted something with a more classical approach.

And Coq is probably nice for what it does, but I really don't care much right now
about _finding_ proofs, I just want to check ones I've already found.

And both of these tools are really quite heavyweight; I wanted something lighter.

A modern but somewhat older proof-checker that is based on symbol manipulation is
[MetaMath].  It fits the bill in many ways, but its syntax is quite ugly.  It has
a huge body of work rendered to web pages though, so you should check it out too.

[The Incredible Proof Machine]:     http://incredible.pm/
[Post canonical systems]:           https://en.wikipedia.org/wiki/Post_canonical_system
[MetaMath]:                         http://us.metamath.org/
[proof calculus]:                   https://en.wikipedia.org/wiki/Proof_calculus
[natural deduction]:                https://en.wikipedia.org/wiki/Natural_deduction