Choice Rules and the Belief-Based View of ASP, Part 1

Date: 11 Oct 2010
From: Vladimir Lifschitz
To: TAG

Last week, Torsten Schaub wrote to us about a new release of the ASP
grounder Gringo.  Version 3 of Gringo is a wonderful system, and its
input language combines some of the attractive features of the input
languages of lparse and dlv.

Like dlv, Gringo-3 will not complain about "weakly restricted rules,"
such as those found in the standard definition of transitive closure:

q(X,Y) :- p(X,Y).
q(X,Z) :- q(X,Y), q(Y,Z).

There is no need to add domain predicates to the body of the second
rule.  When TAG discussed solving the Hitori puzzle using ASP, Wolfgang
Faber wrote (in the message dated October 16, 2006): "domain predicates
are evil."  The role of domain predicates in Gringo-3 is more limited than
in lparse and in Gringo-2.

On the other hand, Gringo is similar to lparse in that it allows us to
use choice rules.  We can express, for instance, that q is an arbitrary
subset of p by writing

{q(X)} :- p(X).

This beautiful construct, invented in Helsinki in the early days of ASP,
plays an important role in the "generate-and-test" programming methodology:
we generate by choice rules and test by constraints.  But it has never
been added to the input language of dlv, apparently because its designers
prefer the generalizations of the answer set semantics that have the anti-
chain property (one answer set cannot contain another answer set of the
same program).  In the language of dlv, the idea that q is an arbitrary
subset of p would be expressed using disjunction and strong negation:

q(X) v -q(X) :- p(X).

It seems that the input language Gringo-3 is a step towards convergence
between the two most widely used ASP languages.  The next step in this
direction (and Ronald Kaminski tells me that this is being considered)
would be to include dlv-style aggregates in the language of Gringo.  In a
dlv program, we can write

    #count{X:p(X)}=1

to express that that p is a singleton.  Gringo, like lparse, offers the
user cardinality constraints instead of the #count construct.  They allow
us to talk about the number of atoms in an answer set, but not directly
about the number of values of a variable satisfying a given condition.
And cardinality constraints involve domain predicates, which, according
to Wolfgang, are evil.

=========

Date: 12 Oct 2010
From: Michael Gelfond
To: Vladimir Lifschitz

Loosening some restrictions on domain predicates is great.
I also like the DLV way of treating aggregates.

I however do not find the concept of choice rule beautiful --
even though of course it is a very important discovery/invention.

Partly my feeling can be caused by difficulties I had defining this  
construct to undergraduates. But this was a long time ago -- better
definitions could have been found.

So it will be useful if you could comment on this.

=========

Date: 12 Oct 2010
From: Vladimir Lifschitz
To: Michael Gelfond

I would explain the intuitive meaning of the rule

{q(X)} :- p(X)

like this: for each object with the property p, decide arbitrarily whether
it has the property q.

=========

Date: 19 Oct 2010
From: Michael Gelfond
To: Vladimir Lifschitz

Suppose your program consists of

p(a)
p(b)

and the rule

{q(X)} :- p(X).

According to your reading I expect answer sets (I only show q):

{-q(a),-q(b)}
{q(a), -q(b)}
{-q(a), q(b)}
{q(a), q(b)}

This is what will happen with DLV's version of the program.
But according to you deciding that "a does not satisfy q" is not  
recorded as -q(a).  Why?

=========

Date: 20 Oct 2010
From: Vladimir Lifschitz
To: Michael Gelfond

You noted that the answer sets of the program

p(a).
p(b).
{q(X)} :- p(X).

are

p(a) p(b) 
p(a) p(b) q(a) 
p(a) p(b) q(b) 
p(a) p(b) q(b) q(a) 

rather than

p(a) p(b) -q(a) -q(b)
p(a) p(b) q(a) -q(b)
p(a) p(b) -q(a) q(b) 
p(a) p(b) q(b) q(a) 

Why, are you asking, deciding that a or b does not satisfy q is not
recorded as a negative literal?

The way I see it, in ASP programs we use predicates of two kinds, let's
call them "symmetric" and "asymmetric".  The fact that an object a does
not have a property p is reflected by the presence of -p(a) in the
answer set if p is "symmetric", and by the absence of p(a)  if p is
"asymmetric".  In the second case, the classical negation of p is not
used in the program at all.  In our example, is asymmetric.  If we want
to make it symmetric, we'll add the closed-world assumption rule

-q(X) :- p(X), not q(X).

