Universal quantification, impredicative terms,
closed/open worlds, and effects
This note (first written on Oct 14, 2004 and updated on Oct 18, 2004)
discusses universal quantification of variables in the body of a
clause, given open- and closed-world assumptions. We also discuss two
ways of expressing impredicative terms like (exists U. [U,U]), and
`common subexpression elimination' in logical programs. We draw
parallels with effects, of creating logical variables.
We will be discussing Horn-clause--based logical programming systems
such as Prolog, Datalog, and Kanren (kanren.sourceforge.net).
Let us consider the following set of facts (the extensional database,
in Datalog terms):
?- dynamic reqd/2.
student(john).
student(bob).
reqd(cs,cs311).
reqd(cs,cs611).
took(john,cs311).
took(john,cs611).
took(bob,cs311).
took(bob,math101).
and the predicate perhaps_cs/1 defined as
perhaps_cs(X) :- student(X), reqd(cs,Course), took(X,Course).
The predicate is true for all people who are students and took at
least one required CS course.
A Horn clause is a disjunction of literals with exactly one
positive literal. All free variables are implicitly universally
quantified. For example, the clause defining perhaps_cs/1 can be
written in the conventional logical notation as follows
forall X Course. (perhaps_cs(X) or ^(student(X) & reqd(cs,Course)
& took(X,Course)))
==
forall X Course. (perhaps_cs(X) or ^student(X) or ^reqd(cs,Course)
or ^took(X,Course))
Using the standard logical transformation rules, we can re-write the
above formula as
forall X. (forall Course. (perhaps_cs(X) or ^student(X)
or ^reqd(cs,Course)
or ^took(X,Course)))
== { use rule: forall A. (a | b) === a | forall A. b if A does not occur
freely in a}
forall X. (perhaps_cs(X) or ^student(X) or
forall Course. (^reqd(cs,Course) or ^took(X,Course)))
==
forall X. (perhaps_cs(X) or ^student(X) or
forall Course. (^(reqd(cs,Course) & took(X,Course))))
==
forall X. (perhaps_cs(X) or ^student(X) or
^(exists Course. (reqd(cs,Course) & took(X,Course))))
The familiar Prolog rule emerges: variables that occur in the head of
the clause (such as X) are implicitly universally
quantified. Variables that occur only in the body of the clause (such
as Course) are implicitly existentially quantified. In Kanren, the
latter, existential quantification is explicit.
Thus perhaps_cs/1 is indeed true for students who took _some_ required
computer science course. Now we would like to find people who took
_all_ required CS courses. There are two ways of doing this: using
eigenvariables and double negation. There is a subtle difference
between the two methods.
The double negation method (explained, e.g., in Datalog literature):
cs_complete(X) :- student(X),
not((reqd(cs,Course), not(took(X,Course)))).
This clause can be re-written as the following FOL formula
forall X Course. (student(X) & (reqd(cs,Course) -> took(X,Course)))
-> cs_complete(X).
We find that only 'john' has completed all the required courses *that
are listed in the database*. This method takes the closed-world
assumption. The above program is safe in Datalog sense (all logical
variables are range-limited).
A different way of writing cs_complete/1 with the logical variable
Course universally quantified within the body of the clause is to
use the natural deduction [*] rule everyI:
alpha[A/X] ==> forall X. alpha
where A is an eigenvariable.
[*] A Prolog program must necessarily operate in some meta-logic; we
just picked NK.
So, if we wish to express the formula
forall X. (cs_complete_(X) or ^student(X) or
^(forall Course. (reqd(cs,Course) -> took(X,Course))))
in Prolog or Kanren, we write it in the following form
forall X. (cs_complete_(X) or ^student(X) or
^(eigen Course. (reqd(cs,Course) -> took(X,Course))))
Or, in the Prolog notation,
cs_complete_(X) :- student(X), gensym(ccc,Course),
assert(reqd(cs,Course)),
took(X,Course).
The reason for gensym is to make sure that when the formula gets
duplicated during the resolution (e.g., with the conjunction
"cs_complete_(john), cs_complete_(bill)" that may occur in a program),
each copy has its own value of the eigenvariable. In Kanren,
adding an assumption (like reqd/2) to the database is handled far more
gracefully, see for example, proofs in the Kanren example directory.
In order for cs_complete_ to succeed, we need to add an additional
clause to our program:
took(john,X) :- reqd(cs,X).
The clause asserts that john took every CS course -- which is
described in the database *or* may be added into the database in the
future. So, the eigen-variable method takes the open-world assumption.
* copy_term and impredicative terms
Suppose we have a logical program
(1) ok1([U,U]).
okpair(X,Y) :- ok1(X), ok1(Y).
The predicate ok1/1 determines that its argument is OK if it is a list
of two identical elements. The predicate okpair/2 determines if its
two arguments are OK. We can easily verify that okpair([1,1],[2,2])
holds.
We can say: ok1/1 has only one answer, [U,U]. Why don't we precompute
it and inline it? We can try either
(2) okpair(X,Y) :- OK = [U,U], X = OK, Y = OK.
or
(3) okpair(X,Y) :- X = [U,U], Y = [U,U].
From a different perspective: suppose ok1/1 in (1) is a complex
predicate that takes a long time to evaluate. Program (1) invokes this
predicate twice, ok1(X) and ok1(Y). Can we do a `common subexpression
elimination' and re-write (1) into
(4) ok1([U,U]).
okpair(X,Y) :- ok1(Z), X = Z, Y = Z.
Obviously, (2)-(4) work differently from (1), because
okpair([1,1],[2,2]) will no longer succeed.
When Prolog resolves both instances of ok1/1 in (1), it makes two copies
of ok1/1 and ensuring that the variable names are renamed correspondingly
(alpha-converted). Logically, program (3) corresponds to
(5) forall X Y. (okpair(X,Y) or ^(exists U. (= X [U,U]) &
(= Y [U,U])))
whereas program (1), after resolution, is
(6) forall X Y. (okpair(X,Y) or ^(exists U. (= X [U,U])) or
^(exists U. (= Y [U,U])))
==
forall X Y. (okpair(X,Y) or forall U. ^(= X [U,U]) or
forall U. ^(= Y [U,U]))
== {conversion into the Horn clausal form}
forall X Y U U1. (okpair(X,Y) or ^(= X [U,U]) or
^(= Y [U1,U1]))
to move the quantifier forward, we have to alpha-convert bound
variables. We can see now how copy_term comes about.
Suppose however we want to re-write (1) into the following form:
(7) okpair(X,Y) :- okpair1(X,Y,?).
where okpair1/3 is something like
okpair1(X,Y,Z) :- X = Z, Y = Z.
what should we write in place of '?' in (7)?
A straightforward answer would be: (exists U. [U,U]). That is,
okpair(X,Y) :- okpair1(X,Y,(exists U. [U,U])).
Here, (exists U. [U,U]) is an impredicative term. Alas, Prolog doesn't
support impredicative logic. So, we need a work-around. One
work-around is this:
(8) okpair(X,Y) :- okpair1(X,Y,[U,U]).
okpair1(X,Y,Z) :- copy_term(Z,Z1), X = Z1, copy_term(Z,Z2), Y = Z2.
The other work-around is this:
(9) ok1([U,U]).
okpair(X,Y) :- okpair1(X,Y,ok1).
okpair1(X,Y,Z) :- call(Z,X1), X = X1, call(Z,Y1), Y = Y1.
We're essentially using the second-order logic (variable
predicates). This is precisely the solution in the
kanren/examples/type-inference.scm
One should emphasize the equivalence of (8) and (9). Furthermore, (8) is
an `optimal' form of (9), where the predicate ok1 is in the `solved'
form. Both (8) and (9) are two ways of emulating (exists U. [U,U]).
A different view of looking at this is from the point of view of
effects. As Chung-chieh Shan pointed out, there is one effect in Kanren:
creating of a logical variable. So, if we have an expression "ok1(X),
ok1(Y)" and we know that ok1/1 is effect-free (that is, it creates no
logical variables), then we indeed can do common-sub-expression
elimination and write it as "ok1(X), X = Y". OTH, if ok1/1 is
effectful, we can factor the call to ok1/1 out only if we perform the
same effects as before. That's what copy_term is for.