[net.lang.prolog] PROLOG Digest V3 #19

RESTIVO@SU-SCORE.ARPA (04/17/85)

From: Chuck Restivo (The Moderator) <PROLOG-REQUEST@SU-SCORE.ARPA>


PROLOG Digest           Wednesday, 17 Apr 1985     Volume 3 : Issue 19

Today's Topics:
                    Query - Redundant Comparisons,
       Implementations - C-Prolog & Optimal Logics & Semantics
----------------------------------------------------------------------

Date: Fri 12 Apr 85 08:43:28-PST
From: PEREIRA@SRI-AI.ARPA
Subject: C-Prolog cloning

It is becoming more and more difficult to keep track
of all the versions of C-Prolog that people mention
on this Digest.  In particular, I was surprised to
read that there is anything in sysbits.c in the
version 1.5.edcaad that checks for some file
descriptor being a terminal. You see, I *wrote*
1.5.edcaad, and my copy of the source has no such
thing... Maybe this is a novel manifestation of
self-modifying code :-).

-- Fernando

PS. EdCAAD is not on this net. To get the latest
EdCAAD C-Prolog, write to them using paper mail.
wgr

------------------------------

Date: Sat, 13 Apr 85 02:01:07 est
From: "Dennis R. Bahler" <DRB%Virginia@csnet-relay.arpa>
Subject: Advice for redundant comparisons

I have a problem which could use the advice of an expert
Prolog programmer, which I am not.

I have defined a predicate closure/2, defined over the
power set of an arbitrary set, and wish to test its
instantiations for NONconformance to an axiom, call it
c5, which states that

        CL(X int Y) = CL(X) int CL(Y)

(where CL(X) means closure(X), and 'X int Y' means X
 intersect Y).

What I have now is:

c5:-    closure(X,CX), closure(Y,CY), not(eqset(X,Y)),
        intersection(X,Y,IXY), closure(IXY,CIXY),
        intersection(CX,CY,ICXCY),
        not(eqset(CIXY,ICXCY)),
        printerror(5), etc....

with the utility functions defined in reasonable ways.

My problem is that the default execution of Prolog will
test all PERMUTATIONS of pairs of X and Y, i.e.,

        X = [a,b] Y = [b,c] and then
        X = [b,c] Y = [a,b]
        etc.

and thus does exactly twice as much work as necessary.

I would like advice about how to efficiently test non-redundant pairs
of clauses, something on the order of:

        for (i=0; i<MAX; i++)
                for (j=i+1; j<=MAX; j++)
                        { clause[i] <relop> clause[j] }

-- Dennis Bahler

------------------------------

Date: Fri 12 Apr 85 13:22:12-PST
From: Joseph A. Goguen <GOGUEN@SRI-AI.ARPA>
Subject: Optimal Logics for Logic Programming

Several people have asked me for references for the
results about largest logics having initial models.
Here they are:

A. Tarlecki, "Abstract Algebraic Institutions which
Strongly Admit Initial Semantics", University of Edinburgh,
Computer Science Department, report number CSR-165-84, 1984.

 B. Mahr and J.A. Makowsky, "Characterizing Specification
Languages which Admit Initial Semantics", Theoretical
Computer Science, volume 31, pages 49-60, 1984.

B. Mahr and J.A. Makowsky, "An Axiomatic Approach to
Semantics of Specification Languages", Proceedings, 6th GI
Conference on Theoretical Computer Science, Dortmund,
Springer-Verlag Lecture Notes in Computer Science, Volume
145, 1983.

J.A. Makowsky, "Why Horn Formulas Matterin Computer Science:
Initial Structures and Generic Examples", Department of
Computer Science, Technion, Haifa, Israel, 1985.

The first report is the most general, covering cases such
as strongly typed first order equational logic with
subsorts.  The next three cover only the the Horn clause
cases, and the last (and first) correct some errors in the
second and third reports.

