The French Toast Problem, Discussion
Dates: March 11-16, 2015
From: Vladimir Lifschitz
Most solutions that I have received are in the input language of
lparse/gringo. There are three exceptions: solutions 4 and 11 are for
IDP, and solution 10 is for clingcon. Speaking of the choice of the
input language in the proposed solutions, here is what I find puzzling:
- no use dlv, an excellent ASP system used in serious applications;
- no use of strong negation (even disguised in the form of auxiliary
predicates) -- a feature widely used in ASP formalizations of dynamic
domains;
- no use of action languages (implemented in CCalc, coala, and
cplus2asp). Are action languages a thing of the past?
Some solutions actually calculate the time needed to cook all 3 pieces
of french toast, given some upper bound; others only verify that the
problem can be solved within a given time.
Solutions differ from each other by their choice of fluents and actions.
(In Solution 5 there are no fluents at all; just the action of cooking
a piece P. There is no need to describe its effects. Amazing!) They
differ also by their approach to formalizing inertia. Some formulations
are more elaboration tolerant than others. Some are remarkably
concise. Some use clever optimization tricks; others don't -- the search
space here is small, after all.
===
I just added one more solution to the list posted at
http://www.cs.utexas.edu/tag/discussions.html. It's in the language of
SPARC, an ASP language with sorts that is based on dlv.
===
The newest arrival in the French Toast family is for dlv.
So my question why no one used dlv is now answered: this was an accident!
===
Two more descriptions of the French Toast domain have been added to the
list. Solution 15 is in the modular action description language ALM.
Solution 16 is in the input language of dlv.
=====================
Date: Mar 27, 2015
From: Michael Gelfond
It was interesting to read multiple solutions to Vladimir's problem.
I certainly did not expect this variety of programming styles.
Vladimir asked me to send an email to TAG explaining how SPARC is
different from other ASP languages, and, if possible comment on my
own solution.
So, here it is:
Unlike most other versions of ASP, SPARC is a typed language. It's programs
have sorted signatures and SPARC supports means for the description of
those signatures - object constants and their sort, and the sorts of
the parameters of the program's relations.
In the view of SPARC designers this allows a programmer to better structure the
program. It also help to automatically determine some syntax and semantic errors
and to avoid thinking about safety of ASP rules. The system can be downloaded from
https://github.com/iensen/sparc/wiki.
LPNMR paper on SPARC can be found in
http://www.depts.ttu.edu/cs/research/krlab/pdfs/papers/sparc-camera.pdf
There are two implemented versions.
One, implemented on top of DLV, supports ASP with consistency restoring rules.
One, built on top of Clingo, is limited to ASP.
I had positive experience with the language in class -- students were not
confused by safety rules, had better error messages, and saved a lot of time
normally spent on correcting errors caused by typos -- a wrong spelling
of a name, mix up in order of parameters of a relation, etc.
The discipline imposed by the necessity of typing was useful too.
In some cases it helped me to find better representations of knowledge for
my problems.
Now some comments on the program:
The main thing was to decide on the representation for toasts.
This lead to introduction of a sort #side. (Sort names in SPARC start with a #.)
Other sorts - steps, actions, and fluents - are common for action theories.
For instance,
#side = 1..m.
#action = toast(#side).
define two sorts. The first is simply a set of integers from 1 to m.
The second is a set of terms { toast(1),...,toast(m) }.
After the sorts are defined we have declarations of programs relations and their sorts,
which are followed by regular rules. (No safety requirement is needed).
In writing the rules I was first coming up with dynamic causal laws,
state constraints, definitions, and executability conditions of an action
language AL (also called AL_d) (one can find the language description in my book).
A rule
holds(toasted(S),I1) :-
occurs(toast(S),I),
I1 = I+1.
corresponds to causal law:
toast(S) causes toasted(S)
A rule
-occurs(toast(S2),I) :-
occurs(toast(S1),I),
same_toast(S1,S2).
is a translation of
impossible toast(S1), toast(S2), same_toast(S1,S2),
etc.
There is one interesting difference though:
Strictly speaking, executability condition
"impossible to toast more then two sides at the same time"
cannot be written in AL using aggregates.
So originally I had,
-occurs(A3,I) :- occurs(A_1,I),
occurs(A_2,I),
A1 != A2,
A1 != A3,
A2 != A3.
Of course, the representation with aggregates:
:- #step(I),
#count{A:occurs(A,I)} > 2.
is more pleasant.
COMMENT
In a new action language ALM it would be possible to use aggregates.
The executability condition in ALM will look as follows:
impossible |{ A : instance(A,toast), occurs(A) }| > 2.
However, aggregates are not included in the original version of ALM
since ALM's semantics is given in terms of Answer Set Prolog which
didn't have semantics of aggregates which we would find to be fully satisfactory.
I hope to expand ALM using aggregates defined without vicious circles as
in our recent work with Yuanling Zhang.
END COMMENT
Hopefully, this is enough to start a discussion.
Any questions, feedback and comments on this and other programs
will be appreciated.
=================
Dates: Mar 31, 2015
From: Vladimir Lifschitz
Even though SPARC assigns sorts to object constants and to the argument
positions of predicate symbols, it does NOT assign sorts to variables.
In this sense it differs from many-sorted languages familiar from logic.
When geometry is formalized in the language of first-order logic, we may
use variables for points, variables for lines, and variables for planes.
When we distinguish between sets and classes in set theory, we use
variables for sets and variables for classes. In a similar way, sorts
("types") are assigned to variables in most procedural programming
languages, so that we can talk about integer variables, floating point
variables, etc. Not in SPARC, which follows the tradition of Prolog and
other ASP languages: variables don't have sorts.
"Domain" statements, similar to variable declarations that specify
sorts of variables, are available in lparse and in early versions of
gringo. But the designers of gringo decided not to allow them in
Version 4.
So this is what many ASP researchers feel: the idea of assigning sorts
to variables, which is widely used in logic and in procedural
programming, is out of place in logic programming.
I am wondering why.
===============
Date: April 1
From: Bart Bogaerts
To: Vladimir Lifschitz
Interesting question.
In IDP, not only predicate positions have types, but also variables have
types. I believe this is often useful in order have a specification that is
natural as possible. Types restrict the range of a quantification. Natural
language specifications of problems solved by ASP systems (almost) never
contain quantifications about "everything", in these natural language
specifications range over a specific subset of the domain, which often
correspond to types.
Hence, if the natural language specifications rely on typed "variables",
why not use them in the formal specification as well?
As an example, I have annotated all informal language quantifications in
your description of the French toast problem with the (natural) type they
refer to.
You have three pieces of uncooked french toast *[a type toast]* and one hot
pan. Each one *[one refers to toasts, hence "each" is a quantification over
toasts] *needs to be cooked on both sides *[both quantifies over the sides]*.
Each side *[each quantifies over sides]* can be cooked by placing it on the
hot pan for one minute. The pan can only fit two *["only two" refers to "at
most two toasts"]* pieces of french toast at once, and only one *[only one
quantifies over sides]* side of each at a time *[each is a quantification
over time]*. How many minutes does it take to cook all three *[all three
quantifies over toasts]*, and how do you do it?
Also, when reading a formal specification, I often think of variables as
"typed". For example, consider (from the Sparc specification), the line
all_toasted(I) :-
#count{S : holds(toasted(S),I)} = m.
I would read this line: "For all times I *[time]*, allToasted(I) holds
if the number of sides *[side] *s such that s is toasted at time I
equals m".
I would not read it "for all I, alltoasted(I) holds if the number of S
such that S is toasted at I equals m."
In fact, to understand the Sparc line, it is important to know that S
refers to a side and I to time.
Summarized, from a modelling perspective, I think types are often very
natural, both for predicate positions and for variables. There are more
advantages associated to types, but Michael already mentioned those.
=============
Date: Apr 1, 2015
From: Pedro Cabalar
To: Vladimir Lifschitz
I'm not sure about what you mean by "assigning sorts to variables".
While in Prolog, variables are placeholders that can be instantiated by
anything at any moment, I don't think that in ASP we are using them in that
way. Much on the contrary, I think that we all bear in mind variable types
implicitly in most ASP programs.
Take, for instance:
orphan(X) :- not hasparents(X).
This rule is unsafe, and we would typically "undo" that problem by adding
a domain predicate
orphan(X) :- not hasparents(X), person(X).
Anyone would say that "person(X)" is a sort assignment for variable X. In other
words, we handle variable sorts implicitly.
In the case of SPARC, this is even more explicit, as far as I understand.
SPARC allows you specifying the argument sorts hasparents(#person) and
orphan(#person). Doing so, safety is not a problem and the original rule
would work because X can be assigned sort #person unambiguously. Moreover,
if we have a predicate haswheels(#vehicle) and we take a rule like:
orphan(X) :- not hasparents(X), haswheels(X).
I guess SPARC will yield an error if #vehicle and #person are unrelated sorts,
because X cannot be consistently assigned a sort. To sum up, I do think that
the idea of "assigning sorts to variables" is indeed being handled both in
ASP (implicitly) and in SPARC (explicitly).
On the other hand, I suspect that what you mean with "assigning sorts to
variables" is that LP people don't like "explicit global sort declarations
for variables". That is, clauses of the form
#domain person(X).
or, say, perhaps
X : #person.
then I agree. But I think that this is mostly because they create an
incoherent situation: while the sort of X with this clause affects to the
whole program (X is always of sort person), the scope of each X is limited
to the rule where it occurs (X is not always the same person for all rules).
I agree that this may be confusing (especially when you have grounding in mind)
although, as you say, it is not so strange in many-sorted logics after all.
===========
Date: Apr 1, 2015
From: Vladimir Lifschitz
To: Pedro Cabalar
You are right, by assigning sorts to variables I mean assigning them
explicitly and globally. And I like your explanation: in ASP, assigning
a sort to a variable globally is somewhat unnatural because the scope of
a variable is limited to a single rule.
I hope the designers of SPARC will comment on your example:
orphan(X) :- not hasparents(X), haswheels(X).
Is it true that SPARC will produce an error message given a rule like
this?
==============
Date: Apr 1, 2015
From: Evgenii Balai
SPARC will produce a warning for the rule like
orphan(X) :- not hasparents(X), haswheels(X).
and will continue the execution (answering queries or computing answer sets).
In the implementation, a proper flag, -wasp or -wcon needs to be set to see the warning.
While the rule has no ground instances, we do not consider the case as an error.
Errors of SPARC occur in more obvious violations,
e.g, when a non-numeric ground term is used as an argument whose sort is a set of natural numbers.
For more details about the difference between errors and warnings in SPARC, see section 2.1 of
our SPARC paper: http://www.depts.ttu.edu/cs/research/krlab/pdfs/papers/sparc-camera.pdf