Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!munnari.oz.au!lee
From: lee@munnari.oz.au (Lee Naish)
Newsgroups: comp.lang.prolog
Subject: Re: Programming in PROLOG vs. Programming in Logic
Keywords: explicit type checking, types as pre/post-conditions
Message-ID: <3289@munnari.oz.au>
Date: 7 Mar 90 01:26:26 GMT
References: <18009@duke.cs.duke.edu>
Sender: news@cs.mu.oz.au
Reply-To: lee@munmurra.UUCP (Lee Naish)
Organization: Comp Sci, University of Melbourne
Lines: 49

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