From p.singleton@keele.ac.uk Wed May  9 12:57:08 2001
Received: from scooby.lineone.net (scooby-s1.lineone.net [194.75.152.224])
	by swi.psy.uva.nl (8.11.2/8.11.2) with ESMTP id f49Av7322258
	for <prolog@swi.psy.uva.nl>; Wed, 9 May 2001 12:57:07 +0200 (MET DST)
Received: from keele.ac.uk (host213-123-74-153.dialup.lineone.co.uk [213.123.74.153] (may be forged))
	by scooby.lineone.net (8.10.2/8.9.3) with ESMTP id f49AuwH07261;
	Wed, 9 May 2001 11:56:59 +0100 (BST)
Message-ID: <3AF91D4E.94274ACD@keele.ac.uk>
Date: Wed, 09 May 2001 11:34:54 +0100
From: Paul Singleton <p.singleton@keele.ac.uk>
Organization: SmartArts Computing Consultancy
X-Mailer: Mozilla 4.74 [en] (WinNT; U)
X-Accept-Language: en
MIME-Version: 1.0
To: prolog@swi.psy.uva.nl
CC: "Richard A. O'Keefe" <ok@atlas.otago.ac.nz>
Subject: Re: [SWIPL] sorting database?
References: <200105040103.NAA212362@atlas.otago.ac.nz>
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit

"Richard A. O'Keefe" wrote:

> ...
> In general, relying on the order in which solutions are returned is
> unwise.  Occasionally it is extremely unwise.

Since Prolog's execution strategy is well-defined and deterministic,
it is surely legitimate and in some cases clearly useful that the spec
of a library procedure (etc.) might define the order in which solutions
are returned, and that code which calls such a procedure might rely on
this?

I bet there's lotsa code out there which relies on e.g.

    (   member(X, List) ->

committing to the frontmost element of List which unifies with X (rather
than e.g. the rearmost).

But I'm not sure whether the accepted spec of member/2 includes a
guarantee about the order in which list elements are visited?

Could SWI-Prolog legitimately implement member/2 as

  member(X, [_|Xs]) :-
      member(X, Xs).

  member(X, [X|_]).

i.e. generate elements "backwards"?  Would this break legacy apps,
and whose fault would it be? :-)

Isn't the problem that: while we can formally state some mode, type and
determinacy properties of code, such that we can statically (& mechanically)
check that the specified behaviour of a called procedure satisfies the
assumptions of a call, it is less easy (infeasible?) to specify and check
solution-order assumptions and properties?

Perhaps if we disregard the actual orders of solutions, and merely note
whether a procedure's solution order is defined or not, then we could
statically check code for some degree of consistency, and e.g. generate

  wARNING: The semantics of ->(p(A,B),_) is dependent on the solution
  order of p/2, which is undefined.

Paul Singleton

