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

[Peter Schachte]

On 4 May 1998, Lee Naish wrote:

> When you write merge its important to know what context it will be called
> from, and that determines what assumptions you can use when coding it.
> For example, assume the last argument will be constrained to be sorted
> (perhaps merge will be called only in mode (out,out,in)).  You can then
> code merge using structural induction on the last argument and end up
> with quite a neat correct version.  Interestingly, it does no
> comparisons!

You may be able to get that anyway:

	merge([], Xs, Xs).
	merge(Xs, [], Xs).
	merge([X|Xs], [Y|Ys], [X|XYs]) :-
		X =< Y,
		merge(Xs, [Y|Ys], XYs).
	merge([X|Xs], [Y|Ys], [Y|XYs]) :-
		X >= Y,
		merge([X|Xs], Ys, XYs).

When compiling clause 3 for mode (out,out,in) with the supplied
admissibility requirements, it may be possible to automatically infer from
the fact that that X =< every element of XYs and merge(Xs, [Y|Ys], XYs) the
fact that necessarily X =< Y.  Similarly for clause 4.  I do think it makes
sense to use admissibility constraints in this sort of way.

> The normal version is coded using the assumption that the
> first two arguments are constrained (typically this means input).  It
> will be correct if called backwards also.  An appropriate definition of
> admissibility is
> 
> :- admissible list_merge(X,Y,Z) => (sorted(X), sorted(Y) ; sorted(Z)).

But then the atom list_merge([1],[2],[2,1]) would be admissible.  I don't
think it should be (of course it will always fail, but I think then we're
confusing failure with inadmissibility).  Or is your idea of admissibility
something like "if it's admissible and it succeeds, then it computes the
correct answer?" 

> (if a predicate is known to work in more modes then the admissibility
> criteria can be made *weaker*).  Of course we still have correctness
> criteria such as
> 
> :- assertion list_merge(X,Y,Z) => sorted(X), sorted(Y), sorted(Z).

I'm not sure this is still desirable in conjunction with the supplied
admissibility condition.  It's a lot of repetition.  See below.

> >My thought was that it means that the predicate is only guaranteed to behave
> >in the intended way if all the conditions hold for all input arguments. 
> 
> Its not always possible to separate out conditions corresponding to a
> subset of the arguments.  eg we might have two args, a list and its
> length; what if only one is input?  ie. there can be "relationships among
> arguments" as you mentioned earlier.

In such cases (that part of) the condition is not required to hold on call. 
But the condition still must hold on success.  The idea is that no predicate
should ever produce a solution which would be deemed to be inadmissible as a
call.  This is why it seems to me that it shouldn't be necessary to have the
same information as both assertions and admissibility constraints.  The
former says "call me with anything you like, I promise the situation will be
*this* if I succeed."  The latter says "if you call me with inputs that
satisfy the part of this constraint that can be checked, I promise the
situation will be *this* if I succeed; if they don't satisfy it, may do
anything."

I'd be interested to see an example where this approach won't work.  After
extensive research, I've concluded that this should handle everything (ie, I
thought about one example and it seemed to work).

> >Further, it promises that on success, the conditions will hold for all
> >output arguments. 
> 
> The truth values true and inadmissibile are distinct; this seems to try
> to combine truth and inadmissibility in some way.

I don't see that.  I am using 2-valued logic to determine admissibility, but
I think that should be ok.  (Though there may be a problem if the predicates
you're using as admissibility criteria themselves have admissibility
constraints that aren't met; then whose fault is it?  I guess it must be
the declarations that are wrong). 

> >You'd probably actually want to generate code something like
> 
> >	...,
> >	(  \+ sorted(X) ->
> >		report_inadmissibility("sorted(X)", "list_merge(X,Y,Z)",
> >					File, Line)
> >	;  \+ sorted(Y) ->
> >		report_inadmissibility("sorted(Y)", "list_merge(X,Y,Z)",
> >					File, Line)
> >	;  list_merge(X,Y,Z),
> >	   (   \+ sorted(Z) ->
> >		    report_inadmissibility("sorted(Z)", "list_merge(X,Y,Z)",
> >					   File, Line)
> 
> You should report a wrong answer rather than inadmissibility here.

Agreed.

> For the reverse mode you would want to report inadmissibility if the
> third arg was unsorted and an error if either of the first two were
> unsorted.

Agreed.


-Peter Schachte               | The time for action is past! Now is the time
mailto:pets at cs.mu.OZ.AU       | for senseless bickering!
http://www.cs.mu.oz.au/~pets/ |     -- Ashleigh Brilliant 
PGP: finger pets at 128.250.37.3 |