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

[Michael Ben-Y. <sep...@mw...>]

Albert Graef wrote:
> (I hope you don't mind that I'm cc'ing this to the mailing list since
> the reply should be interesting for others, too.)

No problem.

> 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).

Thanks. I'll have a look at this.

> I still think that a KB completion module for Pure would be very useful,
> for less ambitious applications in mathematical logic. E.g., if you have
> a little equational theory (a free group, say), and you want to do some
> computations in that group, you really want a complete set of equations
> which decides the word problem in that theory. Group theorists would
> probably be happy with that (although there surely are software packages
> for group theory which already do this kind of stuff).

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. (Hopefully far more than just S, K
and I combinators, of course, so that one can prove theorems about the
sort of simple functions a person might actually write in an "untyped"
functional language, such as Pure itself.) As someone with absolutely no
experience in this, I ask: is KB completion hopelessly inefficient for
such rich theories?

> Yes, I that that a KB completion procedure would be a useful addition.
> It could be just provided as a separate Pure module which programmers
> can load if they need it. But as explained above, I don't see that it
> would be feasible to incorporate it into the compiler itself.

OK, that makes good sense.

> Yes, that already works, you can use the eval function to execute
> arbitrary Pure code at runtime. E.g.:

Excellent. Thank you.

>> I ask because the GPL then requires the resulting application to be GPLed
>> since it includes Pure itself. A more permissive license, such as LGPL
>> or BSD, is in order if Pure is to be used in this way in commercial
>> applications.
> 
> You're right, I haven't thought about that yet. But since I'm the author
> and only copyright holder of the Pure software, I can do that without
> any ado when the issue comes up. I'll probably switch to LGPL then.
> Maybe I should do that right away, I will think about it.

Good to hear.

Kind regards,

Michael