RESTIVO@SU-SCORE.ARPA (05/07/85)
From: Chuck Restivo (The Moderator) <PROLOG-REQUEST@SU-SCORE.ARPA>
PROLOG Digest Tuesday, 7 May 1985 Volume 3 : Issue 22
Today's Topics:
Implementation - CP,
LP Library - Abstracts
----------------------------------------------------------------------
Date: Sun 5 May 85 19:31:35-EDT
From: Vijay <Vijay.Saraswat@CMU-CS-C.ARPA>
Subject: The !-annotation revisited. #1]
Some time ago in these channels I had defined a read-only
annotation '!' which was meant to replace Concurrent
Prolog's '?', which I felt had a messy and unjustifiable
semantics.
In the last issue, "THRIFT%ti-csl.csnet@csnet-relay.arpa"
mentions a '+' annotation, but I fail tosee how it is
different from '!'. To make matters clear, here is a
more thorough discussion of '!'. (Note that this is a
substantially revised version of my previous submission.)
In the following, "term" is used to refer to
either an atom or a functional term.
First, assume that unification of a compound term T1 against
a compound term T2 is carried out by checking if T1 and T2
have the same functor and arity and then unifying their
corresponding arguments in PARALLEL.
The '!' annotation can only decorate instances of terms in
the head of a clause. If a Term (variable OR constant OR
compound term) T! occurs in the head of a clause, then
unification T!-V, where V is a variable will suspend and
remain suspended until V has been instantiated (to a
constant or a possibly non-ground compound term), after
which the unification T-V will be attempted. Like the `?',
the `!' is not inherited by embedded terms, that is, it
applies only to the term instance textually indicated in the
program.
However, if '!' annotates a term t1 inside a term t, then it
must also annotate all sub-terms of t which contain t1
(including t). In fact, we will define an embedded
occurrence of a '!' to be shorthand for just such a series
of '!' annotations in the term. (The atom at the head of a
clause is always !-annotated.)
Note: 1. This restriction is necessary to prevent
occurrences of unify(X, f(a!)) which doesn't make sense
because you cannot require a sub-term to be present unless
you also require the superior term to be present.
2. wait/1 in CP seems to achieve the suspension part of '!'
but cannot be used to simulate it in CP-without-? without a
control primtive to sequence goals.
3. A simple lazy sequential O(N^2) algorithm can implement
!-unification correctly. (See next message in this Digest)
Note:
1. unify(Y!, X!) can never occur.
2. unify(Y, Y!) can, and suspends till Y is instantiated.
3. There is no 'inheritance' of '!' via X!-Y
unifications like there is for X?-Y.
4. The !-annotation can never 'occur' in any goal call at
run-time.
With '!' each CLAUSE decides what is to be INPUT to it.
With '?' each CALL decided what would be input to that call.
If all the clauses have the same pattern of input
specifications, then the '!' annotations could be removed in
favor of a mode-specification for the predicate. Since
nested '!' annotations are allowed within a term, in general
it is not possible to remove '!' annotations in favour of
mode declarations. (Of course, every program annotated with
the Dec-10 Prolog '+' (input) or '?' (dont-know) annotations
can be rewritten using '!' annotations; hence '!' is more
'general'.)
Examples: 1. merge/3. Equivalent mode: merge(+,+,?).
merge([A|X]!, Y, [A|Z]):- merge(X, Y, Z).
merge(X, [A|Y]!, [A|Z]):- merge(X, Y, Z).
2. plus/3. (No single equivalent mode declaration.)
plus(X!, Y!, Z):- Z is X+Y.
plus(X!, Y, Z!):- Y is Z-X.
plus(X, Y!, Z!):- X is Z-Y.
'!' is less powerful than '?' because it cannot be used to
simulate 'var' and hence write a b-merge like program, even
assuming strict-AND fairnes of the scheduler.
Hence I would propose using '!' in conjunction with var/1.
For var/1 I would propose some syntactic sugar: another
annotation (^, say). Again, the ^-annotation can occur only
in the clause-head, and annotates just the occurrence of the
Term it is textually adjacent to. The unification Term^-X
succeeds only if X is a variable and results in X being
unified with Term. If X is not a variable, then Term^-X
FAILS, though this must be regarded as a control failure.
Term^-X NEVER suspends.
Note that nested occurrences of ^ do not make sense.
Examples:
1. "foo(foo^)^" is meaningless.
2. "foo(foo^)" will match any of the following terms:
X, foo(X).
3. "foo(foo^)!" will match any of the following terms:
foo(X).
I feel I must also sound this note of warning. With the
assumption of weak AND-fairness (which, roughly paraphrased
says that every enabled goal will be reduced in a finite
amount of time), var/1 (or ^) is enough to write a program
which exhibits unbounded non-determinism. That is, the
program always terminates, but for every natural number 'k'
can produces as output y > k. Here it is:
p(X):- p(X,Stop), stop(Stop).
p(s(X), Stop^):- p(X,Stop).
p(X, stop).
stop(stop).
(Note: this is not a CP program: its a 'pure' (save for ^)
Horn logic program.) Without going into details suffice to
say that the semantics of constructs which allow unbounded
non-determinism can cause severe headaches because the limit
of arbitrary chains may not exist. My personal feeling is
that '^', or its equivalent, should be allowed in any
language which purports to be a CONCURRENT language; of
course as soon as we introduce '!' or '^' we are not talking
of LOGIC languages any more.
'!' cannot be (because it was not DESIGNED to be) used to
export 'protected' variables. But the whole thesis here is
that clauses should be forced to specify what their input is
and hence the 'embedded channel' problem in Hellerstein and
Shapiro, ISLP, 1984 can be taken care of by !-protecting at
the consume site instead of ?-protecting at the produce
site.
'!' seems to cover the vast majority of uncontroversial uses
of the `?' and is far simpler semantically. For example, it
can be shown that once a goal previously blocked on '!'
becomes unblocked, it remains unblocked through commit time.
No proposal for '?' which does things like unify X with Y?
to make X Y? in all its occurrences can do that.
Finally, for a more formal treatment of the !-annotation,
see next message.
-- Vijay Saraswat.
------------------------------
Date: Sun 5 May 85 15:39:36-EDT
From: Vijay <Vijay.Saraswat@CMU-CS-C.ARPA>
Subject: Semantic of the !-annotation. #2
Here is a more formal discussion of the '!' annotation.
Please see previous post for an informal motivation. It is
taken from my forthcoming tech rep 'Problems with Concurrent
Prolog'.
There are a number of other alternate formal definitions.
This semantics of '!' has been used to give two formal
semantics to Concurrent Prolog programs. Please see
succeeding messages.
-- Vijay A. Saraswat
The !-annotation.
In this section, we will think of terms as trees, that is,
as partial functions from the set of all possible paths
(i.e. finite and infinite sequences of natural numbers) to a
co-domain C +{\bot}, where C is the set of node-labels. If
the function is not defined for a given argument, we will
take its value to be \bot. Then terms are trees over the
co-domain of function symbols and variables.
We can now define ANNOTATIONS to be simply trees over the
domain {tt}+ {\bot}, with the interpretation that the (node
specified by the) path l is annotated by p iff p(l)=tt.
However, we would also like to insist that if a term is
annotated then all its super-terms are also annotated.
Therefore, we require that if p(l)=tt, then so is p(l'), for
all prefixes l' of l. [Ancestor condition]
An annotation p is APPLICABLE to a term t iff for all l,
t(l) is defined when p(l) is.
We would now like to give the semantics of an annotated
term. The annotations serve to restrict the set of terms
with which the annotated term can unify. Consider a term s
annotated by p and a term t. First we would like to express
the notion of a most general unifier for s and t which
ignores all the annotated nodes in s and the corresponding
nodes in t, if they exist.
The p-RESTRICTED MGU of two terms s and t, denoted by
mgu_r(p,s,t), where p is an annotation applicable to s, is
the most general substitution q such that p(l)# tt =>
(q(s))(l) = (q(t))(l).
According to the intuitive meaning of !, we must ensure that
all annotated terms unify against non-variable terms. This
means that when unifying a term s against t, if there is a
path l such that p(l)=tt and s(l)=s' and t(l)=t', we cannot
proceed until and unless t' is instantiated. But if t' is
instantiated, we can remove the annotation on s'. So we can
find mgu-!(p,s,t) by unifying the terms in s which are not
!-protected by p against the corresponding sub-terms of t,
i.e. by computing mgu_r(p,s,t). If this leads to
instantiating a variable in t which has a corresponding
sub-term in s that is !-protected, then we can remove this
annotation and start again. If mgu(s,t) exists, then the
process terminates in success iff there are no more
!-annotations left, and then mgu-!(p,s,t)= mgu(s,t) and in
failure iff all nodes !-annotated by the current p in t are
variables. Hence:
An !-MGU of two terms s, t where p is an annotation
applicable to s, is a substitution q_n such that there
exists a sequence p=p_0, ... p_n=\bot such that for all l.
p_{i+1}(l)=tt <-> p_i=tt & (q_i(s))(l) is a variable, where
q_i=mgu_r(p_i, s, t)
(p_n=\bot means that there are no nodes in p_n which have
the value tt.)
Note that mgu_r(\bot,s,t)=mgu(s,t).
------------------------------
Date: Sun 5 May 85 15:40:22-EDT
From: Vijay <Vijay.Saraswat@CMU-CS-C.ARPA>
Subject: A new commit: & #3
Now that we seem to have recovered from the discussions on
the meaning of '?' in Concurrent Prolog, let me initiate a
discussion on the role of '|'.
In the following, by CP I mean CP with '!' and without '?'.
The reason is that there doesn't exist (as yet) a consistent
definition of '?' and I consider '!' to be a perfectly
useful and simple substitute for '?'.
The semantics of CP can be given by specifying which
SLD-derivations are ADMISSIBLE, given a query and a
CP-program. I contend that the reason CP is not a logic
programming language is because it does not distinguish
failed admissible SLD-derivations from admissible
SLD-refutations. Because of its don't care non-determinism,
committing can only be locally angelic, i.e it chooses
values for its free variables such that its guard executes
successfully, but its body may still fail for the chosen
values. This means:
1. Validity of unannotated axioms is not sufficient for
partial correctness: a given query wil assuredly succeed
(or loop) ONLY if all finite admissible SLD-derivations
are refutations, which is a very strong condition.
2. There can be no notion of negation-as-failure
even with respect to admissible derivations. (i.e. at
best we can hope that negation means that no admissible
derivation for the query is a refutation... even that is not
compatible with '|'.)
3. Many Horn logic axiom definitions cannot be used in CP.
As an illustration, no version of the axioms:
p(X,Y):- t(X,Y).
p(X,Y):- t(X,Z), p(Z,Y).
annotated with CP's annotations can be guaranteed to work
correctly (i.e. compute the transitive closure of p/2) for
an arbitrary (Horn) definition of p/2. (For example,
consider the program:
p(0,1). p(0,2). p(1,3).
I. t(X!, Y!):- p(X,Y)| true.
II. t(X!, Y!):- p(X,Z), t(Z,Y)|true.
The query '?-t(0,3).' may fail because in II, p(X,Z) may
commit to:
p(0,2). )
There are two simple alternate interpretations for 'commit'
which distinguish between successful and unsuccesful
admissible derivations.
1. CP-amb or the '&' annotation: don't-know operator. (This
corresponds to McCarthy's famous "amb" operator in the
context of HLP.) Interpretes "commit" as "make global". It
does not snip off other OR-siblings, but instead continues
to follow them, allowing MULTIPLE commits of OR-siblings.
Each commit is to a different copy of the rest of the
environment. In effect whereas 'a:-g | b.' extends some
admissible refutation of 'g' by an admissible refutation for
'b' to return ONE (selected from possibly many) refutation
for 'a' (all this talk is modulo multiple environments),
'a:-g & b.' extends EVERY admissible refutation of 'g' by
an admissible refutation for 'b' and returns ALL of them as
refutations for 'a', thereby avoiding a local commitment to
one refutation of 'a'. Therefore, an SLD-derivation ends in
failure only if all admissible derivations are finite and
failing, just as for Prolog.
A completely formal description of & is given in my
forthcoming tech rep 'An operational semantics for
Concurrent Prolog'.
2.CP-backtrack or the '\' annotation. Interpretes "commit"
as "make global and freeze other OR-brothers". Here ONE
admissible SLD-derivation is followed until it terminates.
If it terminates in success, nothing is done. Failure
induces backtracking. For partial correctness, the exact
backtracking scheme used is not important (chronological,
dependency-directed), though of course pragmatically it is
quite important, as long as it can be guaranteed that the
system will not terminate in failure as long as even one
admissible SLD-derivation path has not been pursued. That
is, no FINITE SLD-derivation is admissible unless it is a
refutation or else all admissible derivations are finite and
failing.
Lemma: Given a CP program and a query, the set of possible
answers to a query is the same if the '|' is interpreted as
'commit', '&' or '\' uniformly in the program.
That is, | and & are equivalent as far as the success
semantics is concerned.
The relationship between interpreting '|' as commit, '&' and
'\' uniformly in a program is as follows:
[CP]
1.i Execution of a query ALWAYS terminates IFF all
admissible SLD-derivations are finite.
1.ii Execution may terminate in failure even if there
is an admissible refutation.
[CP-backtrack]
2.i As in 1.i.
2.ii Execution terminates in failure ONLY IF no
admissible SLD-derivation is a refutation. If a
query terminates in failure under CP-backtrack, it
will always terminate in failure under CP.
[CP-amb]
3.i Execution of a query always terminates IFF either
there is an admissible SLD-refutation or all
admissible SLD-derivations are finite.
3.ii As in 2.ii.
Caveat:
As in Prolog, allowing implicit search allows the user to
write very inefficient programs. On the other hand, for
whatever it is worth, much of Guy Steele's thesis work on
constraints can be recast in such a logic framework.
I would like to retain '|' much for the same reason that the
'!' is used in Prolog: sometimes it helps to signal
determinate situations and avoid redundant solutions. When
mixing '&' and '|', executing a '|' does not affect any
previous '&' that may have been executed: it just kills off
any remaining OR-siblings.
I leave you with the following example: (& represents the
"amb-commit").
prod(X!,Y!,Z):- Z is X*Y | true.
prod(X!, Y, Z!):- X =/= 0 | Y is Z/X.
prod(X, Y!, Z!):- Y =/= 0 | X is Z/Y.
prod(X, Y, Z!):- less(X,Z), less(Y, Z), Z := X*Y | true.
Z := X!*Y! :- Z is X*Y.
This can "solve" prod(X,X,16) to give X=4 provided that
less/2 is assumed defined as if by the collection of clauses
less(i#,j#):- true & true. for each value of i# and j# such
that i# < j#, so that it serves as a generator.
-- Vijay Saraswat
------------------------------
Date: Sun 5 May 85 15:41:48-EDT
From: Vijay <Vijay.Saraswat@CMU-CS-C.ARPA>
Subject: A meta-interpreter for CP[!,|,&] #4.
Here is a simple meta-interpreter for CP[!,|,&] in
CP[!,|,&]. Note that it is not possible to give as simple
an interpreter for CP[!,|] in CP[!,|]. This interpreter can
be extended to give an interpreter for CP[!,^,|,&] in
CP[!,^,|,&].
We define a predicate cp/1 which takes as input a goal and
solves it. The user-program is added in as clauses of the
form:
clause(Head:-Guard | Body):- true & true.
or
clause(Head:- Guard & Body):- true & true.
where:
1. All instances of '!' in Head are replaced by '$', which will
be regarded as a unary post-fix function symbol,
2. Guard and Body are sequences of goals of the form '{g_1, ...,
g_n}'.
In addition we also have the following axioms (which can be
added automatically):
For every functor f/n, (n>= 0) in the user-program, the
axioms:
f(X1,...Xn)! = f(Y1,...Yn)$:- X1 = Y1,...Y1=Yn | true.
f(X1,...Xn)$ = f(Y1,...Yn)!:- X1 = Y1,...Y1=Yn | true.
Then the interpreter is the following:
X=X:- X =\= G$.
unify(X!, Y):- X =Y | true.
execute(G!):- clause((Goal :- Guard | Body)),
unify(Goal, G),
execute_all(Guard) | execute_all(Body).
execute(G!):- clause((Goal :- Guard & Body)),
unify(Goal, G),
execute_all(Guard) & execute_all(Body).
execute_all({One|Rest}!):- true | execute(One), execute_all(Rest).
execute_all( true!):- true | true.
There are two cheats involved in this simple interpreter:
1. The term {g_1, ... g_n} (analogous to Dec-10 Prolog's [g_1,
... g_n]) is actually shorthand for the term g_1@(g_2@...
g_n)))..), where the @/2 operator is ASSOCIATIVE and
COMMUTATIVE. Hence {g_1,... g_n} represents a SET (actually
multi-set) of goals, rather than a list of goals, and when
unified against {X_1,... X_m|X} succeeds if 1 <=m <=n, and
unifies SOME m goals (not necessarily the FIRST m) from g_1
... g_n with X_1 ... X_m and the set of the rest of them
with X. We use sets instead of lists in order to avoid
giving priority to goals that might textually occur first in
the body of a clause; the same effect could be achieved by
using some random selection function. So the first cheat is
assuming that CP has a notion of associative-commutative
unification built in.
2. Second, we cheat in using the binary predicate =/=, which
has a weak form of var/1 built into it. Of course, given
=/=, we can simulate =/=, so we still have a complete
meta-interpreter. I do not know how to avoid using some
such device and still get an elegant program. Possibly by
representing user-program terms in a special fashion, one
may define a var/1 for user-program terms, but it is sure to
be messy.
The reason one cannot write as simple an interpreter for
CP[!,|] is that in CP[!,|] one cannot add the user-program
as a list of clauses to the interpreter as we have done
because then a call to clause(Head:-Guard|Body) would
succeed at most once, selecting some clause/1 clause at
random whereas we would like to select all clauses in
parallel and execute their guards concurrently,i.e. we DON'T
KNOW which clause we want. Hence we are forced to represent
the program explicitly as an argument to the interpreter, as
a list of clauses and that makes any meta-interpreter very
messy. But of course using the & in the body of clause/1
clauses achieves just the desired effect.
-- Vijay A. Saraswat
------------------------------
Date: Sun 5 May 85 15:42:29-EDT
From: Vijay <Vijay.Saraswat@CMU-CS-C.ARPA>
Subject: An operational semantics for CP. #5
Here is the abstract from a forthcoming tech rep "An
operational semantics for Concurrent Prolog".
-- Vijay A. Saraswat
Abstract. In this paper we present a simple
operational semantics for CP[!,|,&] using the notion of
Plotkin-style labelled transition system, which we believe
offers a simple, general framework for issues of concurrency
in Horn logic programming. The space of configurations we
work with naturally reflects the AND-OR process structure of
an executing concurrent logic program. The problems solved
in giving this semantics were the representation and
manipulation of a distributed environment and the effect of
two different kinds of commits: the don't care commit
originally proposed in \ref{Cp} and the don't-know commit
proposed in \ref{problems-cp}, together with their
interactions.
From the transition system, we extract various
`meaning-functions' for a program. We show that with
respect to one of these (the `success-semantics') a
CP[!,&] is the same as the corresponding CP[!, |]
program.
Essentially the transition system is a formalisation of a
derivability predicate in pure Horn logic, i.e. the
semantics can be looked upon as the specification in pure
Horn logic of a high-level interpreter for CP which
represents precisely the sequence of computations possible
for a given query and a given CP program.
------------------------------
Date: Sun 5 May 85 15:46:13-EDT
From: Vijay <Vijay.Saraswat@CMU-CS-C.ARPA>
Subject: A scenario semantics for CP. #6
Here is the abstract from my forthcoming CMU Tech report: "A
scenario semantics for Concurrent Prolog".
-- Vijay A. Saraswat
Abstract: In this paper we present a simple bottom-up
semantics for CP which captures the set of all possible
answer-substitutions for a query, given a CP[!,|,&] program.
The basic idea is to define a transformation analogous to
T_p:I rightarrow I (which defines the semantics of a pure
Horn logic program as lfp(T_p)). Because of CP's
annotations, however, we cannot interprete processes as
predicates over the underlying Herbrand base; we need more
operational information. We define the notion of {it
scenarios}, adapted from the semantics given in cite{brock}
for non-deterministic data-flow languages, and give the
success-semantics of a CP[!,|,&] program as lfp(S_p) of a
transformation S_p:I_s rightarow I_s from sets of scenarios
to sets of scenarios.
------------------------------
End of PROLOG Digest
********************