Recognizing when two arithmetic expressions are essentially the same

Re:Recognizing when two arithmetic expressions are essential... by coolio222 on Tuesday August 22, 2017 @06:28PM (#15076915)

You defined rewrite rules that reduce an expression down to a 'normalized' form such that two expression are equivalent if they reduce to the same 'normalized' form. These rules are obvious for simple arithmetic expressions.

Is it possible to deduce the normalized form and the rewrite rules from a set axioms automatically (e.g. for relational (like SQL) expression with operands like join, project, filter)?

[ Parent | on HN ]

Re:Recognizing when two arithmetic expressions are essential... by zmonx on Wednesday August 23, 2017 @04:23PM (#15084729)

In the terminology (may I say: terms) of term rewriting, you are looking for a so-called completion procedure. This takes a set of axioms and turns it into a convergent term rewriting system (or not, because it may not terminate!).

If the completion procedure succeeds, you end up with rules that always terminate, and which reduce any given term to its normal form. In the literature, search for Knuth-Bendix and Huet completion procedure, if you are interested. For SQL, it may get quite complex, but still doable, potentially with some extensions of the primary method.

There are all kinds of variations on the general scheme. If you are interested in term rewriting, a solid starting point is Term rewriting and all that by Baader and Nipkow.

[ Parent | on HN ]

Re:Recognizing when two arithmetic expressions are essential... by coolio222 on Thursday August 24, 2017 @05:01AM (#15088604)

Thank you very much. I checked Wikipedia for Knuth-Bendix and will try to get hold on the book.

[ Parent | on HN ]