Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is meant by "logical purity" in Prolog?

What is meant by "logical purity" (in the context of Prolog programming)? The logical-purity tag info says "programs using only Horn clauses", but then, how would predicates like if_/3 qualify, using as much as it does the cut, and the various meta-logical (what's the proper terminology? var/1 and such) predicates, i.e. the low-level stuff.

I get it that it achieves some "pure" effect, but what does this mean, precisely?

For a more concrete illustration, please explain how does if_/3 qualify as logically pure, seen in use e.g. in this answer?

like image 814
Will Ness Avatar asked Aug 11 '15 12:08

Will Ness


People also ask

What is predicate logic in Prolog?

Prolog is a programming language based on predicate logic. A Prolog program attempts to prove a goal, such as brother(Barney,x), from a set of facts and rules.

Does Prolog use first order logic?

Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily as a declarative programming language: the program logic is expressed in terms of relations, represented as facts and rules.

What is functioning of cut operator in Prolog?

The cut, in Prolog, is a goal, written as !, which always succeeds, but cannot be backtracked. Cuts can be used to prevent unwanted backtracking, which could add unwanted solutions and/or space/time overhead to a query. The cut should be used sparingly.


1 Answers

Let us first get used to a declarative reading of logic programs.

Declaratively, a Prolog program states what is true.

For example

natural_number(0).
natural_number(s(X)) :-
        natural_number(X).

The first clause states: 0 is a natural number.

The second clause states: If X is a natural number, then s(X) is a natural number.

Let us now consider the effect of changes to this program. For example, what changes when we change the order of these two clauses?

natural_number(s(X)) :-
        natural_number(X).
natural_number(0).

Declaratively, exchanging the order of clauses does not change the intended meaning of the program in any way (disjunction is commutative).

Operationally, that is, taking into account the actual execution strategy of Prolog, different clause orders clearly often make a signifcant difference.

However, one extremely nice property of pure Prolog code is preserved regardless of chosen clause ordering:

If a query Q succeeds with respect to a clause ordering O1, then Q does not fail with a different ordering O2.

Note that I am not saying that Q always also succeeds with a different ordering: This is because the query may also loop or yield an error with different orderings.

For two queries Q1 and Q2, we say that G1 is more general iff it subsumes G2 with respect to syntactic unification. For example, the query ?- parent_child(P, C). is more general than the query ?- parent_child(0, s(0))..

Now, with pure Prolog programs, another extremely nice property holds:

If a query Q1 succeeds, then every more general query Q2 does not fail.

Note, again, that Q2 may loop instead of succeeding.

Consider now the case of var/1 which you mention, and think of the related predicate nonvar/1. Suppose we have:

my_pred(V) :-
        nonvar(V).

When does this hold? Clearly, it holds iff the argument is not a variable.

As expected, we get:

?- my_pred(a).
true.

However, for the more general query ?- my_pred(X)., we get:

?- my_pred(X).
false.

Such a predicate is called non-monotonic, and you cannot treat it as a true relation due to this property: This is because the answer false above logically means that there are no solutions whatsoever, yet in the immediately preceding example, we see that there is a solution. So, illogically, a more specific query, built by adding a constraint, makes the query succeed:

?- X = a, my_pred(X).
true.

Thus, reasoning about such predicates is extremely complicated, to the point that it is no fun at all to program with them. It makes declarative debugging impossible, and hard to state any properties that are preserved. For instance, just swapping the order of subgoals in the above conjunctive query will make it fail:

?- my_pred(X), X = a.
false.

Hence, I strongly suggest to stay within the pure monotonic subset of Prolog, which allows the declarative reasoning along the lines outlined above.

CLP(FD) constraints, dif/2 etc. are all pure in this sense: You cannot trick these predicates into giving logically invalid answers, no matter the modes, orders etc. in which you use them. if_/3 also satisfies this property. On the other hand, var/1, nonvar/1, integer/1, !/0, predicates with side-effects etc. are all extra-logically referencing something outside the declarative world that is being described, and can thus not be considered pure.

EDIT: To clarify: The nice properties I mention here are in no way exhaustive. Pure Prolog code exhibits many other extremely valuable properties through which you can perceive the glory of logic programming. For example, in pure Prolog code, adding a clause can at most extend, never narrow, the set of solutions; adding a goal can at most narrow, never extend, it etc.

Using a single extra-logical primitive may, and typically will, already destroy many of these properties. Therefore, for example, every time you use !/0, consider it a cut right into the heart of purity, and try to feel regret and shame for wounding these properties.

A good Prolog book will at least begin to introduce or contain many hints to encourage such a declarative view, guide you to think about more general queries, properties that are preserved etc. Bad Prolog books will not say much about this and typically end up using exactly those impure language elements that destroy the language's most valuable and beautiful properties.

An awesome Prolog teaching environment that makes extensive use of these properties to implement declarative debugging is called GUPU, I highly recommend to check out these ideas. Ulrich Neumerkel has generously made one core idea that is used in his environment partly available as library(diadem). See the source file for a good example on how to declaratively debug a goal that fails unexpectedly: The library systematically builds generalizations of the query that still fail. This reasoning of course works perfectly with pure code.

like image 73
mat Avatar answered Oct 19 '22 08:10

mat