Solid Intuition/AC

From SE Wiki
Jump to: navigation, search

Associativity and Commutativity (Symmetry)

Status Quo

When doing formal proofs on paper, the associativity of operators is usually taken into account by simply dropping the parenthesis around expressions. This makes reasoning intuitively easy while still being fully formal. The form a+b+c can be seen as normal formal for expressions (a+b)+c and a+(b+c).

Symmetry on the other does not have a normal form and is usually handled on paper by just applying the law a+b=b+a implicitly without mentioning it explicitly.

Handling in the proof tool: first attempt

Both issues can be handled in a very straight-forward way which does not require much extra work in implementing and explaining the tool: for associativity we can always use the normal form; for symmetry we can have the law of symmetry shown as first match (when it applies) and be invoked with a simple touch of key "1" (for "apply first matching step"). When viewing the full proof, symmetry steps (like other "minor" steps) can simply be hidden from the presentation using the mechanism which is provided for hiding trivial steps anyway.

Feature Interaction

The straight-forward way of handling associativity conflicts with our specification of zoom in which every expression has a top-most operand and we can zoom into either argument of it. Now we could see an associative operator as an n-ary operator and zoom directly into the subexpressions below, i.e. from a+b+c zoom directly to a, b, or c without passing via either a+b or b+c. But the problem is that for applying laws we sometimes just 'want' to focus on a+b or b+c. A simple example being the application of the symmetry law. Another problem is unification: for example, applying the symmetry law to a+b+c could lead to either b+c+a or c+b+a, depending on which association is chosen.

Compromise for first Prototype

Both associativity and symmetry have to be explicitly invoked via the standard mechanism of making a proof step. This makes best use of existing functionality and avoids feature interaction. A helpful addition is to display superfluous parenthesis in grey or only when the mouse hovers them; this ensures that a unique tree structure is preserved, no feature interaction occurs, but the screen looks still quite clear. A better mechanism for AC can be thought-out once the basics of the tool are working and can be played around with.

The following example shows that this is not much of a loss. In the expression "a+b+c" we can either zoom on "a" or "b+c" or we can zoom on "a+b" or "c". Since zoom is done on the simple click of a button "left" or "right" we need some extra user-action to choose which parenthesizing we want to assume. Given that application of a law is also done with a simple click of a button this action can as well be the choice of the Associativity Law. This has the advantage of using two simple separate gestures and interaction with other features is immediately clear. (For instance, it takes three small gestures to zoom on "b" but then there is no doubt whether zooming out leads to "a+b" or "b+c" because one of them was an intermediate step and that's what we also pass on our way back.)