Ghilbert 2 sketch

25 views
Skip to first unread message

Raph Levien

unread,
Jun 4, 2017, 6:09:47 PM6/4/17
to ghil...@googlegroups.com
As promised, attached is a file containing sketches of what I think Ghilbert 2 syntax might look like. There are parts I'm very happy about, parts I'm still wrestling with, and parts that are up in the air.

The first thing to note is Unicode symbols. As I just answered Adam, I'm not fully committed to these. They are more annoying to input than ASCII, for sure, and not ideal for display. My final decision is largely going to be based on how well Unicode works in practice.

Another obvious feature is infix syntax with precedence. I'm convinced this is a useful investment. Pratt precedence parsers are not very hard, and I think infix math is much easier to deal with. Also, by having syntax there's a lot more we can do in the space between concrete and abstract syntax. For example, if I decide to go in the direction of LF and use lambda-expressions for binding, I can just declare that ∀xϕ is simply syntax for (all (lambda x ph)). I'm also interested in making 123 syntax for (:d 1 (:d 2 3)), etc.

The proof syntax is where things get the most interesting, and I'm basically very happy with this sketch. A theorem takes zero or more hypotheses with syntax "(hypname: hyp)" before a colon and the conclusion. Then comes the proof (here I'm assuming that neither ";" nor "::" can appear inside a wff).

A proof is a sequence of lines. Each line has an optional colon-delimited label, a proof expression, then an optional bracket-enclosed term representing the result of the proof line. Lines other than the last that are missing results are separated by ";".

A proof expression is an identifier naming an axiom, theorem, or hypothesis, followed by as many arguments as that identifier takes (hypotheses take no arguments). An argument is another proof expression (parenthesis-enclosed if it takes one or more arguments), a label, or the special label "_". This last simply refers to the previous line.

Result terms are unified with the result of that line of the proof. Any subterm can be replaced with "_". Thus, ";" is equivalent to "[_]". Result terms have three purposes:
* Making proofs easier to read.
* Giving names to dummy variables.
* Filling in terms that cannot by synthesized through unification.

This third purpose is apparent in the proof of "id", for which the result of the first ax_1 has an unconstrained subterm.

I also expect result terms to play a significant role in interaction with IDE-like tools. For example, after typing a line, the user could request the tool to print the result after that line. Also, since the expectation is that most proof lines are very short, it's likely that brute force search with no special theorem-proving logic could work well to instantiate a proof line for a goal expressed as a result.

Even without an IDE, I expect that result terms will be important for proofs-in-progress. They can express subgoals, and a command-line tool can report on progress in the form of which proof lines match their results, and details of the mismatch in case of unification failure. It can also help with cleanup by reporting proof lines that are not attached to the final proof tree.

Lastly, the user's choices in breaking a proof into lines will guide the final presentation of a proof. I expect that an initial presentation will include all results as written. Intermediate results (missing result terms or nontrivial arguments) could be expanded using some variant of a disclosure triangle. Also, subterms replaced with "_" could similarly be initially elided but expanded on request. I've given three forms of addeq0, all with the same proof tree, to demonstrate control over conciseness. Of course, labels also give considerable control over the order of presentation for proof lines.

I'm really pleased about the way the "_" label exposes the chained structure common in Metamath-style proofs. For example, a proof of A = D could be written:

proof A=B;
eqtr _ (proof B=C);
eqtr _ (proof C=D)

This seems very intuitive to me, and I think will help illuminate the structure of proofs considerably beyond simply presenting the proof tree.

To sum, I'm excited that this small increment of complexity, structuring proofs into lines each with a result, can help make it significantly easier both to read and to write proofs, especially compared to the old RPN syntax.

Feedback welcome,

Raph
scratch.gh

Adam Bliss

unread,
Jun 4, 2017, 10:19:21 PM6/4/17
to ghil...@googlegroups.com
Very excited. Quick questions:

theorem disjsn: ⊢ A ∪ {B} = ∅ ↔ ¬B ∈ A ::(

Is that a typo or is my phone font rendering \cap as \cup??


theorem id: ⊢ ϕ → ϕ {
    ax_1
    [ϕ → ϕ → ϕ] 「 could be [_ → ϕ → _] 」
    mpd _ ax_1
}

Is the {} just an alternate form of ::( or does it carry some meaning?

Since, for my part, it's very hard to consider these changes statically, how close are we to having a verifier to play with?

--Adam

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Raph Levien

unread,
Jun 4, 2017, 11:46:32 PM6/4/17
to ghil...@googlegroups.com
Both are typos. I originally had {} instead of ::() but realized it would be impossible to disambiguate the former from set notation within a term. Corrected version attached.

I'm not going to make a promise of exactly when, but I'm feeling pretty good motivation. It's likely first version will have no distinct variable checking, and definitely no namespaces / modules, but it should still be possible to play with.

Raph
scratch.gh
Reply all
Reply to author
Forward
0 new messages