Comment by hyperpallium2 | Hacker News Reader

Comment by hyperpallium2 | Hacker News Reader

I want to write a term rewriter for algebraic equations (just commute, assoc, distr, etc), but I wonder about the UI: the best way for a user to specify which parts to transform?

Here's the obvious ways I've thought of - have I missed some?

- Derivations are usually written as before and after, and sometimes the name of the transform, and the reader must work out the arguments. Could have the program check the transform... but I'd like to save the user all that rewriting...

- You could specify the arguments with a function at that point (using location to address them). Seems just as bad.

- An awkward path through the parse tree to specify each argument is also possible.

- In a GUI, arguments could be selected by clicking.

- The user could name the transform, and the program automatically find where it is applicable, and apply it - or give a list of applications, and the user selects which one. But this is a step towards an automatic theorem prover, and is more automation than I want the user to have.

Are there other ways?

I was thinking something close to Haskell pattern matching with some variation.

Ex:

AdditionRule (x :: NumericExpr) + (y :: NumericExpr) = eval(x) + eval(y)

It's been a while but I also remember seeing a concise DSL for tree rewriting in the ATLR compiler. It also had escape hatches for things like context and precedence calculations.

In terms of GUI and clicking, I think it might need to be more sophisticated than that.

What does clicking mean when you are a clicking on a sum type? Is it just that variant of the ADT, the entire type?

What about for complex expressions? Are you selecting just a term in that complex expression or the entire expression?

I suppose if you were looking at a tree visually then you could select a lot easier.

Seeing how other languages do "destructuring" or "pattern matching" might provide other possible alternatives.

That's sophisticated! I'm thinking highschool algebra, like

  a+b     = b+a
  (a+b)+c = a+(b+c)
  a.c+b.c = (a+b).c

Defined by that literal text. Applying them is the step I'm wondering about...

One difficulty comes above the target, when it's not the root. e.g. wanting to commute the target a+b in

  x.(y + z.(a+b))

The other difficuly lies below the target, where each letter in the above rules can represent an arbitary expression - so it's awkward to tell which expression is meant by clicking on it (as you note).

So I'm thinking of clicking on an operator, to uniquely select its two operands - that would work for commute. Other gestures, like long-click, double-click, drag-n-drop etc may be enough. Pop-up menu for the worst case!

I think, the Haskell example defines a rule, rather than applying an existing one? I think, too, a DSL for transforms in ANTLR also would be for defining them.

Similarly, I think destructuring is a kind of definition. The 3 rules defined above are pretty much destructuring and constructuring (heh). The difference is in usage or application: in a program, you need to supply the target as the root, but in highschool algebra, it can be at any depth in the expression.

I think you'd be best by defining two classes of rules. The first would be simplifications, and these you want to apply as much as possible. The second would be definitions, which can be used to help make simplifications possible, but otherwise should not be applied just because.

Not sure what you mean.

Sometimes you need to "complexify" to put an expression into a form in which you can do something, then simplify it back. You can even generate new terms out of nothing (because b = b + 0 and 0 = a + (-a)) to obtain a specific form. The simplist example I can think of is completing the square:

To get minimum of x^2 + 2x + 2:

  x^2 + 2x         + 2  =
  x^2 + 2x + 1 - 1 + 2  =
     (x+1)^2      + 1
  because (x+1)^2 >= 0, minimum is 1

So it's important that equivalences like ax+bx = (a+b)x can be applied in either direction - not just in the left-to-right, simplifying direction of factoring, but also the right-to-left direction of expansion.

BTW If always "simplifying", the process is contained, and the possibilities are limited. But because of expansion and generation, it is unconstrained, and can be anything.

I think of "definitions" as defining the meanings of new syntax - in effect, they are lemmas. Can you elaborate on what you mean by them?

BTW the option to automatically apply simplifications would be useful in an assistent tool. But what I'm aiming at is a facilitation of each tiny tedious step - so it's not quite as tedious, but you aren't skipping anything.

I thought I understood your problem statement as something along the lines of "How do I stop the rule (a+b)->(b+a) from firing just because they can". So my proposal was to only attempt to apply certain rules if they helped reach the goal, where the goal was simplification. They would not fire in and of themselves, but always in a chain that ended in some desired simplification rule also firing.

Thanks for explaining. I want the user in manual control, and the problem is how the user specifies what is to be done.

I did entertain some automation as one way to achieve this: to present a set of different things that could be done - and the user could select from that set, instead of specifying the details explicitly. It's not my preferred approach, because it suggest/hints more to the user than I want to ... but it is a solution to the specification problem.

I think I can see your suggestion as a refinement of that approach, of not blindly listing every possible next step, but just the most useful ones. And further, selecting from a set of different series of rule applications. One could also rank them.

Your version of the problem is appropriate for a proof assistent - but I'm aiming at something quite a bit more rudimentary!

----

BTW my motivation for this project is partly to get clear on some formal aspects of proof - the mathematics I've studied so far has only formalized some domains, but not proof itself.

I can also feel it as a fun game, to be able to transform expressions... though whether that turns out to be the case remains to be seen!

The `traces` procedure from Redex displays a navigable graph of all applicable transformations and their result.

https://docs.racket-lang.org/redex/The_Redex_Reference.html#...

Reply on news.ycombinator.com