Subject: Re: predicate logic & using accumulater

From: "Richard A. O'Keefe" <[email-masked]>
Date: Mon, 10 Jan 2000 15:45:54 +1300 (NZDT)

Uwe Mayer wrote:
	I am learning from a book, called "Clause and Effect" by
	William F. Clocksin.  In worksheet 6 he introduces the use of an
        accumulator in a procedure, calculating the length of a list:
	
	1.
	length([], 0).
	length([H|T], N) :- length(T, Nt), N is Nt+1.
	
	2.
	length(L,N) :- accumulate(L, 0, N).
	
	accumulate([], A, A).
	accumulate([H|T], A, N) :- A1 is A+1, accumulate(T, A1, N).
	
	Furthermore he states that the second version should be preferred.
	WHY?  For debugging purposes?

It has nothing to do with debugging, and everything to do with converting
body recursion to tail recursion.  The point is that the second version
can be executed in bounded (and rather small) memory space, while the
first version cannot.  This really has very little to do with Prolog
per se; efficient techniques for compiling tail calls and the accumulator
passing method for converting body calls to tail calls were first
developed for functional languages.

	my second question is more theoretical.
	in analysis phrases like "for all" and "there exists"
	(dt.  Quantoren) are used.
	
"quantifiers" in English.

	my second book states that we are only using first order predicate logic in
	prolog. (fine)

Not even all of that.

	and that in first order predicate logic we use these <Quantoren> on
	individuals and varriables (fine)

Not true.  Quantifiers introduce logical variables, which stand for
individuals.  You cannot "use quantifiers on" individuals.

	BUT that in second (and higher) predicate logic these <Quantoren> work on
	predicate varriables. (not fine)
	
On the contrary, extremely fine and very important.
They may also work on function variables.

	i have problems immagening such a construction.

Here is an example of a second-order predicate:

    for all binary relations P: S x S -> Bool	<- second order quantifier
        reflexive(P) if and only if
           for all elements X: S		<- first order quantifier
              P(X, X)

If you want to say that the composition of any two reflexive relations
is reflexive, but the composition of two transitive relations is not
necessarily transitive, that's a second-order statement.

Prolog cannot quantify over functions or predicates (you _can_ with a
bit of work quantify over *names* of existing predicates, but that is
not true higher order quantification) but there are logic programming
languages that can, to some degree.

	first case is clear, f.e.:
	
	define a partial map censor such that the goal censor(X,Y) maps
	the input list X of words onto the output list Y of words in
	which no prohibited words from prohibit(Z) appears.

	prohibit(bother).
	prohibit(blast).
	prohibit(drat).
	prohibit(fiddlestick).
	
	censor([],[]).
	censor([X|T],[X|L]) :- not prohibit(X), censor(T,L).
	censor([X|T],L) :- prohibit(X), censor(T,L).
	
	the second clause of censor can be described as "censor matches
	the head of the input list to the head of the output list, if FOR ALL
	VALUES of the head of the input list:  prohibit(head of input list)
	fails and recurse on the tail of the input list".

In fact the second clause is
	(forall X) (forall T) (forall L)
	~prohibit(X) & censor(T, L) => censor([X|T], [X|L]).

	this would be quantifying (using <Quantoren>) on varriables.

*All* quantifiers of *any* order involve variables.  The question is
what the possible *values* of those variables might be.  In this clause,
the implicit universal quantifiers do NOT in any useful sense quantify
over "variables", they quantify over terms in the Herbrand Universe
(the set of labelled trees that can be made using functors that appear
in the program consistently with their arities).

	Can anyone give me an example of quantifying on predicate varriables?

	censor(Filter, [], []).
	censor(Filter, [X|T], [X|L]) :- ~Filter(X), censor(Filter, T, L).
	censor(Filter, [X|T],    L ) :-  Filter(X), censor(Filter, T, L).

Here the values of Filter would be predicates.
In Prolog, the values of Predicates can be closures; *names* of existing
predicates together with zero or more arguments already supplied.
(Pure) Prolog, however, cannot construct *new* predicates or functions
as part of its solution process (some logic programming languages can).

	Why are such constructions not possible in Prolog?

Because 
    propositional calculus (no quantifiers) is decidable
    unary function-free predicate calculus is decidable
    first-order predicate calculus is *semi*-decidable
    second-order predicate calculus is *un*-decidable in general.
and
    higher-order programming (with *given* function or predicate
    values) as in functional programming can be "faked" quite easily
    by automatically augmenting each Prolog program with the definitions

	% call/1
	call(p(X1,X2,X3)) :- p(X1, X2, X3).
	...
	% call/2
	call(p(X1,X2), X3) :- p(X1, X2, X3).
	...
	% call/3
	call(p(X1), X2, X3) :- p(X1, X2, X3).
	...
	% call/4
	call(p, X1, X2, X3) :- p(X1, X2, X3).
	...

    where each predicate in the program is represented in each of these
    tables.  That allows code like

	censor(Filter, [], []).
	censor(Filter, [X|T], L) :-
	    ( call(Filter, X) -> L = R ; L = [X|R] ),
	    censor(Filter, T, R).

	why are they useless?
	
They are NOT useless.  Higher-order quantifiers are quite useful.
Prolog is just one point in the spectrum of possible logic programming
languages.  Certain engineering choices were made, which permitted
efficient implementation on 1970s hardware with 1970s knowledge.