A Formal and Precise treatment of Simplification? I am looking to gain a deeper understanding of, and increase my own skill in "Mathematical Simplification". But I've been finding the concept overly vague and haven't been able to find any good resources myself.
Here are some of the questions/ideas I am attempting to clarify:
-When exactly is a number or expression considered "Simpler" than another?
-What are common and useful techniques for Simplification?
-How much of Simplification is Objective and how much is Subjective?
-Is there a generalization of Simplification that covers much more of Mathematics then basic Arithmetic and Algebra? (Say from the perspective of Set Theory, Category Theory, Abstract Algebra etc.)
My question can best be summed up by asking if there are any detailed, formal and rigorous explanations of Simplification? If there isn't, why is that so? Is this concept of "Simplification" that textbooks seem to assign such paramount importance simply an artifact of "school-math" that proper mathematicians don't concern themselves with?
Suggestions of external resources and/or personal insight are both appreciated.
 A: You might be interested in term rewriting. The idea is to consider expressions called terms which can basically model any kind of mathematical expression and congruences between these terms. The ultimate goal of this theory is to provide methods to decide whether two terms are congruent, by orienting each congruence $t\simeq u$ into a rewrite rule $t\rightarrow u$, and applying many such steps to find a common reduct $w$, we write
$$ t\rightarrow^* w\ \ ^* \!\leftarrow u$$
For this to be a procedure, we commonly require two properties:


*

*Confluence: if $t \rightarrow^* v $ and $t \rightarrow^* u $ then there is some $w$ such that $ u\rightarrow^* w\ \ ^* \!\leftarrow v$

*Termination: there is no infinite sequence
$$ t_1\rightarrow t_2\rightarrow t_3\rightarrow\ldots$$
Given these two properties, the decision procedure for deciding congruence is simple: take both terms and rewrite them as much as possible. This will be a finite process, by termination. By confluence, it is not too difficult to see that the final terms obtained will be identical if and only if the original terms are congruent.
Now for your question: over the years, people have developed a great many mathematical (and programmatic) tools to help one determine termination of a set of rewrite rules. The most common way to do this is to determine a certain relation $R$ on terms, which verifies $t \rightarrow u \Rightarrow t R u$. In this sense, every such tool gives a precise definition of what it means for $t$ to be simpler than $u$: it is the statement $t R u$. Note that this relation can be significantly more complex than simply syntactic size: the relation
$$\sqrt{a} - \sqrt{b}\quad R\quad \frac{a-b}{\sqrt{a} + \sqrt{b}} $$
can be seen as a simplification, as the number of differences of square roots is strictly smaller in the right expressian than in the left. The wikipedia page gives some more examples, and Baader & Nipkow give a rather comprehensive overview.
