Defaults Involving Functions

Date: 17 Apr 2012
From: Vladimir Lifschitz
To: TAG

I am reading now the KR'12 paper by Mike Bartholomew and Joohyung Lee
(http://peace.eas.asu.edu/joolee/papers/fsm-kr.pdf), and I found there
an interesting observation that the authors have unfortunately hidden
in the middle of a highly technical discussion, where it can be easily
overlooked.

How does ASP solve the frame problem, say, in the blocks world?  The
traditional way of doing that is to write

  % inertia
  on(B,L,T+1) :- on(B,L,T), not -on(B,L,T+1), T<lasttime.

and to include also the rule

  % uniqueness of location
  -on(B,L1,T) :- on(B,L,T), L!=L1.

(These are pretty much quotes from my 2002 paper posted at
http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=924).  In the
absence of additional information about the location of block B at
time T+1, the inertia rule above will allow us to derive on(B,L,T+1)
for the location L that satisfies on(B,L,T).  But if we are given
conflicting information about the location of B at time T+1 then this
inference will be disabled by the uniqueness of location rule.

What Mike and Joohyung noticed is that there is another way of
achieving the same result.  They express the uniqueness of location by
the constraint (rule with the empty head)

  :- 2 {on(B,LL,T): location(LL)}.

They include also an "existence of location" constraint:

  :- {on(B,LL,T): location(LL)} 0.

Then inertia is expressed by the choice rule

  {on(B,L,T+1)} :- on(B,L,T), T<lasttime.

("If on(B,L,T) then decide arbitrarily whether to assert on(B,L,T+1).")
In the absence of additional information about the location of B at
time T+1, asserting on(B,L,T+1) will be our only option, in view of the
existence of location constraint.  But if we are given conflicting
information about the location of B at time T+1 then not asserting
on(B,L,T+1) will be our only option, in view of the uniqueness of
location constraint.

This alternative formulation is more economical, because it eliminates
the need for strong negation.  I wish I knew it in 2002.

It is based on a general method of expressing default assumptions about
values of functions (and that is what the paper by Mike and Joohyung is
to a large degree about).  Here is another example of the use of that
method.  We want to say that, by default, blocks are presumed to be on
the table at time 0.  The traditional formalization, in the presence of
the uniqueness rule with strong negation in the head, may look like this:

  on(B,table,0) :- not -on(B,table,0).

And here is the new solution, in the presence of the existence and
uniqueness constraints:

  {on(B,table,0)}.

============

Date: 17 Apr 2012
From: Yuliya Lierler
To: TAG

Interestingly, the reading of

 	on(B,table,0) :- not -on(B,table,0)

as

   by default, blocks are presumed to be on the table at time 0

does not seem to be as natural for the rule

 	{on(B,table,0)}.

Rather, it says that
 	blocks maybe on the table at time 0, or
 	it is OK for blocks to be on the table at time 0.

============

Date: 17 Apr 2012
From: Vladimir Lifschitz
To: Yuliya Lierler

Here is how I understand the relationship.  A block may be on the table or
not on the table.  But it can't be nowhere at all.  Consequently, in the
absence of information about a different location, it has to be on the
table.

===========

Date: 17 Apr 2012
From: Yuliya Lierler
To: Vladimir Lifschitz

Yes, and for understanding the rule

 	{on(B,table,0)}.

in this way it is important to view it in a bundle with
"the uniqueness of location" and the "existence of location" constraints.

The rule

 	on(B,table,0) :- not -on(B,table,0)

by itself seems to disclose more information.


============

Date: 17 Apr 2012
From: Paolo Ferraris
To: Yuliya Lierler

I agree. It seems to me that the difference is made by the "existence of 
location" constraint, that is explicit in Mike and Joohyung's formulation,
but it is inferred in the traditional formulation only if existence holds
at the previous  time stamp as well. Notice, for instance, that

  % inertia
   on(B,L,1) :- on(B,L,0), not -on(B,L,1).
  % uniqueness of location
   -on(B,L1,1) :- on(B,L,1), L!=L1.


(no rules with on(B,L,0) in the head) has the empty set as an answer 
set. This is clearly not possible with an explicit existence constraint.

Under both existence constraint by Mike and Joohyung and uniqueness in 
the traditional formulation,

   not -on(B,L,1)

seems to be strongly equivalent to nested expression

   not not on(B,L,1),

so that inertial rule

   on(B,L,1) :- on(B,L,0), not -on(B,L,1).

can be written as

   on(B,L,1) :- on(B,L,0), not not on(B,L,1).

and then as

   {on(B,L,1)} :- on(B,L,0).

as Mike and Joohyung propose.

==============

Date: 18 Apr 2012
From: Michael Gelfond
To: TAG

I agree with Yuliya too.

Paolo correctly states that the new solution only works if each block
is assumed to be supported by table or other block.  I normally do not
make this a necessary part of the blocks world story.

Vladimir says:

> This alternative formulation is more economical, because it eliminates
> the need for strong negation.

I am not sure why it is more economical.
The first (old) solution "eliminates" need for choice rules and  
cardinality constraints.

==============

Date: 19 Apr 2012
From: Joohyung Lee
To: TAG

To me a more economical way is to write as

  {loc(B,T+1)=L} :- loc(B,T)=L, T<lasttime     (1)

under the language proposed in the KR'12 paper. As Vladimir pointed,
that was the main subject of the paper, i.e., how to extend the
stable model semantics with "intensional functions."

The rules Vladimir quoted,

 {on(B,L,T+1)} :- on(B,L,T), T<lasttime.

 :- 2 {on(B,LL,T): location(LL)}.
 :- {on(B,LL,T): location(LL)} 0.

were obtained as a byproduct of eliminating intensional function "loc"
in favor of intensional predicate "on" in order to use answer set
solvers.  (I hope someday an answer set solver (or its preprocessor)
can directly accept a rule like (1) ).

I have used this encoding method in my class on answer set programming
where I didn't introduce strong negation, and students seem
to catch up the idea quickly.

---

> Paolo correctly states that the new solution only works if
> each block is assumed to be supported by table or other block.
> I normally do not make this a necessary part of the blocks world
> story.

I normally make this assumption when dealing with multi-valued
fluents in answer set planning. In each state, every block has a
location (other block or the table). I wonder when we need to avoid
this assumption. Could you please tell me?

---

Note that the blocks world was chosen intentionally in that paper to
avoid the use of strong negation. There is one place where strong
negation is a bit more economical even with the new encoding, when we
express Boolean fluents. Consider

   {up(true,T+1)} :- up(true,T), T<lasttime.
   {up(false,T+1)} :- up(false,T), T<lasttime.

plus the unique and existence constraints for Boolean values. It
becomes a bit simpler to write it as

   {up(T+1)} :- up(T), T<lasttime.
   {-up(T+1)} :- -up(T), T<lasttime.

and add the existence constraint

   :- {up(T), -up(T)} 0.

but no need for the uniqueness constraint as it is built-in in the
semantics of strong negation.

==============

Date: 19 Apr 2012
From: Marcello Balduccini
To: Joohyung Lee

> (I hope someday an answer set solver (or its preprocessor)
> can directly accept a rule like (1) ).

I don't know if it's what you are looking for, but in the past several
months I have been working on a solver that among other things accepts
directly the syntax of (1) -- modulo small syntactic variations.  The
solver is called clingof, is based on clingo and is available from
http://marcy.cjb.net/clingof/. The last example on the web page shows
the use of choice rules similar to (1).

In the language of clingof, (1) would be written:

{ loc(B,T2) #= L } :- loc(B,T1)#=L, time(T1), block(B), loc(L),
                      T1<lasttime, T2=T1+1.

The domain predicates are required because of the older version of clingo
that my solver is built upon. This will change in the not-too-distant future.

I haven't had a chance to read your KR'12 paper, but the two rules seem to
have the same meaning.

A simple program, ex1, which uses the re-writing of (1) is:

#nherb loc/2.
#const lasttime=1.

time(0..lasttime).
loc(l1;l2).
block(b1;b2).

loc(b1,0) #= l1.

{ loc(B,T2) #= L } :- loc(B,T1)#=L, time(T1), block(B), loc(L),
                      T1<lasttime, T2=T1+1.

#hide.
#show #nherb loc/2.

The first statement declares loc/2 to be what in clingof's terminology is
a "non-Herbrand" function. The rest of the program should be quite
straightforward.  The answer sets found by running "clingof 0 ex1" are:

Answer: 1
loc(b1,0)#=l1 
Answer: 2
loc(b1,0)#=l1 loc(b1,1)#=l1

==============

Date: 20 Apr 2012
From: Pedro Cabalar
To: TAG

Sorry for the long mail, and for adding some noise to the discussion.
I also introduced an approach for evaluable (non Herbrand) functions back
in ICLP'08. There is even a previous approach for evaluable functions
(FASP) by Lin & Wang, but it didn't allow default values. 

In my language, this is how the default value of the example is declared:

loc(X,0):=table :- not loc(X,0) # table, block(X).

Operator '#' is read as 'has a value different from'. Thus, the rule above
simply says that the location of a block at time 0 is table if we cannot
prove that it has a value different from table. This operator # (called
'apartness') and its notation is not new: it comes from a work by Dana
Scott in the 70's where he introduced partial functions in intuitionistic
logic. We can also use # for inertia as follows:

loc(X,T2):=L :- loc(X,T1)=L, not loc(X,T2) # L, block(X), succ(T1,T2),
                location(L).

You can find a prototype frontend called lppf plus several additional
examples at

http://equilibriumlogic.irlab.org/?q=node/11

As far as I know, both Vladimir's intensional functions and Joohyung's new approach assume that functions are total. This is why a rule like:

(1)  loc(X,0)=table :- not not loc(X,0)=table, block(X)

or simply

{loc(X,0)=table} :- block(X).

works as a default value assignment. In my case, however, functions can
be partial if nothing prevents so, and thus, the rule above just says that
we are free to take an answer set where loc(X,0) has value table or leave
loc(X,0) undefined (no value). In this sense, I think, it is closer to the
'traditional' ASP encoding with predicates. The only implicit assumption we
are including is uniqueness of value.

Any function f(X) in my approach can be forced to be total by the addition
of an axiom such as

:- not \E f(X).

where \E represents Dana Scott's 'existence' operator, meaning that f(X) has
some value, i.e.,  is defined. In fact, \E f(X) is just an abbreviation of
the equality f(X)=f(X) which always holds, provided that f(X) has a value.

In our example, we can force the location of a block, say, at time 0, to
be total:

:- not \E loc(X,0), block(X).

If we combine (1) and (2) we get a quite similar behaviour to Joohyung's
and Vladimir's use of default values.

Regarding Vladimir's observation that opened this discussion, I'm not using
strong negation for default values either. However, I must recognize that I'm
just replacing it by a quite similar operator "#". In fact, you can easily
emulate strong negation using partial Boolean functions, so I didn't even
introduce strong negation in lppf.

By a personal discussion with Marcello, I understand that his approach also
allows partial functions but uses strong negation, although I don't know
more details yet. I'm happy to see that the topic is arising some interest.
It would be nice to discover the formal relations among all these approaches.

==============

Date: 2 May 2012
From: Gerald Pfeifer
To: TAG

> and add the existence constraint
> 
>    :- {up(T), -up(T)} 0.

Constraints like these always make my brain heart, since in a
way they carry more negation, intuitively.

Why not write

  up(T) v -up(T).

==============

Date: 7 May 2012
From: Vladimir Lifschitz
To: Gerald Pfeifer

It seems to me that your formulation is much too strong, it would make
the usual ASP solution to the frame problem invalid.  The program

  up(0).
  up(1) :- up(0), not -up(1).

has one answer set: {up(0), up(1)}.  But adding the rule

  up(1) v -up(1).

will add one more answer set, {up(0), -up(1)}, in conflict with the idea
of inertia.

I agree that the rule

   :- {up(T), -up(T)} 0.

(or, in the dlv syntax, :- not up(T), not -up(T).)  is "negative", but this
is exactly what we want.  It expresses the "negative" idea that incomplete
answer sets do not represent states and consequently should be dropped.