🚀 go-pugleaf

In article <2562@randvax.UUCP>, narain@randvax.UUCP (Sanjai Narain) writes:
> 
> In a sense, an executable specification is quite easy to obtain.  Suppose
> one can specify a problem in a formal language.  Then, one can use any
> complete theorem prover for it to query that specification.  So, what is
> to distinguish doing this in full first-order logic from doing the same in
> definite clauses (with SLD-resolution)?  It is the possibility of
> specifying algorithmic knowledge in the latter.

	True. An interesting point to note is that for uniform proofs, one
only needs to consider sub-formulae of the goal in order to find proofs,
and so each of the logical connectives corresponds to an operation in a
search space. Hence, one can interpret the logical connectives as some kind
of instruction. This, I think, is getting closer to what you describe as
algorithmic knowledge above. 

> Often, when people are told about the merits of Prolog, especially its
> logical basis, they assume they are relieved of the responsibility to
> specify algorithmic knowledge. [more]

	I think this is due to the way that a successful SLD-derivation can
be interepreted as a proof in first-order logic. That does not mean that
a similar proof has a successful SLD-derivation. For example, if the goal
A,B succeeds in Prolog, then we may interpret this as a proof of A \land B,
but that does not necessarily mean that the goal B,A will succeed, as it
may loop. Hence, the interpretation is "one-way". However, there are some
cases in which we can reverse the direction -- ie when the program does not
rely on a particular computation rule and ordering of clauses. Thus if we
rely only on the existence of a proof, rather than the manner in which it
is found, then programmers are relieved of the responsibility to specify
algorithmic knowledge. Otherwise, if we want a stronger result, we need to
do more work. As ever, it is all a trade-off. 

> But the interesting aspect is that Prolog allows one
> to think about algorithms in a logical manner (in addition to offering
> good expressive power).

	This is the part that should be stresses, I think, rather than
thinking of Prolog as programming in logic. 


				Cheers,
					James.