[mercury-users] re: determinism question

[Fergus Henderson]

On 03-Nov-1998, Don Smith <dsmith at cs.waikato.ac.nz> wrote:
> The type, mode, and
> determinism declarations of a Mercury procedure are not complete
> specifications of the procedure's semantics.

Certainly.

> I rather tend to regard
> the code itself as an (executable) logical specification.
> I thought that's the main idea of logic programming!

That's one way of looking at things.  I wouldn't say it is the
only way of looking at things.  I think that looking at things
only in that way misses some important points.  But that
is another topic which we could probably discuss at great length,
so for the sake of this discussion I'm happy to look at things
in those terms.

However, you need to be careful to distinguish between the logical
specification, and the way that logical specification is expressed
in code.  The code denotes a particular logical relation;
any other code that denotes the same relation gives the same
specification.  You can change the code without changing the
specification (for example, by applying a meaning-preserving
transformation).  If predicates are to be treated as units
of encapsulation, then changing the code in this way should
not affect the legality of callers.  Conversely, if the form (rather
than just the meaning) of the code in the body of a predicate were to
affect the legality of calls to that predicate, then the form of that
code must be considered part of the interface specification for that
predicate, which would be an undesirable change from the status quo.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.