3 ms·

I was thinking something close to Haskell pattern matching with some variation. Ex: AdditionRule (x :: NumericExpr) + (y :: NumericExpr) = eval(x) + eval(y)

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

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