Admissibility (was Assocative predicates)

[Lee Naish]

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

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

Yes, all sorts of optimization *might* be able to be done by a smart
compiler but I'm sure Fergus wouldn't like to guarantee that they all
will be and my main point is that programmers generally leave out
important information about the declarative reading of their predicates
when coding and the bits which are left out depend on the intended
modes.

> > :- 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?" 

Yes.  If it's admissible and it succeeds, then it *should* compute the
correct answer.  Admissibility is part of the interface specification I
guess.

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

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

The assertion above does not hold: list_merge can succeed with junk.
Admissibility says "*irrespective of any claims to the contrary*, the
implementor malkes no warranty of the correctness of this procedure
if this condition is violated".  The assertion is only true in the
context of the admissibility condition.  One reason why there is so much
overlap in this example is the fact that two modes are involved.  If you
look at a single moded version (say forward) then admissibility only
talks about the first two args and the assertion will only talk about
the last arg.

	lee