QuantoDerive
QuantoDerive is the new scala-based GUI that will replace the existing Quantomatic GUI. These pages are for planning various aspects of the tool. QuantoDerive uses a project-based idiom for defining systems of axioms and using axioms to perform derivations. A project consists of various JSON files:
-
main.qtheory- details about how a particular theory is visualised and implemented in the core -
*.qaxiom- axioms. Rules that do not need to be proven. -
*.qgraph- graphs. These can be edited and used to start derivations. -
*.qderive- derivations. Conceptually, these are trees, where nodes correspond to a single application of a rewrite rule. -
*.qtheorem- theorems. Rules whose validity needs to be established. This is done by tagging proof heads in derivations with a theorem's name.
For more info on graph, rule, and theory formats, see file formats.
Following the project/IDE style, the (directory or logical) structure of the project is displayed on the side, with a main editing area in the centre. Theories can be modified using three distinct modes of editing, which are activated depending on what kind of file is in focus. The three modes of editing are as follows.
- Graph Editor - for auxiliary and scratch graphs
- Rule Editor - for axioms and theorems
- Derivation Editor - for derivations
A central concept in QuantoDerive is that of validation. For a theorem to be valid, it must be connected to a valid derivation. For a derivation to be valid, every step must be an axiom or another valid theorem. Thus, the validity of one theorem can depend on the validity of another. Clearly this dependency relation must be well-founded, with the bottom elements all axioms. More details are given below.
The graph editor can be run stand-alone or (ultimately) inside of QuantoDerive. Its designed to be as simple as possible, and does not need to communicate with the core. It loads and saves files in the .qgraph file format.
Many aspects of the interface are obvious, so here are suggestions on how to do the less obvious things.
Currently, all vertices are laid out with fixed positions. However, it might be nicer to only give fixed positions for node-vertices and boundaries (i.e. wire-vertices with one or zero adjacent edges), then lay out the intermediate nodes automatically. For multiple wires between two node-vertices, it would look nice to lay out wire-vertices interpolated along the bezier curve of each edge.
The intermediate wire-vertices should be selectable, but not draggable. Deleting a wire-vertex would upgrade its neighbour(s) to boundaries.
!-boxes are add via the Add !-Box tool. With this tool selected, the user can drag boxes around collections of vertices to ! them. They can also be modified when the Select tool is active (TODO: decide whether to let !-box editing be its own tool). !-boxes can be edited in various ways. Most of these have to do with working with the "hot corner" of the !-box, which can be thought of as logical !-node which connects to the contents of the box. (See arXiv:1204.6695 for how this works).
Delete a !-box by selecting it and pressing the DELETE key. Add child vertices or !-boxes by dragging a line from the corner of the !-box to the vertex or child !-box. When a !-box is selected, it will show lines connecting the corner of the !-box to any of its child vertices or !-boxes. Centred on each of these lines is a small X the user can click to remove the child from the !-box. The lines and the X'es should be light and unobtrusive (perhaps becoming darker on mouse-over) to not confuse the eye.
Rules are edited much as before, in a side-by-side manner. One notable difference is that boundaries are visually (and semantically) distinguished from other wire vertices. Boundaries are created by a distinct tool, not available in the graph editor, which creates a boundary in the same physical position on both sides of the rule. The boundary vertices on the LHS and the RHS are then locked to each other, so when the user moves or deletes the boundary on one side, the change occurs simultaneously on the other side.
!-boxes are treated in a similar manner. When they are created/deleted/nested/un-nested, this operation happens jointly. Also, when a boundary vertex is added or removed from a !-box, this happens jointly.
When the user tries to save, the client checks that all other (non-boundary) wire vertices have exactly one input and one output. Otherwise, it will refuse to save.
At any point while editing a graph, the user can click a button to start a derivation. This creates a new derivation starting at the open graph and opens the derivation editor. While performing a derivation, the user constructs a proof history, which is essentially a tree whose nodes are labelled by applications of rewrite rules. It will look something like this:
Unlike the usual notion of a proof, where the history is linear, a derivation is more free-form in that it allows branching. This affords two benefits. Firstly, it allows experimentation while searching for a proof, and secondly, it can succinctly express multiple proofs that start the same way.
A derivation tree has two kinds of nodes: proof steps (shown in black above) which represent a rule that has already been applied, and proof heads (shown in white), which mark a position from which a proof can be continued. What the user sees in the main area depends on what kind of node is selected.
If a proof head is selected, then the current graph is displayed on the left, and available rewrites are displayed on the right. By default, as soon as the user clicks on a head, it starts searching for rewrites in the entire graph. This is done asynchronously so the user doesn't lose responsiveness while this happens. To narrow down the rewrites, the user can select a subgraph and hit spacebar to filter rewrites to only those matching the selected graph. Various other commands for working with subsets of rewrites, etc. are also supported.
A proof step displays the graph prior to rewriting on the left, and the graph after rewriting on the right. On the left, it highlights the section of graph that was removed, and on the right, the section that was added. The user can perform various commands from here.
If this proof step is the last step before the proof head, the user may delete the proof step and roll back to its parent. The user may also create a new branch. In this case, a new proof head is added as a child of the current proof step and the history advances there. If the user navigates away from this proof head without performing a proof step, the proof head is removed.
It also has several buttons for navigating the derivation. Back and forward behave has expected, except in the case where a proof step has multiple successors. In this case, it could either (a) ghost, forcing the user to manually select a successor from the history or (b) prompt the user for which branch to take.
Another alternative would be to show all of the successors on the RHS, each with their own "next" button.
When a project is loaded or changed, theorems may need to be re-checked. Before talking about validating theorems, we define the procedure for validating one rule against another.
A rewrite rule R1 is said to validate R2 if R1 can be used to rewrite lhs(R2) to a new graph H such that there is a boundary-preserving isomorphism between H and rhs(R2). In other words, up to some renaming, R1 can be applied to lhs(R2) to get rhs(R2). In the case where R1 validates R2, the soundness of R1 implies the soundness of R2.
Except in certain corner cases where matching is undecidable (wild !-boxes), the validation problem is always decidable. Naively, this can be done by enumerating all of the possible matchings of R1 on to lhs(R2), rewriting, and performing a graph isomorphism check. In the worst case, rule validation is O(2^(2n)). Fortunately, most validations can be trivialised with some heuristics and a bit of caching.