Drew McDermott <drew.mcdermott <at> yale.edu> writes:
> Are you sure you need to build the bodies of functions at run time?
I think so. My application is as follows:
I have a theorem prover that does rewriting
on terms of a logic. A term "f(g(x))" is represented in
LISP as '(f (g x)) and I have rewrite rules like "f(g(y)) =>h(y)".
The relevant function symbols (here f,g,h) and their arity as
well as the set of rewrite rules are specified interactively by the user,
so they (occasionally) change during the run of my prover.
Now the implementation of rewriting is as follows:
Generate a Lisp function f for every function
symbol f. Calling f with a term t as argument
rewrites the term "f(t)". If the only rewrite
rule that has f as the toplevel function symbol on the
left side is f(g(y)) => h(y) then this function does
the following: Check if the argument x has the form '(g u)
with some term u. If not just return '(f t) otherwise
call Lisp function h on u to simplify the term '(h u).
So the generated code for f is
(lambda (x)
(if (eq (car x) 'g) (g (cadr x)) `(h ,(cadr x))))
Rewriting any term "f(t)" is now done bottom-up by
simplifying the argument t first and then applying lisp function f
to the result. This strategy of generating code is SIGNIFICANTLY
more efficient than the usual strategy of interpreting
rewrite rules (as most other theorem provers do), so I
don't want to lose it.
The code I have now calls a function "generate" with the
rewrite rules of f, which gives the lambda expression above
as result and then calls "(comp f code)". comp is defined as
(defun comp (f lambdaexp)
(if (heuristis-says-compile f)
(compile f lambdaexp)
(setf (symbol-function f) lambdaexp)))
Some heuristic says whether it is more efficient to
invest the time to compile f, making execution more
efficient, or whether executing the interpreted code
is better.
I should mention, that this isn't even the full truth:
actually, before the first call to f, f is defined as
'(lambda (x) (comp f (generate rewrite-rules-of-f)) (f x))
to avoid generating the (usually complex) lambda expression at all, if f
is never called (I typically have specifications with some hundred function
symbols and several thousand rewrite rules). Function generate
is rather complex (around 5000 lines of code) since actually
terms of a higher-order logic are rewritten modulo associativity
and commutativity, so I don't want to do a complete reimplementation.
Changing a rewrite rule for f causes recompilation of f,
so I need to dynamically change the function definition.
To debug the rewriting I can simply call the appropriate
function on toplevel, trace the function calls etc. which
is very convenient. That seems impossible to me if I use
local functions.
Gerhard
P.S. I'm sorry if this message opens another thread,
I tried to post a followup using my Mozilla
browser, but it get an error about "top-posting",
and can't find a way to avoid it.
