pf@romeo.cs.duke.edu (Pierre Flener) (03/07/90)
I post this article in the name of Yves Deville (Univ. of Namur, Belgium); it is his answer to Lee Naish's statement about my original posting. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- In article <17578@duke.cs.duke.edu> pf@cs.duke.edu (Pierre Flener) writes: > "Programming in PROLOG" is NOT equal to "Programming in Logic" > There are basically 4 ways to face this dilemma: > ... > (4) "Programming in PROLOG = Programming in Logic + ..."; i.e. you provide > the tools that allow you to program in Logic, and THEN convert your > program into a PROLOG program. He also briefly summarizes my book : Logic Programming : Systematic Program Development, Yves DEVILLE, International Series in Logic Programming, Addison-Wesley, March 1990. > This book can be loosely summarized as follows: starting from the above > viewpoint on Programming in Logic, 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]. The above statement is correct but is much imprecise. In order to make such an approach realistic, the following questions should be answered : - What is the specification of a logic procedure (or program)? - What is a logic description? - What does it mean that a logic description is correct wrt a specification? - How to construct a correct logic description? - What does it mean that a logic program is correct wrt a specification? - How to derive a correct and efficient PROLOG program from a logic description? - ... These questions are treated in detail in the abovementioned book. I will therefore not extend on this subject here. In article <???> lee@munnari.oz.au (Lee Naish), Lee Naish's answer to Pierre Flener introduces the interesting problem of types : > 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, A.D) :- append(B, C, D). The question here is what does it mean to be equivalent (or correct) with respect to the specification, and especially how can types be handled? Let me illustrate on this append example the approach we follow. Two different approaches are possible : 1. Types are preconditions. 2. Explicit type checking in the code. A good choice is to consider explicit type checking at the logic description level, and to consider types as preconditions at the PROLOG level. A logic description of append would thus be : append(L1,L2,LApp) <==> L1=[] & LApp=L2 & list(L2) v L1=[H|T1] & append(T1,L2,TApp) & LApp=[H|TApp] With this logic description, we have that append(l1,l2,l3) is true (with l1, l2 and l3 ground terms) iff l1, l2, l3 are lists and l3 is the concatenation of l1 and l2. At the PROLOG level, a straightforward translation of the above logic description yields the following first PROLOG program : append([], L2, L2) :- list(L2). append([H|T], L2, [H|TApp]) :- append(T,L2,TApp). Is the literal list(L2) necessary? If an approach of explicit type checking is taken, then it should be kept. The resulting program is however not efficient (when L2 is a ground list) and not easy to use (when the arguments are variables, the solutions from the second clause are never reached). We prefer to consider types as preconditions at the PROLOG level. But what does it mean since parameters could be variables or neither ground nor variable. In this append example, the precondition will be the following : For a given call append(A,B,C), where A, B, C are PROLOG terms (not necessarily ground), There must exist ground instances of A, B and C which are lists. It is the programmer's responsability (i.e. the user of the procedure) to make sure this precondition is fulfilled when the procedure is used. If there is no type checking at the PROLOG level, then types should also be considered as postconditions. In this append example, the postcondition will be the following : For a given call append(A,B,C), where A, B, C are PROLOG terms (not necessarily ground), If S is a computed answer substitution for this call, Then there must exist ground instances of (A)S, (B)S and (C)S which are lists. It is here the implementor's responsability (i.e. the one who builds the procedure) to make sure that this postcondition will be fulfilled by the computed answer substitutions. In our append example, the list(L2) literal is then useless according to the above statements. We thus get the classical PROLOG program: append([], L2, L2). append([H|T], L2, [H|TApp]) :- append(T,L2,TApp) It is advantageous to consider explicit type checking at the logic description level for the following reasons. First, this approach can lead to a type checking program, if desired. Second and more important, when type checking is not considered at the PROLOG level, the type checking literals introduced at the logic level cannot always be suppressed. In some problems, they must be kept in order to avoid incorrect answers. A simple example, called compress(List_Char, Compact_List_Char), can be found in Section 9.6 of the abovementioned book. The problem of types is one of the various problems a programmer should face when constructing a PROLOG program (e.g. order of literals, termination, occur check, negations, cuts, number of solutions, ...). The use of a methodology encourages the programmer to explicitely consider all these problems at the right moment and in a systematic way. Yves Deville, University of Namur, Belgium yde@info.fundp.ac.be =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
lee@munnari.oz.au (Lee Naish) (03/07/90)
In article <18009@duke.cs.duke.edu> pf@romeo.cs.duke.edu (Pierre Flener) writes: >I post this article in the name of Yves Deville (Univ. of Namur, Belgium); >In this append example, the precondition will be the following : > For a given call append(A,B,C), > where A, B, C are PROLOG terms (not necessarily ground), > There must exist ground instances of A, B and C which are lists. >It is the programmer's responsability (i.e. the user of the procedure) to make >sure this precondition is fulfilled when the procedure is used. > > If there is no type checking at the PROLOG level, then types should also >be considered as postconditions. In this append example, the postcondition >will be the following : > For a given call append(A,B,C), > where A, B, C are PROLOG terms (not necessarily ground), > If S is a computed answer substitution for this call, > Then there must exist ground instances of > (A)S, (B)S and (C)S which are lists. >It is here the implementor's responsability (i.e. the one who builds the >procedure) to make sure that this postcondition will be fulfilled by the >computed answer substitutions. I agree this seems to be a reasonable way of handling the problem in standard Prolog. The Mycroft & O'Keefe type checking scheme could be considered an implementation of this (placing more restrictions on the program to make type checking decidable). However, one disadvantage is that the computation rule can determine whether the preconditions are satisfied. This must make the theory more complicated, and the system more difficult to use in systems which allows coroutines or parallel execution. The following use of append is always "safe" but, depending on the execution order (eg, if append is called before the is_list call completes), the precondition might not be met. safe_append(X, Y, Z) :- is_list(Z), append(X, Y, Z). With a left to right computation rule, you would want to put the call to append first (to avoid infinite loops), so its not feasible to write this generic safe_append (you would have to carefully examine the input/output modes of all uses of append, and possibly have two versions of safe_append - one which tests Y, the other which tests Z). In the scheme which I have proposed, we can say that safe_append is type correct (which is independent of the computation rule), and hence it is sound and complete with respect to the (typed) specification whatever (sound and complete) execution method is used. lee