jjourdan@a.gp.cs.cmu.edu (Jean Jourdan) (08/25/90)
Hi All, Could someone tell me something about Partial evaluation and Negation as failure with a Closed World Assumption. Is it a such problem solver sound? If yes, could you give a quick prove to me. Thanks in Advance. Jean Jourdan jjourdan@cs.cmu.edu
vu0310@bingvaxu.cc.binghamton.edu (R. Kym Horsell) (08/25/90)
In article <10319@pt.cs.cmu.edu> jjourdan@a.gp.cs.cmu.edu (Jean Jourdan) writes: >Could someone tell me something about Partial evaluation and Negation as >failure with a Closed World Assumption. Is it a such problem solver sound? >If yes, could you give a quick prove to me. Partial evaluation is a rather beautiful area of symbolic computation. In essence, given a program that performs some computation, PE determines what the program is that performs the same computation with some (or all) of the inputs pre-defined; i.e. it produces a ``specialized'' version of the original program. PE is not limited per se to any particular language (i.e. it can deal with FORTRAN as well as PROLOG or LISP). The *real* beauty arise from using a partial evaluator written in the same language that it (partially) evaluates. All sorts of interesting possibilities arise from this area -- automatically generating compilers, etc. being the most obvious. A lot of work pn this stuff is done ``way up north'' in Denmark, etc. Negation as failure/closed word is an unrelated topic (as far as I can see). It provides a method for implementing a form of negation easily. Instead of having to keep track of statements known to be true and those known to be false (with the inherent danger of ``knowing'' something to be both) the closed world assumption says that anything that can't be proved (true) must be false. Due to incompleteness in usual theories a rather large hole is left for those ``statements which cause a loop in theorem provers''. If we adopt the closed world assumption then negation, in languages like Prolog, is simply performed by determining whether or not we *can* prove a statement. In trying to prove not(X) we try to prove X -- if we can't (i.e. X ``fails'') then not(X) is assumed to be proved. It can be shown that this technique is sound if (iff?) X is ground (i.e. contains no uninstantiated variables). For example: not(X=1) in *original* Edinburgh Prolog produces the result ``no''. Prolog's logic here is that X=1 succeeds (presuming X is unbound, of course) so therefore not(X=1) fails. Some versions of Prolog (and these are becomming common now) *delay* the evaluation of negated goals until they are ground -- in effect we only try to decide not(X=1) when X has been given a value. Hope this helps, -Kym Horsell