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

[Albert G. <Dr....@t-...>]

Michael Ben-Yosef wrote:
> I was imagining something more like an equational theory of combinators,
> with only one binary function symbol, representing composition, and
> plenty of constant symbols representing combinators, with equations
> defining their intended semantics.

Yes, that should be an interesting application, and much more
interesting for cs people than group theory. :)

> As someone with absolutely no
> experience in this, I ask: is KB completion hopelessly inefficient for
> such rich theories?

I have no idea. I've never used KB for anything but trivial examples
which I did using pencil and paper. ;-) Guess you'll just have to try...

Albert

-- 
Dr. Albert Gr"af
Dept. of Music-Informatics, University of Mainz, Germany
Email:  Dr....@t-..., ag...@mu...
WWW:    http://www.musikinformatik.uni-mainz.de/ag