There are many examples of asymmetric predicates in serious applications
of ASP.  I suspect, for instance, that in the USA-Advisor the predicates
system/1, link/3, jet_of/2, direction/2, tank_of/2, maneuver/1 are
asymmetric.  Are the classical negations of these predicates ever used
in the program?

========

Date: 22 Oct 2010
From: Michael Gelfond
To: Vladimir Lifschitz

It is interesting.  I never thought in terms of what you call symmetric and
asymmetric predicates.  I am not sure it is necessary though -- DLV's
approach to "choice  rule" does not require this distinction.

> I suspect, for instance, that in the USA-Advisor the predicates
> system/1, link/3, jet_of/2, direction/2, tank_of/2, maneuver/1 are
> asymmetric.  Are the classical negations of these predicates ever used
> in the program?

Probably they are not. But this, in our mind, was not related to  
asymmetric predicates.

There are several possible reasons for not using classical negation in  
the USA advisor.

The first (but the least important one) may be simply sloppiness.

The second one is more important.  Our main concern at the time was
efficiency. So, according to our standard methodology we would first write
epistemologically correct representation of knowledge (which will contain
classical negation and proper CWA rules and will mostly be an ASP version of
AL action description) and after that transform this representation into an
equivalent one to make it faster, e.g., drop CWA's and in some places
replace classical negation by NOT.

Equivalence was precisely defined.

What you refer to as "the program" was viewed by us as a collection
of  LP-functions -- or in current terminology collection of modules.
LP function had a collection of input and output predicates and was viewed
as a mapping from some domain -- set of collections of input literals --
to the set of collections of output literals.

So programs were defined as equivalent if they define the same function.

Predicates link, tank, occurs, etc were input predicates; "holds" was an
output predicate.

But in the beginning we would have CWA for, say,  relation "tank".
So if we wanted to ask the query

tank(a)

the program will be able to derive

tank(a)

or

-tank(a)

and answer YES or NO respectively.

After the CWA was dropped then, if tank(a) were not derivable, the program
would answer UNKNOWN.  The answer will not be epistemologically correct
which was o.k. since "tank" was not an output predicate and no
epistemological correctness was promised for such query.

========

Date: 24 Oct 2010
From: Michael Gelfond
To: Vladimir Lifschitz

Here is a follow up to my previous message.  It is a little lengthy but it
contains a new definition.

Vladimir writes:

"I would explain the intuitive meaning of the rule

{q(X)} :- p(X)

like this: for each object with the property p, decide arbitrarily  
whether it has the property q."

Michael:

This does not sound as the usual reading of ASP rule.

I normally read a rule as a constraint on a set, S, of beliefs
of a rational agent "if S satisfies the body of the rule then
it must satisfy its head". Other understanding of S is possible
but the rule still says "if S satisfies the body then it satisfies
the head".

So some time ago I suggested to a version of the choice rule:

rule of the form:

{q : p}

read as

"q is a subset of p".

The definition I gave to this construct in Representing Knowledge
in A-Prolog was rather short and, I think, easy to explain.  It was
however limited to programs without classical negation.

Here is a brief attempt on generalize this definition to programs
which have both negations.

Set S (of ground literals) satisfies {q : p} if for every term t

1. if q(t) in S then p(t) in S
2. q(t) in S or -q(t) in S

The second rule is justified by the fact that our set q is exact --
i.e. membership in it is fully defined.  (If one wants to consider sets
which are not exact the definition can probably be modified accordingly.)

For simplicity assume that atoms of the form {q:p} only occur in the  
rules' heads.  Reduct, r(P,S), is obtained from a program P by

1. Replacing all rules of the form

{q : p} :- body

where {q : p} is not satisfied by S by

:- body.

2. Replacing every remaining rule of the form

{q : p} :- body

by

q(t) :- body

for every t such that p(t) in S,
and

-q(t) :- body

for every t such that p(t) is not in S.

DEF:
S is an answer set of P if it is an answer set of r(P,S).

As expected, program P1:

p(a).
p(b).
{q(X) : p(X)}.

will have answer sets:

p(a) p(b) -q(a) -q(b)
p(a) p(b) q(a) -q(b)
p(a) p(b) -q(a) q(b)
p(a) p(b) q(b) q(a)

It is interesting to look at the program P2

p(a).
q(b).
{r(X) : p(X)}.
{r(X) : q(X)}.

and compare its answer sets defined by the new definition to that
of lparse.

The only "new" answer set the program has is

{p(a),q(b),-r(a),-r(b)}

