Re: [pure-lang-users] Rewrite system completion in Pure?

[Gregory M. T. <mi...@pa...>]

Albert Graef <Dr....@t-...> sed:
> There's however a practical issue there, due to the way term pattern
> matching is implemented in the Pure compiler (which essentially is the
> "left-to-right term acceptor" technique I invented for my master thesis,
> see my article in the RTA 91 proceedings, Springer). This technique
> yields very fast matching code (an essential prerequisite for a TRS
> programming language), because it's deterministic (non-backtracking).
>   >.>><>>>> > *But* there are pathological cases of term sets where the automata are
> exponential in size (that's also discussed in my paper). Now if you
> start adding lots of overlapping equations to the running program, as
> any form of Knuth-Bendix completion typically does, it might hit that
> wall and the dynamic compilation as well as the program itself will
> become very slow and unusable. :(

Does this problem only happen when the equations are added at
run-time?  If so, why?