You wrote:
> It's decidable whether two NAND circuits implement the same function, I'm pretty sure it's not decidable if two EML trees describe the same function.
Perhaps, perhaps not, same function so basically is this question solvable:
A(x[,y,...]) = f(x[,y,...])-g(x[,y,...]) == 0 everywhere?
if a user brings EML functions f and g; given their binary EML trees; can we decide if they represent the same function, so the question form is
A(x)=0 EVERYWHERE?
(like given 2 fractions a/b == c/d ? do the fractions represent the same fraction?)
From Wikipedia link reikonomusha gave:
> Miklós Laczkovich removed also the need for π and reduced the use of composition.[5] In particular, given an expression A(x) in the ring generated by the integers, x, sin xn, and sin(x sin xn) (for n ranging over positive integers), both the question of whether A(x) > 0 for some x and whether A(x) = 0 for some x are unsolvable.
Here the question forms are
1) exist x such that A(x) > 0 (does there exist an x where A(x) becomes positive?)
2) exist x such that A(x) = 0 (does there exist a value such that A(x) becomes 0? or basically find real roots
so at least the forms on WikiPedia don't generate the results both of you claim it does.
it does present undecidability results, but not straightforwardly in the context of this EML work.
second the Richardson's theorem is about the function on the reals, not complex functions (I mean the roots must lay somewhere)