cwp@otter.hple.hp.com (Chris Preist) (08/19/88)
Could any of you give me information on the representation of universal quantification in the various dialects of PROLOG available please? We have a problem which contains universal quantifications within the body of a clause, and wish to represent these in as pure and logical a fashion as possible. Thanks for any help forthcoming. Chris
goldfain@osiris.cso.uiuc.edu (08/29/88)
Clocksin and Mellish chapter 10 discusses this and related notions. Basically, all variables in a Prolog clause are understood to be universally quantified. It is existential quantification that is somewhat harder to express.
hamid@hilbert.uucp (Hamid Bacha) (08/29/88)
In his reply to: cwp@otter.hple.hp.com (Chris Preist), <7000001@osiris.cso.uiuc.edu> goldfain@osiris.cso.uiuc.edu writes: > >Clocksin and Mellish chapter 10 discusses this and related notions. > >Basically, all variables in a Prolog clause are understood to be universally >quantified. It is existential quantification that is somewhat harder to >express. You seem to have some confusion concerning universal and existential quantification. What the previous message was referring to was universal quantification in the body of a clause. What Clocksin & Mellish were talking about was universal quantification at the beginning of a clause. When you move a universal quantifier from the body of a clause to the outside of that clause, it becomes an existential quantifier. The following example provides a distinction between the two cases: p(X) :- forall(Y) q(X,Y) can be rewritten as: forall(X) (p(X) <- forall(Y) q(X,Y)) forall(X) (p(X) v ~ forall(Y) q(X,Y)) forall(X) (p(X) v exists(Y) ~q(X,Y)) forall(X) exists(Y) (p(X) v ~q(X,Y)) forall(X) exists(Y) (p(X) <- q(X,Y)) or in PROLOG (assuming it is allowed): exists(Y) p(X) :- q(X,Y). In fact, the above is not an acceptable logic program clause. As the following example (supplied by VS Subrahmanian) shows: b <- forall(X) q(X) q(a) <- q(s(X)) <- q(X) The least fixed point of this program is attained after omega+1 iterations of the Tp operator, instead of omega steps which is the case for pure logic programs.
jah@lfcs.ed.ac.uk (James Harland) (08/30/88)
In article <1600016@otter.hple.hp.com> cwp@otter.hple.hp.com writes: > >Could any of you give me information on the representation of universal >quantification in the various dialects of PROLOG available please? We >have a problem which contains universal quantifications within the body >of a clause, and wish to represent these in as pure and logical a fashion >as possible. > >Thanks for any help forthcoming. > >Chris In article <7000001@osiris.cso.uiuc.edu> goldfain@osiris.cso.uiuc.edu writes: > >Clocksin and Mellish chapter 10 discusses this and related notions. > >Basically, all variables in a Prolog clause are understood to be universally >quantified. It is existential quantification that is somewhat harder to >express. I don't think this is quite what the original request was about. You are correct in saying that all variables in a Prolog clause are understood to be universally quantified *at the front of the clause*. For example, given the Prolog clause p(X) :- q(X,Y). we may interpret this as a formula of first-order logic as all x all y p(x) if q(x,y) which is equivalent to all x p(x) if exists y q(x,y) This is well-known and appears in Lloyd's book. As I understood the original posting, the question referred to clauses like all x p(x) if all y q(x,y) which is different from the above clauses. I'm no expert, but two Prolog systems which address this sort of issue are Nu-Prolog (guru: Lee Naish, lee@mulga.oz) and Lambda Prolog (guru: Dale Miller, dale@linc.cis.upenn.edu). Chris <cwp@otter.hple.hp.com>: I tried to email you, but it bounced, and when this article came along I decided to post. I hope this is of some help. Cheers, James Harland jah@lfcs.ed.ac.uk
johnson@csli.STANFORD.EDU (Mark Johnson) (09/01/88)
(1988) Expires: References: <1600016@otter.hple.hp.com> <7000001@osiris.cso.uiuc.edu> <745@etive.ed.ac.uk> Sender: Reply-To: johnson@csli.UUCP (Mark Johnson) Followup-To: Distribution: Organization: Center for the Study of Language and Information, Stanford U. Keywords: The paper by Kanamori and Horiuchi in vol 2. of the Proceedings of the 4th Intl Conference on Logic Programming (MIT Press, 1988) is relevant to the question of existential and universal quantifiers in Prolog. They discuss (and prove "correct") the "Unfold-Fold" transformation, which, among other things, is capable of transforming a predicate definition of the form: less_than_all(X,L) :- % X is less than _every_ member of L list(L), % L must be a list (member(!Y,L) -> X < !Y). % if Y is an elt of L, then X < L. into a predicate definition of the form: less_than_all(X,[]). less_than_all(X,[Y|L]) :- X<Y, less_than_all(X,L). The variable !Y in the first definition of less_than_all is called a universal variable, because it is interpreted as being universally quantified within the body of the clause. In many circumstances the Unfold-Fold transformation can transform a definite formula (containing universal variables) into a definite clause that can be used by Prolog. In its most general form the Unfold-Fold transform can be difficult to apply usefully, since there are many ways of unfolding and then folding a set of formulae, and not all of them result in useful programs. I think that it may be possible, however, to find a restricted class of formulae for which a simple control strategy can direct the application of the Unfolding and Folding operations in such a way that they result in predicate definitions useful in Prolog systems. Mark Johnson