3 ms·

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 p

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?

jswrenn 6y ago
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#%28def._%28%28lib._redex%2Fgui..rkt%29._traces%29%29 https://docs.racket-lang.org/redex/The_Redex_Reference.html#...
bcheung 6y ago
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.
- hyperpallium2 6y ago
  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.
  - jdmichal 6y ago
    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.
    - hyperpallium2 6y ago
      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.

jswrenn 6y ago

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#%28def._%28%28lib._redex%2Fgui..rkt%29._traces%29%29 https://docs.racket-lang.org/redex/The_Redex_Reference.html#...

bcheung 6y ago

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.

hyperpallium2 6y ago
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.
- jdmichal 6y ago
  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.
  - hyperpallium2 6y ago
    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.