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

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

Dear Michael,

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

> An interesting possibility opens itself up if equations in Pure are
> first class, which I believe they weren't in Q.

No, in Q they aren't, at least not without emulating Q in Q. ;-)

> I'm not sure if they are in Pure

Well, yes and no. If you restrict your programming to "Pure Pure", i.e.,
the purely functional part of Pure, then no, because adding a new
equation to the running program is a side effect. "Pure Pure" is pretty
much the entire language, except the exception handling primitives
(throw/catch), the "*p = x" kind of operations (put_int et al) in
primitives.pure, and eval in strings.pure. The latter is what's
currently available to add new rewriting rules at runtime, it's not
really documented yet, but I'll have to say more about that below.

> It seems that once could
> build a powerful equational reasoning system on Pure, which would enable
> one to reason about it's functions as defined by rewrite equations, or
> at least the side-effect free ones.

Yes, certainly. What's currently missing is a function in the runtime
which returns the current list of equations, but that information is
readily available (e.g., the "list" command of the interpreter already
uses it) and will be made available to user programs as soon as I get
around implementing a decent interface for the reflection stuff.

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. :(

> This would also be incredibly useful to prove things about types in Pure
> programs, i.e. it would be a way for the compiler of Pure, a dynamically
> typed language, to produce code which is closer to the performance of
> that produced by compilers for statically typed languages such as Haskell.

I seriously doubt that this will be practical, at least on this scale
and for this application (i.e., type inference in Pure). It's not only
that the completion may fail (even with "unfailing" KB completion you
still have to find a term order or valuation under which the rules are
reducing), but all forms of KB are also fairly slow.

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

> Would you be interested in incorporating such an equational reasoning
> engine into Pure?

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.

> On another point, you say that Pure is designed to be more reflective
> than Q. Does/Will Pure include the ability to incorporate the Pure
> compiler/interpeter runtime in a deployed application, so that new code
> can be compiled at runtime? This is one of the hallmarks of Lisp (and
> Smalltalk) and a very desirable feature for dynamic languages.

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

  > using system;
  > foo x y = eval $ sprintf "%s %s = %s+1;" (str x,str y,str y);
  > foo bar 42; foo bar 23;
  eval "bar 42 = 42+1;"
  eval "bar 23 = 23+1;"
  > list bar
  bar 42 = 42+1;
  bar 23 = 23+1;
  > bar 42; bar 23;
  43
  24

As you can see, the interface is a bit icky right now because eval takes
the source code as a string, but it's workable. I'll add more of those
reflection capabilities I promised when I have the time. The interpreter
already has an API to process equations represented in a symbolic form,
I just need to add a routine to the runtime which gives access to that
functionality.

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

Best,
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