🚀 go-pugleaf

In article <1944@randvax.UUCP> narain@randvax.UUCP (Sanjai Narain) writes:
>There is another reason why functional programming is more elegant
>than logic programming, which has to do with manipulation of
>infinite structures. Suppose one wants to compute the first 3 elements of
>an infinite list l. In logic one may say:
>	compute_list_l(L),first(3,L,X).
>By coroutining compute_list_l and first, one may solve first(3,X), but
>one would never be able to solve compute_list_l fully.  Thus, no theorem
>would be proved, so within the strict framework of logic programming
>one would not be entitled to infer anything.
>
>In functional programming however, one may evaluate the term:
>
>	first(3,compute_list_l)
>
>which would neatly reduce to its normal form, namely the first 3 elements
>of l.

When I saw this, I thought "that can't be right, functional programming
and logic programming are hard to tell apart, they can't be that different."
And of course they aren't.

Consider a Horn clause definition (I avoid Prolog notation because we're
talking about logic programming, not Prolog as such):

	list_of_ones(cons(1,X)) <- list_of_ones(X);

	first(0, L, nil) <- true;
	first(s(N), cons(X,Xs), cons(X,Ys)) <- first(N, Xs, Ys);

Now ask a coroutining system the question

	? Ans | first(s(s(s(0))), Xs, Ans), list_of_ones(Xs);

We get the intermediate results
answer(Ans) <- first(s(s(s(0))), Xs, Ans), list_of_ones(Xs);  % do first
answer(Ans) <- Xs = cons(X1,Xs1), Ans = cons(X1,Ys1),	      % do list...
	       first(s(s(0)), Xs1, Ys1), list_of_ones(cons(X1,Xs1));
answer(Ans) <- Ans = cons(1,Ys1),
	       first(s(s(0)), Xs1, Ys1), list_of_ones(Xs1);
	by calling first then list_of_ones
answer(Ans) <- Ans = cons(1,cons(1,Ys2)),
	       first(s(0), Xs2, Ys2), list_of_ones(Xs2);
	by two more such steps
answer(Ans) <- Ans = cons(1,cons(1,cons(1,Ys3)),
	       first(0, Xs3, Ys3), list_of_ones(Xs3);	% do first
	and the final result is
answer(cons(1,cons(1,cons(1,nil)))) <- list_of_ones(Xs3);

Surely this is a valid theorem?  (The rules give us no way to find a
finite Xs3, but the theorem only says that _if_there_were_ such an
Xs3, the answer would be [1,1,1].)

If we consider a functional definition:
	def list_of_ones = cons(1, list_of_ones);
	def first(0,L) = nil
	+++ first(s(N),cons(H,T)) = cons(H,first(N,T));
and ask for the value of the expression
	first(s(s(s(0))), list_of_ones)?
we get precisely the same kind of response:
the value of the expression is cons(1,cons(1,cons(1,nil)))
PROVIDED that list_of_ones has some finite value.  Of course,
it is unavoidable in functional programming that some expressions
do NOT have (non-bottom) values...

Each answer is as valid as the other.  In functional languages one
hacks lazy evaluation by moving away from "strict" evaluation.  We
could probably work out a non-strict logic if we tried.  (Hmmm...)