The main feature of TryAlgebra is its ability to recognise formulas. Rather than applying formulas manually by rewriting expressions by hand, you simply select the expression to which you want to apply a formula, and choose it from the list of suggestions.
Previously, you created a file containing identities as a template for mathematical expressions, with placeholders that captured the actual values. TryAlgebra then attempts to apply these templates to the selected expression.
Simple string pattern matching, such as that used in regular expressions, is too restrictive. Furthermore, it does not recognize mathematical syntax, which can result in incorrect interpretation and matching. The solution is to parse the expression as a syntax tree, assigning a precedence order to each operator. Although this makes pattern matching more restrictive than simple string matching, fewer expressions will match the structured pattern. However, this approach at least preserves syntax and mathematical rules to some extent.
This still isn't very useful.
We want the system to be more flexible so that it can use some math to determine whether the expression matches the template. For example, it could apply the commutativity or distributivity properties. It could also cancel out something. This would make it really useful.
This is where the term rewriting system comes into play. It works like this: you provide it with basic mathematical identities, which it then uses to match the selected expression against the template.
These systems are used for compiler optimization and simplifying expressions, as well as in computer algebra systems. In fact, the range of applications is not as extensive as I thought. However, the idea and mathematical principles behind them are very powerful and fundamental to the entire field of mathematics. TRS is formalized in math books using notions from 'universal algebra'. This topic is also fundamental and abstracts the entire field of algebra. The main idea is that we do not need to know the actual meaning of functions; we can simply treat them as symbols, and the relationship between them can be described using equivalence classes.
I have currently implemented the TRS using saturation, which is similar to what Egg Optimizer does. Put simply, saturation involves applying identities to parts of the selected expression until it matches the template. There are few significant optimizations involved. The first is the equivalence graph, or e-graph, which stores mathematical expressions and all their rewritten versions in a compact way. The second is the congruence closure. I won't go into detail here, but this property enables more identities to be found without the need to apply mathematical rules. This property operates at a meta level and is applicable to any set of mathematical rules. It is actually a very simple property, but I will write about it in another post.
The example below illustrates how TRS algorithm is used.
It attempts to match '(ac + k)²' with '2ab + a² + b²' using listed identities. It is written in prefix notation; in TryAlgebra you'll be able to apply it to the familiar math notation. As you can see, it finds how to substitute a and b to match expressions modulo identities:
The following posts will provide more details on the main aspects of the TRS. There are actually a lot of interesting things!
Top comments (0)