Variables in Answer Set Programming

Date: Fri, 31 Dec 2004
From: Vladimir Lifschitz
To: TAG

I'm thinking these days about the use of variables in ASP programs.  Here
is a simple program with variables in the input language of lparse:

  a(1).
  {b(X):a(X)}.

The second rule means, intuitively, that b is an arbitrary subset of a, and
smodels tells us that this program has two answer sets:

  Answer: 1
  Stable Model: a(1) 
  Answer: 2
  Stable Model: b(1) a(1) 

Consider now the following program P:

  a(1).
  a(2) :- b(1).
  {b(X):a(X)}.

lparse doesn't accept P as correct input, and this is related to the fact,
I think, that P is not omega-restricted (Tommi Syrjanen, "Omega-restricted
Logic Programs", in Proc. LPNMR-01).  I'm wondering whether refusing to
define the concept of an answer set for programs like P is a reasonable
semantic choice.

I expect that P will have 3 answer sets

  a(1)
  a(1), a(2), b(1)
  a(1), a(2), b(1), b(2)

once we give an appropriate definition of an answer set for programs with
variables.  I don't know what this definition will look like, but here are
some observations and questions that may help us invent it.

1.  If we rewrite the last rule of P as

  {X:b(X)} subset {X:a(X)}

we'll get, I think, a program in the language ASET ("A-Prolog with sets")
defined and implemented by Michael Gelfond and his students.  Is it
meaningful and executable in ASET?

2.  If we rewrite the last rule of P as

  b(X); not b(X) :- a(X)

the result P' will be a program with nested expressions, except that
we need to decide how to ground it.  I suspect that if we choose *any*
set of symbols that includes 1 and 2, and ground P' by substituting
these symbols for X, the answer sets for the resulting ground program
will be always the sets shown above.  In this sense, P' is "domain
independent."

3. P' can be also viewed as a formula of first-order equilibrium logic
that David Pearce is working on.  What is the status of P' in that logic?

Please share with me your thoughts about P and about the semantics of
variables in answer set programming in general.

======

Date: Fri, 31 Dec 2004
From: Michael Gelfond
To: Vladimir Lifschitz

Program
a(1).
a(2) :- b(1).
{X:b(X)} subset {X:a(X)}

of ASET has three answer sets:

a(1).
b(1),a(1),a(2).
b(1),b(2),a(1), a(2).

Intuitively, 'b' is an arbitrary subset of 'a' which is defined
by rules 1 and 2 of the program. (in a sense the definition
is mutually recursive)

The answer sets are reasonably in tune with the intuitive
meaning of rules.
I do not have ASET on my computer so cannot check now
but it should be executable.

I do not really know if the program is meaningful.
I do not remember such recursive definitions in mathematics.
Does anyone? In my programs I usually define 'a' and after that
say "let 'b' be a subset of 'a'. ''
(i.e. in ASET the problem is not really that closely realated to "treatment
of variables" .  Rather it is about which definitions of sets are useful.)

======

Date: Sat, 1 Jan 2005
From: Vladimir Lifschitz
To: Michael Gelfond

One more observation: we can rewrite the last rule of P

  {b(X):a(X)}

as the disjunctive rule

  b(X) v c(X) :- a(X)

(intuitively, c is the complement of b) and execute the program under dlv.
Then we'll get three answer sets similar to those shown in your message:

  {a(1), b(1), a(2), c(2)}

  {a(1), b(1), a(2), b(2)}

  {a(1), c(1)}

> I do not really know if the program is meaningful.
> I do not remember such recursive definitions in mathematics.
> Does anyone? In my programs I usually define 'a' and after that
> say "let 'b' be a subset of 'a'. ''
> (i.e. in ASET the problem is not really that closely realated to "treatment
> of variables" .  Rather it is about which definitions of sets are useful.)

It seems to me that even if programs like P are not useful, it may be a good
idea to aim at a semantics of programs with variables that is applicable to
P and to other programs that are not omega-restricted.  An attempt to define
a more general semantics may lead to a *simpler* semantics.  There was a time,
for instance, when the best available semantics of negation as failure was
the iterated fixpoint semantics for stratified programs.  Stratifications
are messy.  Even if all useful programs were stratified, aiming at a
semantics that doesn't rely on stratifications would have been a good idea:
the definitions of the well-founded model and of stable models are simpler,
besides being more general.

======

Date: Sun, 2 Jan 2005
From: Michael Gelfond
To: Vladimir Lifschitz

Interesting.
This transformation seems to be rather general.
Is it equivalent (modulo new predicate symbols)
to {b(X) : a(X)} where 'a' is 'legal' from thev stanpoint of lparse?

> It seems to me that even if programs like P are not useful, it may be a good
> idea to aim at a semantics of programs with variables that is applicable to
> P and to other programs that are not omega-restricted.  An attempt to define
> a more general semantics may lead to a *simpler* semantics.  There was a time,
> for instance, when the best available semantics of negation as failure was
> the iterated fixpoint semantics for stratified programs.  Stratifications
> are messy.  Even if all useful programs were stratified, aiming at a
> semantics that doesn't rely on stratifications would have been a good idea:
> the definitions of the well-founded model and of stable models are simpler,
> besides being more general.

I agree. It may lead to a simpler semantics.
However the first thing we did after reading the stratification
paper was to look for meaningful examples of non-stratified programs.
It was useful too.

One more comment:

You say that 'intuitively, the rule {b(X):a(X)} says that 'b' is an arbitrary
subset of 'a'.

It seems to me that according to this reading the program P

a1(1).
a2(2).
{b(X) : a1(X)}
{b(X) : a2(X)}

should have one answer set {a1(1),a2(2)}.
Smodels however will produce four of them.

This was one of the reasons I introduced ASET.

======

Date: Sun, 2 Jan 2005
From: Paolo Ferraris
To: TAG

My way of understanding a rule of the form

{b(X):a(X)} :- body         (1)

is as the following rule

{b(X)} :- a(X), body.       (2)

(This is Vladimir's second proposal, except that here I am not 
considering (2) as a rule with nested expressions.)
Some nice properties of this characterization are that (2), at least 
when body is empty, is "domain independent" as Vladimir said, and it 
seems to me that, when (1) and (2) can be grounded by lparse, two 
strongly equivalent sets of rules are generated.

However, this characterization doesn't seem to make things easier for 
lparse: by taking Vladimir's example, lparse cannot ground

 a(1).
 a(2) :- b(1).        (3)
 {b(X)} :- a(X).

It doesn't even ground the following program equivalent to (3) that does 
not contain choice rules:

 a(1).
 a(2) :- b(1).
 b(X) :- a(X), {not b(X)} 0.

======

Date: Mon, 3 Jan 2005
From: Vladimir Lifschitz
To: Paolo Ferraris

> My way of understanding a rule of the form
> 
> {b(X):a(X)} :- body         (1)
> 
> is as the following rule
> 
> {b(X)} :- a(X), body.       (2)

You are right, in this case X can be equivalently treated as a "global"
variable.  But there are cases, I think, when it's not clear how to get
rid of local variables:

  a(1).
  a(2) :- b(1).
  1 {b(X):a(X)}.

(The last rule means, intuitively, that b is an arbitrary nonempty subset
of a.)  Do we know how to define the concept of an answer set for programs
like this? I would expect two answer sets in this example:

  a(1), a(2), b(1)
  a(1), a(2), b(1), b(2)

======

Date: Mon, 3 Jan 2005
From: Monica Nogueira
To: TAG

As you may recall, the Lparse manual (pp.29) states that a previous
parser, "parse", would accept and ground programs containing (positive)
non-domain predicates in the body of the rules. More specifically, I think,
it accepted what today is called weakly restricted variables.
That was discontinued with lparse because of implementation/performance
issues.

When writing program P, I would add a "dumb" domain predicate to 'guide'
the grounding process, as follows:

grd(1..2).
a(1).
a(2) :- b(X).
{b(X)} :- a(X), grd(X).

hide grd(X).


As expected, this program is accepted and grounded by lparse, and
has the following answer sets:

1.  a(1)
2.  b(1) a(1) a(2)
3.  b(1) a(1) b(2) a(2)

It's clear that this is no solution to general cases or large programs.
But it can be useful if one wants to check the models computed by
such a program.

Michael wrote:

> It seems to me that according to this reading the program
> 
> a1(1).
> a2(2).
> {b(X) : a1(X)}.
> {b(X) : a2(X)}.
> 
> should have one answer set {a1(1),a2(2)}.
> Smodels however will produce four of them.

I'm not sure why a unique answer set in this case.
Would you mind to elaborate?

======

Date: Mon, 3 Jan 2005
From: Michael Gelfond
To: Monica Nogueira

Rule 3 says that 'b' is a subset of a1.
Rule 4 says that it is a subset of a2.

The only set which satisfies both conditions is the empty set.
So 'b' is empty.

======

Date: Mon, 3 Jan 2005
From: Vladimir Lifschitz
To: Michael Gelfond and Monica Nogueira

Here is how I understand this.  Reading the rule

  {b(X) : a1(X)}.

as "b is an arbitrary subset of a1" implicitly assumes that the program
has no other rules with b in the head.  So in the presence of the rule

  {b(X) : a2(X)}.

this reading is not acceptable.  This is similar to how definitions work
in logic programming.  Reading the pair of rules

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

as "q is the transitive closure of p" implicitly assumes that the program
has no other rules with q in the head.

======

Date: Mon, 3 Jan 2005
From: Paolo Ferraris
To: Vladimir Lifschitz

>You are right, in this case X can be equivalently treated as a "global"
>variable.  But there are cases, I think, when it's not clear how to get
>rid of local variables:
>
>  a(1).
>  a(2) :- b(1).
>  1 {b(X):a(X)}.
>
>(The last rule means, intuitively, that b is an arbitrary nonempty subset
> of a.)  Do we know how to define the concept of an answer set for programs
> like this? I would expect two answer sets in this example:
>
>  a(1), a(2), b(1)
>  a(1), a(2), b(1), b(2)

I agree. I think that it may be convenient to consider rule

1 {b(X):a(X)}.

as a shorthand for

{b(X):a(X)}.
:- {b(X):a(X)} 0.

and similarly for any choice rule with nontrivial bounds in the head.
In this way, local variables in the language of lparse can be explained 
if we understand the meaning of

- variable X in rules of the form

     {b(X):a(X)} :- body.

and

- local variables in cardinality constraints that are in the body of rules.

Local variables of this second kind are still unclear to me.

======

Date: Mon, 3 Jan 2005
From: Vladimir Lifschitz
To: Monica Nogueira

> It's clear that this is no solution to general cases or large programs.

I'd like to understand limitations of your trick with "dumb domain
predicates."  What would be an example of an lparse program that
intuitively seems meaningful but does not seem to be translatable,
using tricks like this, into a program that lparse can ground?  Take,
for instance, my last example

  a(1).
  a(2) :- b(1).
  1 {b(X):a(X)}.

Or we can rewrite this program in the form suggested by Paolo:

  a(1).
  a(2) :- b(1).
  {b(X)} :- a(X).
  :- {b(X):a(X)} 0.

Can we "massage" it into a form accepted by lparse using auxiliary
predicates?

======

Date: Mon, 3 Jan 2005
From: Vladimir Lifschitz
To: Michael Gelfond
e
> Interesting.
> This transformation seems to be rather general.
> Is it equivalent (modulo new predicate symbols)
> to {b(X) : a(X)} where 'a' is 'legal' from thev stanpoint of lparse?

I suspect that the answer is yes.

  CONJECTURE.  Take any program with nested expressions containing a rule of
  the form
  
    p ; not p <- Body                                                 (*)
  
  where p is an atom.  Replace (*) with
  
    p ; q <- Body
  
  where q is a new atom.  Then the answer sets for the new program are
  identical to the answer sets for the old program with q added to those
  that don't contain p.

To see how this conjecture is related to your question, note that (*) is
a possible way to understand

    {p} <- Body

according to the paper by Ferraris and Lifschitz "Weight constraints as
nested expressions," TPLP Vol. 5(1&2) (CoRR: cs.AI/0312045).

======

Date: Sat, 15 Jan 2005
From: Gerald Pfeifer
To: TAG

Wouldn't it be better if someone invested time to remove those limitations 
Lparse currently has instead of continuously pondering on how to work 
around them?

I believe it has been sufficiently proven that one can implement an 
efficient (both in terms of run-time and size of the generated grounding) 
instantiator for ASP programs without requiring domain predicates.


People really seem to like choice rules, so I wonder whether one rainy 
weekend I should add (some form of) these to DLV?

Then you could write the second variant of the first program as

  a(1).
  a(2) :- b(1).

  {b(X)} :- a(X).
  :- #count{X : b(X)} < 1.

instead of the following which uses standard ASP plus DLV's aggregates:

  a(1).
  a(2) :- b(1).

  b(X) v nb(X) :- a(X).
  :- #count{X : b(X)} < 1.

If someone is interested, sending me a specification of such a new 
extension (and translations into standard ASP+DLV's aggregates) might 
speed this up. ;-)

======

Date: Sun, 16 Jan 2005
From: Veena Mellarkod
To: Vladimir Lifschitz

The program:
---------------------------
a(1).
a(2) :- b(1).
{X:b(X)} subset {X:a(X)}.

compute 0, {}.

show a.
show b.
---------------------------

is executable in ASET and the answer sets
returned by ASET are:

 Answer Set #1 : a(1)

 Answer Set #2 : a(1) a(2) b(1)

 Answer Set #3 : a(1) a(2) b(1) b(2)
---------------------------

======

Date: Thu, 20 Jan 2005
From: Vladimir Lifschitz
To: Veena Mellarkod

Thank you for checking this.  I'd like to understand how the computational
process is organized.  Marcello called ASET a "front-end" in one of his
messages.  It's a front-end for what program?  Does its output serve as
input for the usual lparse?  Or is its output a grounded program that can
be directly fed into smodels?

======

Date: Thu, 20 Jan 2005
From: Vladimir Lifschitz
To: Gerald Pfeifer

> Wouldn't it be better if someone invested time to remove those limitations 
> Lparse currently has instead of continuously pondering on how to work 
> around them?

Maybe you are right.  But my main point is that this is not merely the
question of extending lparse.  It seems to me that we didn't yet see a
definition of "correct grounding" for a class of programs in the
language of lparse that includes my examples.  We don't know how to define
the concept of a "good" ("groundable") program in the language of lparse
that would be wider than "omega-restricted."  In other words, we'll need
to do some theoretical work first, to define a specification for such an
extended lparse.

Or maybe I am wrong, and we can try to understand the meaning of
non-omega-restricted rules in the language of lparse by rewriting
them in the language of dlv.  Take an lparse rule with "conditional
literals" in the body, such as

:- {p(X,Y) : a(X)} 0, b(Y).

It means: for every Y from b, the set of all X's from a such that p(X,Y)
belongs to the answer set is not allowed to be empty.  How would you
express this in the language of dlv?

> People really seem to like choice rules, so I wonder whether one rainy 
> weekend I should add (some form of) these to DLV?
>
>
> Then you could write the second variant of the first program as
> 
>   a(1).
>   a(2) :- b(1).
> 
>   {b(X)} :- a(X).
>   :- #count{X : b(X)} < 1.
> 
> instead of the following which uses standard ASP plus DLV's aggregates:
> 
>   a(1).
>   a(2) :- b(1).
> 
>   b(X) v nb(X) :- a(X).
>   :- #count{X : b(X)} < 1.

It seems to me that the need to use auxiliary predicates, such as nb,
which are typically not needed anywhere else in the program, is a blemish on
the input language of dlv that would be easy to remove.  Please do this 
one rainy weekend!

> If someone is interested, sending me a specification of such a new 
> extension (and translations into standard ASP+DLV's aggregates) might 
> speed this up. ;-)

For grounded programs something like this is done in the paper

     Paolo Ferraris, Answer sets for propositional theories,
     http://www.cs.utexas.edu/users/otto/papers/proptheories.ps .

It shows how the choice construct and all the main elements of the
language of dlv except for variables (that is, disjunctive heads and
aggregates) can be treated as syntactic sugar, once we extended the
definition of an answer set to propositional formulas.

======

Date: Thu, 20 Jan 2005
From: Veena Mellarkod
To: Vladimir Lifschitz

There are 2 parts to ASET computational process (similar to lparse-smodels).

1. Grounder
2. Inference Engine

Given an ASet-Prolog program P:

The grounder uses a prolog program (set_parse) to rewrite set-literals and
function-literals in P in a way that lparse could ground P. After
grounding, the set-literals and function-literals are added back to
ground(P).

The inference engine is similar to smodels but computes answer sets for
ground ASet-Prolog programs.

======

Date: Thu, 20 Jan 2005
From: Vladimir Lifschitz
To: Veena Mellarkod

Okay, so ASET works like this:

      your      standard     adding set-literals      your inference engine
-> set_parse ->  lparse  -> and function-literals  ->  (similar to smodels) ->

Is this right?

If so, here is my question: if the input of set_parse is our program

 a(1).
 a(2) :- b(1).
 {X:b(X)} subset {X:a(X)}.

 compute 0, {}.

 show a.
 show b.

then what is its output, what is the program that set_parse asks lparse
to ground?

The reason I am interested in this is that your set_parse is apparently
capable of translating our program into the language of lparse without
making it "non-omega-restricted" -- that's the kind that lparse refuses to
ground.  And I'm curious how this is done.

======

Date: Wed, 26 Jan 2005
From: Veena Mellarkod
To: Vladimir Lifschitz

        set_parse has 3 main procedures: transform1, ground and transform2.
transform1 replaces all sets with newly generated A-Prolog predicates
containing the free variables as arguments. It also records the changes.
For our program:

 a(1).
 a(2) :- b(1).
 {X:b(X)} subset {X:a(X)}.

 compute 0, {}.

 show a.
 show b.

The output of transform1 is:
a(1).
a(2):-b(1).
my_new_atom1.
b(1):-not my_temp_atom,b(1).
my_temp_atom:-not b(1),b(1).

The rule "my_new_atom1." represents the 3rd rule in our program. The last
two rules of the output are introduced so that lparse does not remove b(1)
as false.

This output is the input to ground procedure. The ground calls lparse and
the result of the lparse is the output of ground. The transform2 procedure
uses the recorded changes by transform1 and re-inserts the sets with
proper grounding of the free variables. This output is the input to
inference engine.

======

Date: Mon, 31 Jan 2005
From: Vladimir Lifschitz
To: Veena Mellarkod

Thank you for explaining how ASET uses LPARSE.

It looks like ASET "tricks" LPARSE into doing what it needs.  Here is what
I mean.  Among other things that it does, LPARSE simplifies its input in
various ways.  For instance, if an atom doesn't occur in the heads of the
rules of the input program then LPARSE drops this atom from the bodies of
all rules; it knows that this transformation doesn't change the meaning of
the program.  But LPARSE is not clever enough to notice that dropping
trivial rules such as

   b(1):-not my_temp_atom,b(1).

doesn't change the meaning of the program either.  This is why the last two
rules in the output of transform1 have the desired effect.

======

Date: Sun, 6 Feb 2005
From: Gerald Pfeifer
To: Vladimir Lifschitz

> Among other things that it does, LPARSE simplifies its input in
> various ways.  For instance, if an atom doesn't occur in the heads of the
> rules of the input program then LPARSE drops this atom from the bodies of
> all rules; it knows that this transformation doesn't change the meaning of
> the program.

as far as I can see this transformation is only safe when this atom occurs 
negated (as a negative body literal).  When you make this transformation 
and remove a positive body literal, you may well change the semantics of 
the program.

Consider the program following, which has the empty answer set:

  a :- b.

If you remove b, which does not occur in the head of any rule, from the
body of this rule, we will get {a} as an answer set.

======

Date: Sun, 13 Feb 2005
From: Vladimir Lifschitz
To: Gerald Pfeifer

You are right, thanks for the correction.  I should have said: replaces the
atom by "false."  That amounts to removing the atom when it occurs in the
body negated, and removing the whole role when the it occurs in the body
without negation.