which corresponds to the new intuition.
Set r is required to be the intersection of p and q, i.e.
r is the empty set.

Smodels however will return four answer sets.
If we add CWA for r (as I think you suggested) we will still
have four answer sets.

So the suggested reading of the choice rule differ from
that of lparse not only in the treatment of classical negation.

Note also that the programs of this language still
have anti-chain property (which in my mind correspond to rationality
principle -- believe nothing you are not forced to believe) which
is not, of course, the case with lparse definition.

Any comments?

=========

Date: 24 Oct 2010
From: Paul Fodor
To: Michael Gelfond and Vladimir Lifschitz

Michael, I think you made a mistake here.

> 2. Replacing every remaining rule of the form
> {q : p} :- body
> by
> q(t) :- body
> for every t such that *p(t)* in S,
> and
> -q(t) :- body
> for every t such that *p(t)* is not in S.

For example, according to your transformation the following program and the
result set S={p(a),p(b)}

{q(X) : p(X)}.
p(a).
p(b).

the transformation would be:
q(a).
q(b).
p(a).
p(b).

which doesn't have S as a result set.

So, you probably meant:
 q(t) :- body
 for every t such that "*q(t)*" in S,
 and
 -q(t) :- body
 for every t such that "*q(t)*" is not in S.

------------------------
I saw your emails and I found them very interesting. The symmetric and
asymmetric predicate issue is related to the fact that the result is
considered in a 2-valued or 3-valued mapping. So, in fact, Vladimir wants a
3-valued interpretation (where predicates can be declared symmetrical
or asymmetrical; or considered by default asymmetrical unless they is a
definition to define them as symmetrical).
Next, Michael saw {q : p} as a literal (it can be satisfied or not, and when
is satisfied then "q is a subset of p") and Michael showed a semantics
and considered that if {q : p} is satisfied, then q must be totally defined,
that is "for every term t, either q(t) in S or -q(t) in S". However, he says
that the most general case can be defined in 3-valued interpretations
without that consideration in mind.

> Here is a brief attempt on generalize this definition to programs
> which have both negations.

Maybe other uses of classical negation may be useful:
-{q : p}
{q : -p}
{-q : p}
{-q : -p}
as literals.

with meanings like these:
- when -{q : p} is satisfied, then "q is not a subset of p",
- when {q : -p} is satisfied, then "q is a subset of the complement of p" in
a 2-valued interpretation, or "q is a subset of the set of atoms p(X) known
to be false" in a 3-valued interpretation (I think that even "{q : not p}"
might make sense in a 3 valued interpretation, possibly something like "q is
a subset of the set of atoms p(X) not known to be true").
- when {-q : p} is satisfied, then "the complement of q is a subset of p",
- when {-q : p} is satisfied, then "the complement of q is a subset of the
complement of p",
or something else in other interpretations.

Probably, defining formally all these uses would clarify a lot of things.

=========

Date: 24 Oct 2010
From: Michael Gelfond
To: Paul Fodor

You are absolutely right -- this is a typo.  Your correction is right.
Thanks!

I am glad you liked the discussion.  I also think that working this out
carefully maybe very useful (and not terribly difficult) -- if someone is
interested in doing this with me (and possibly in implementing this in
some existing system) please let me know!

=========

Date: 24 Oct 2010
From: Vladimir Lifschitz
To: Michael Gelfond

Thank you for your interesting comments.  A few more remarks and questions
about choice rules and the symmetric/asymmetric distinction.

1.  In an ASP program, we usually associate a sort with every argument
position of every predicate.  Sorts are not part of the official semantics
of the existing ASP languages; sorts are simply a special case of unary
predicate symbols.  But the intention to treat a predicate as symmetric
doesn't have a precise meaning until we assign sorts to its arguments.
For instance, in a blocks world planning program we may write on(B,L,S) to
express that block B is at location L at step S.  The set of locations
includes all blocks plus the special location "table".  The answer sets of
our program may include neither the atom

on(table,table,0)

not its strong negation, but we will not understand this as incompleteness
of information: we are not in doubt about whether the table is initially on
top of itself!  The predicate on/3 is treated as symmetric

   * relative to the view that its first argument is of sort "block" *

which does not include "table", not of the sort "location" which does.

A sort predicate can be viewed either as asymmetric, or as trivially
symmetric: relative to itself.  Either way, there is no need to use the
strong negation of a sort predicate in the program.

2. You propose a semantics of choice according to which the program

p(a).
q(b).
{r(X) : p(X)}.
{r(X) : q(X)}.

