Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!uflorida!mephisto!mcnc!duke!romeo!pf
From: pf@romeo.cs.duke.edu (Pierre Flener)
Newsgroups: comp.lang.prolog
Subject: Re: Programming in PROLOG vs. Programming in Logic
Keywords: explicit type checking, types as pre/post-conditions
Message-ID: <18009@duke.cs.duke.edu>
Date: 6 Mar 90 16:59:36 GMT
Sender: news@duke.cs.duke.edu
Lines: 131

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

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-