Consider the following language of expressions:
$$ v ::= a | b | c ... $$
$$ e ::= 0 | v | e + e | e - e | max(e, e) | min(e, e)$$
For example, we can form the expression $max(a, min(b, c)) - d$.
Each such expression semantically defines a function from $\mathbb{R}^n \to \mathbb{R}$ by interpreting the expression, e.g. $f(a, b, c, d) := max(a, min(b, c)) - d$.
Is there a normal form for such expressions?
If there is none, is there an algorithm to decide whether the functions coming from two such expressions are identical? For example, $max(a, a)$ and $a$ give the same function, and so do $max(min(a, b), min(c, b)$ and $min(max(a, c), b)$.
If there is no such algorithm, is there a complete set of rewrite rules (identities) such that two expressions with equal functions can be transformed into each other?