Admissibility (was Assocative predicates)

[Lee Naish]

Peter Schachte <pets at students.cs.mu.oz.au> writes:

> > that a more natural view is inadmissibility = ill-typedness of "input"
> > arguments

>I don't think this goes quite far enough.  I'd like to be able to include
>relationships among arguments as admissibility conditions.

This can be done in the schemes I have proposed (the description above
is meant to give a general idea - ill-typedness can apply to the input
arguments collectively and the whole notion of "input arguments" is not
too intuitive for multi-moded predicates).

>	:- admissible list_merge(X,Y,Z) => sorted(X), sorted(Y), sorted(Z).

>is what to do with the sorted/1 condition applied to output arguments?  You
>do want them all there, otherwise you would be missing conditions in some
>modes, and I'd rather not have separate conditions for different modes.  So
>what does this condition mean in the list_merge(in,in,out) mode? 

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

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

Using the latter declaration we can detect buggy computations involving
merge and the former declaration can tell us if the bug is in the
definition of merge (eg merge([1],[2],[2,1]) or merge([2,1],[],[1,2]))
or in the surrounding context (eg merge([2,1],[],[2,1])).

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

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

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

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.

	lee