has one answer set:

{p(a),q(b),-r(a),-r(b)}.

It seems that the counterpart of your approach can be represented in the
language of smodels/clingo as follows:

p(a).
q(b).

{r(X) : p(X)}.
:- r(X), not p(X).       % prohibit non-subsets of p
-r(X) :- p(X), not r(X). % CWA

{r(X) : q(X)}.
:- r(X), not q(X).       % prohibit non-subsets of q
-r(X) :- q(X), not r(X). % CWA

3.  You write that the anti-chain property of answer sets reflects the
rationality principle, "believe nothing you are not forced to believe."
It appears then that your general approach to logic programs--seing rules
as constraints on a set of beliefs of a rational agent--is in conflict
with using any programming constructs violating the anti-chain property.
Would you agree with this?  If so, we face a dilemma: either reject
smodels-style choice rules, or reject your philosophy of logic programming.
That would be a pity, because I like both!

=========

Date: 24 Oct 2010
From: Michael Gelfond
To: Vladimir Lifschitz

> 1.  In an ASP program, we usually associate a sort with every argument
> position of every predicate.  Sorts are not part of the official semantics
> of the existing ASP languages; sorts are simply a special case of unary
> predicate symbols.

As far as I understand this is not a typical view. Often sorts are
treated differently from unary predicates.  The main difference is that
negations of atoms formed by sorts are simply not part of the language.

> But the intention to treat a predicate as symmetric
> doesn't have a precise meaning until we assign sorts to its arguments.
> For instance, in a blocks world planning program we may write on(B,L,S) to
> express that block B is at location L at step S.  The set of locations
> includes all blocks plus the special location "table".  The answer sets of
> our program may include neither the atom
>
> on(table,table,0)
>
> not its strong negation, but we will not understand this as incompleteness
> of information: we are not in doubt about whether the table is initially on
> top of itself!

You seem to be saying that

on(table,table,0)

is false, even though as you explain later the first argument of ON should
be a block and table does not belong to this sort.  From my standpoint
on(table,table,0) is not false but meaningless. If you try to write such a
sentence a good system should simply give you a syntax error.

> The predicate on/3 is treated as symmetric
>
>   * relative to the view that its first argument is of sort "block" *
>
> which does not include "table", not of the sort "location" which does.
>
> A sort predicate can be viewed either as asymmetric, or as trivially
> symmetric: relative to itself.  Either way, there is no need to use  the
> strong negation of a sort predicate in the program.
>

Not only there is no need to do that. Using negation is impossible --  
it is simply not defined for sorts.

> 2. You propose a semantics of choice according to which the program
>
> p(a).
> q(b).
> {r(X) : p(X)}.
> {r(X) : q(X)}.
>
> has one answer set:
>
> {p(a),q(b),-r(a),-r(b)}.
>
> It seems that the counterpart of your approach can be represented in  
> the
> language of smodels/clingo as follows:
>
> p(a).
> q(b).
>
> {r(X) : p(X)}.
> :- r(X), not p(X).       % prohibit non-subsets of p
> -r(X) :- p(X), not r(X). % CWA
>
> {r(X) : q(X)}.
> :- r(X), not q(X).       % prohibit non-subsets of q
> -r(X) :- q(X), not r(X). % CWA
>

Most likely you are right. I attempted to prove something like this
long time ago but was not satisfied with the proof because I could
not fully understand the original lprase definition. Probably it is
possible to prove now using embedding of choice rules into more powerful
logics designed by you and others.

This probably can be also mapped into DLV.

> 3.  You write that the anti-chain property of answer sets reflects the
> rationality principle, "believe nothing you are not forced to believe."
> It appears then that your general approach to logic programs--seing rules
> as constraints on a set of beliefs of a rational agent--is in conflict
> with using any programming constructs violating the anti-chain  
> property.  Would you agree with this?

Absolutely.

> If so, we face a dilemma: either reject
> smodels-style choice rules, or reject your philosophy of logic  
> programming.  That would be a pity, because I like both!

Of course some of us have the dilemma.  For me it is not much of the
dilemma though because I believe that the definition I gave above serves
the goal for which choice rules were invented. I consider this definition
to be a small change preserving the original intent.

That is why I was asking you what is it you like so much about the original
rules.  I hope the discussion at least clarified the dilemma so thanks very  
much for the responses.

=========

Date: 24 Oct 2010
From: Vladimir Lifschitz
To: Michael Gelfond

