🚀 go-pugleaf

In article <17578@duke.cs.duke.edu> pf@romeo.cs.duke.edu (Pierre Flener c/o awb) writes:
> a 3-step methodology is
>proposed: (1) elaboration of a specification; (2) construction of a logic
>description that is correct & complete wrt the specification [sole concern
>is the declarative semantics of Logic]; (3) derivation of a PROLOG program
>that is correct & complete wrt the specification [i.e. coping with
>everything that makes the difference between Logic and PROLOG programming].
>
>Any comments on our approach ???

Various Gurus and True Believers of logic programming have been saying this
sort of thing for a long time.  I don't think its quite that simple.
Efficient Prolog programs are NOT equivalent to natural specifications.
Take append for example.  In the natural specification, all arguments
must be lists.  This is not true of the standard (efficient) coding.  If
the coding was changed, so it is equivalent to the specification, an
extra test would be needed:

	append([], A, A) :- list(A).
	append(A.B, C, D) :- append(B, C, D).

If the specification of append(A,B,C) was changed, so it is equivalent to
the normal coding, it would be:

	A is a list, B is a list if and only if C is a list,
	and C has the same "elements" as A and B in that order.
	The definition of an element needs to be extended to
	non-lists.

The asymmetry of the specification with respect to the first two
arguments reflects the implementation of lists.  If the representation
of lists allowed access to the last element faster than the first
element then the specification of an efficient append would be different.
This is not a desirable property of specifications.

It is tempting to use an "incomplete" specification such as

	If A and B are lists, C is B concatenated onto A.

However, when negation as failure is used, incompleteness turns into
unsoundness.  An append definition which is correct with respect to the
definition above can cause incorrect answers to reasonable queries.
This is all discussed in the following paper:

%A Lee Naish
%T Specification = program + types
%J Proceedings of the Seventh Conference on the
Foundations of Software Technology and Theoretical Computer Science
%C Pune, India
%D December 1987
%E Kesav V. Nori
%O published as Lecture Notes in Computer Science 287
by Springer-Verlag
%P 326-339

I now have an almost final draft of a revised and extended version,
entitled "Types and the intended meaning of logic programs".

	lee