On 16 May 2009, at 03:54, wren ng thornton wrote:
Conor McBride wrote:
Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway)
But unification is what you get by adding non-linearity.
Hang on a minute: we're solving for sb in sb(p)=v not in sb(s)=sb(t)...
Sure, all terms are ground;
...which makes it a rather special and degenerate and unawesome case of unification: the kind of unification you don't need a unification algorithm to solve.
would you prefer I said "testing for membership in an element of the RATEG class"?
I'm not familiar with that terminology, but I'll check out the link.
For more ickiness about RATEG, it's not closed under compliment and the emptiness problem is undecidable (so dead code elimination can't always work). Even restricting to the closed subset (aka "tree- automata with (dis-)equality constraints") leaves emptiness undecidable, though there are a couple still more restricted classes that are decidable.
cf ch.4 of TATA http://tata.gforge.inria.fr/
Let's be clear. The suggestion is only that a slightly more compact notation be permitted for functionality already available via guards or view patterns. It cannot introduce any dead code elimination problems which are not already present. I'm sorry, but I just don't see the bogeyman here. All the best Conor