A careful statement of the results showing that first order
Horn clause logic with equality admits initial models in
exactly the same way as equational logic (and thus also
admits user defined generic abstract data types in the same
way as the special case of equational logic) can be found
in our paper on Eqlog in Jnl. Logic Programming, vol.1,
no.2, Theorem 1; of course the result also applies to the
special case of Horn clause logic without equality, which
is (pure) Prolog, where the initial model coincides with the
traditional minimal Herbrand model.  Proofs will be found
in the revised and extended version of our JLP paper, to
appear in the book edited by de Groot and Lindstrom
entitled "Functional and Logic Programming".

------------------------------

Date: Sun 14 Apr 85 22:13:34-PST
From: Joseph A. Goguen <GOGUEN@SRI-AI.ARPA>
Subject: Semantics of Logic Programming

I agree with Uday Reddy that control is a rather
neglected grandchild in logic programming.  However,
Bob Kowalski's famous slogan "Programming = Logic +
Control" expresses a clean factorization into two
components, so presumably they can be studied and
mastered separately.  In fact, control has been
studied and mastered to a considerably lesser extent;
but perhaps we are about to see some real progress
in this area.  In particular, I hope that some of
the various annotations being suggested can be given
a clean semantics that doesn't violate the logic
component, i.e., that only tells how to solve the
same problem faster.

I don't understand where Reddy got the idea that Horn
clause logic is {true, undefined}-valued.  Every book
on logic or logic programming I ever saw takes the
absolutely traditional view that sentences (in this
case, ground Horn clauses) are either true or false
(the trick of representing them as functions having
values doesn't come up unless you want to translate
clauses into, say, equational logic, as Dershowitz
does); Lloyd's new book is a lovely exposition of
pure logic programming.  It may be that Reddy has
a way to use {true, undefined} as a *domain* for
a denotational semantics of Horn clause programs

-- but that is an entirely different kettle of fish,
and I claim a messier one.  The basic idea of Horn
clause programming semantics (as in the famous 1976
van Emden and Kowalski JACM paper) is that Horn clause
programs give the answers that are true of the initial
model (of course, they call it the minimal Herbrand
model).  So (pure) Prolog is an initial model-based
language.  Theorem 1 of our Jnl. Logic Programming
paper explains this (if you work through the math).

Perhaps it's worth giving a bit more detail here.  The
first point is that pure Horn clause programming doesn't
involve any equations, so the minimal Herbrand model
contains just terms, rather than equivalence classes of
terms, which makes everything simpler (Eqlog is our
generalization for the case where there are equations);
in particular, equality is just syntactic equality, as
in Prolog.  If you add equations, the only difference is
that you compare reduced forms to check equality; but this
is no extra work, since (presumably) you already have the
reduced forms as a result of doing the computations that
you wanted done anyway.  This is because term reduction is
actually the (very powerful and efficient, by the way) form
of computation that is specified by the equations -- i.e.,
logic programming with equations has operational semantics
given by term reduction.  All this should be familiar from
our OBJ language and also work of O'Donnell.

Non-termination is an interesting issue, both for Prolog
and for other initial model-based languages; we think that
we have a good solution based on the theory of continuous
algebras, in which initial algebras contain infinite
computation trees, but that is too complicated to explain
here, except perhaps to say that it seems to be a fairly
straightforward generalization of the usual theory.  By
the way, Prolog II is (in effect) taking a similar line.

Regarding higher-order logic, I agree with David Warren
that we don't really need it in logic programming.  Yes,
it is elegant and powerful.  But it is hard to read, hard
to write, hard to compute with, and generally altogether
more complicated than first order logic.  Even so, we don't
need denotational semantics to explain it, since there is
lots of nice theory in logic, including higher order
equational logic (which will do higher order functional
programming for us, such as Backus' FP) and higher order
model theory; we can even have higher order abstract data
types (due to work by Parsaye and Poigne).

I'd like to repeat what I see as the major moral to be
drawn from much of the discussion in the Digest: we need
more research on making pure logic programming powerful
enough so that we can do practical programming in it
easily and naturally.  Good topics include control,
input-output, states (so we can get rid of assert and
retract), combining functional and logic programming,
termination issues (including lazy evlauation and streams),
polymorphic typing, and (if you don't agree that Eqlog has
already solved them) generic modules and subtypes (as for
multiple inheritance).

------------------------------

End of PROLOG Digest
********************