[m-dev.] Re: assertions (was: Assocative predicates)

[Fergus Henderson]

On 24-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> > NU-Prolog has a syntax for something like this:
> > 
> > 	:- pred foo(T) where foo(X) : invariant(X).
> > 
> > 	:- pred merge(list(T), list(T), list(T)) where
> > 			(merge(L1, L2, _) : sorted(L1), sorted(L2)).
> 
> I think syntactically that's not very good; it would be better to stray from
> NU Prolog syntax for this.  I think preconditions are much the same sort of
> thing as assertions, and should be syntactically similar.

Well, Lee thinks that preconditions are much the same sort of
thing as types.  He has a pretty strong case for it, too ;-)
For example, if the precondition is *not* part of the type of the
arguments, then arguably it would be wrong to write

	:- assertion associative_pred(merge).

because merge is not associative for all values of its inputs,
only for the ones that satisfy the preconditions.

Remember that associative_pred is defined as

	:- pred associative_pred(pred(T, T, T)).
	:- spec associative_pred(P) <=> all [As, Bs, Cs, ABCs]
			(P(As, Bs, ABs), P(ABs, Cs, ABCs)) <=>
			(P(Bs, Cs, BCs), P(As, BCs, ABCs)).
			  
and here the universal quantifier `all [As, Bs, ...]' is actually
an abbreviation for `all [As in T, Bs in T, ...]'.
Thus the assertion `associative_pred(merge)' is true only
if the type of the argument is `sorted_list(_)', not `list(_)'.

I'm not sure about what is the best way to view preconditions.
In some ways, preconditions seem to me like a fairly operational notion.
In other ways, they seem like a high-level notion, related to 3-valued
interpretations: if a goal's precondition is not satisfied, then that
goal is inadmissable, i.e. the intended interpretation of that goal
is a third truth value "inadmissable".

> > Yes, NU-Prolog also has a syntax for this:
> > 
> > 	:- type sorted_list(T) == list(T) where (X : sorted(X)).
> 
> Perhaps in the interest of consistency, this should be something like
> 
> 	:- valid_term T => Conditions.

Consistency with what?

I think it may make more sense to consider type invariants to be
parts of types.  Considering them to be like assertions
for a special predicate `valid_term' may be straining things a little, IMHO.

> So in summary, here are the new declarations/directives I'd like:
> 
> 	:- specification Atom <=> Body.
> 	:- assertion Body.
> 	:- admissible Atom => Body.
> 	:- valid_term Term => Body.	% or maybe Term::Type => Body.

Which of these, if any, would require the body to be mode-correct?

`admissible' declarations correspond to preconditions, but
there's nothing that directly corresponds to postconditions.
Both specifications and assertions of the form `:- assertion Atom => Body'
could be considered as post-conditions.

It might be better to have seperate declarations (e.g. 
`:- precondition Atom => Body' and `:- postcondition Atom => Body')
for assertions that are to be checked at run-time.

I suppose that in addition to postconditions you can also have
a notion of failconditions, to catch goals which should succeed
but instead return no solutions: a specification `Atom <=> Body'
implies a failcondition of `not Atom => not Body' which can be
used for runtime checking.

-- 
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.