We can clarify the situation by distinguishing between the languages of
lparse, gringo, and dlv on the one hand, and the language of what you call
"a good system".  The languages of the existing solvers don't assign sorts
to argument positions, and when we use such a language we simulate sorts by
unary predicates.  These predicates play a special role in the mind of the
program designer, but there is nothing special about them from the point of
view of the syntax of the language.

This is similar to the distinction between one-sorted and multi-sorted
languages of first-order logic.  To say that every point belongs to some
line in a one-sorted language, we would write something like this:

  forall x(point(x) -> exists y(line(y) & in(x,y))).       (1)

In such a language, we can also write

  forall x(point(x) -> exists y(point(y) & in(x,y)));      (2)

this is silly but syntactically correct.

In a multi-sorted ("good") language, we would use a variable p of sort
point, a variable l of sort line, and we would write simply

  forall p exists l in(p,l)

instead of (1).  There would be no way to translate (2) into a language
like this: it has variables for points and variables for lines, but no
variables for "things in general."

When I wrote in the previous message that on(table,table,0) doesn't belong
to an answer set, I was talking about the languages of the existing solvers.
Wheh you replied that this expression is meaningless, you were thinking of
the language of a good system of the future.

=========

Date: 27 Oct 2010
From: Pedro Cabalar
To: TAG

I've been following the discussion on choice rules. This is how I  
understand it, I don't know if it may help or may create confusion.

I agree with Michael in that choice rules are quite difficult to  
explain to students, especially if you have just introduced the  
traditional idea of reduct, which is very intuitive and simple. On the  
other hand, I agree with Vladimir in their treatment and that, in the  
general case, the anti-chain property can be sometimes removed.

It seems that part of the confusion is due to notation itself. Michael  
sees a construct {r(X) : p(X)} as the assertion "predicate r is a  
subset of p'' which, on the other way, may probably be the first sight  
intuition for such a writing if we thought about a reader unaware of  
lparse choice rules. Encoding Michael's interpretation of this  
"subset" construct in First Order Equilibrium Model (or equivalently  
the General Theory of Stable Models) is an interesting topic for  
future study.

The purpose of choice rules, however, is not that of Michael's  
"subset". I guess that a more intuitive notation would have probably  
been

  [ r(X) : p(X) ]

meaning that it is *optional* to take or pick any instance X of p as  
an instance of r. This doesn't mean that r cannot hold for other  
elements due to other rules. The formula above can be seen as an  
abbreviation of the rule

r(X) ; not r(X) :- p(X).

where as we can see, we allow default negation in the head. As we all  
know, rules with default negation in the head do not satisfy the anti- 
chain property. For instance, the program

p ; not p

(or the choice [p] for short) has two stable models: {p} and the empty  
set. On the other hand, negation in the head is really simple to  
explain to students using a straightforward extension of the  
traditional definition of reduct.

Other arguments in favor of considering negation in the head are

a) We have now a semantics for defining stable models for arbitrary  
propositional theories. We know that an arbitrary theory is always  
strongly equivalent to some logic program with the same vocabulary,  
and allowing disjunction and default negation in the head. To obtain  
such a result for disjunctive rules without negation in the head (and  
so, guaranteeing the anti-chain property) we must allow introducing  
auxiliary atoms.

b) Related to a), even using DLV we can "violate" the anti-chain  
behavior if we consider some predicates as auxiliary, for instance, by  
hiding them. Let me adapt an example submitted by Vladimir to TAG some  
time ago. Take again the choice [r(X) : p(X)] or its rule encoding:

    r(X) ; not r(X) :- p(X).

This is strongly equivalent to

    r(X) :- p(X), not not r(X).

Of course, DLV does not have double negation, but we can "encode"  the  
subformula "not r(X)" using a fresh auxiliary predicate "aux(X)" as  
follows:

(1)   r(X) :- p(X), not aux(X).

and defining aux(X) with the unique rule:

(2)   aux(X) :- p(X), not r(X).

Now, look at the two rules (1) and (2) together: they form a typical  
even negative loop to generate a choice in ASP!

I suspect that, in some cases, we use strong negation -r(X) to play  
the role of aux(X) above (aux cannot appear in the rest of the  
program). I also believe that this motivated Vladimir's comment on the  
sometimes limited use of -r(X) for just creating choices.

Now, taking (1),(2) in DLV, if we hide the extent of the auxiliary  
predicate aux(.) we will essentially get the same result as in lparse,  
possibly obtaining "non-minimal" stable models.

---------

(See Part 2 for the continuation of this discussion.)