[m-dev.] Re: Assocative predicates

[Peter Schachte]

On 27 Apr 1998, Lee Naish wrote:
> Wow!  I get sick for a few days and there are a squillion articles to
> followup to (lucky comp.lang.prolog is as boring as usual).

I wondered why you wer so quiet on this topic.  Well, let that be a lesson
to you! 

> Re: admissibility/preconditions etc

I confess I haven't read any of your cited papers, but I'm going to reply
anyway, at my own peril.  

> Several different notions of inadmissibility can be supported.  Eg
> inadmissibility = ill-typedness in the scheme above.  However, it seems
> 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.  Also, there may
sometimes be restrictions on individual arguments that don't seem important
or prevalent enough to make it worth thinking of that as a "type."  I'd
rather think of generalized types (in Mercury this would be regular types
with attached constraints) as admissibility conditions on all predicates
with arguments of that type.

> I think its important to recognise the notion of admissibility when
> designing certain aspects of the language.  The meaning of general
> assertions should probably be restricted so as to apply to only
> admissible atoms.  There should be some way to declare admissibility.
> One simple way is to allow special meta predicate(s) admissible
> (and/or inadmissible) in assertions.  eg
> 
> :- assertion admissible(list_merge(X,Y,Z)) => sorted(X).

This is exactly what I had in mind.  But I think admissibility is an
important enough concept to merit it's own declaration syntax, leading me to
propose the syntax:

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

(It might be argued that list_merge should be a predicate of 3 sorted_lists,
in which case this declaration would be unnecessary, but humor me for this
example.)  This is what I'd like to say about list_merge/3, but the question
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? 

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. 
Further, it promises that on success, the conditions will hold for all
output arguments. 

Put another way, in --check-assertions mode (or whatever the Mercury
compiler's equivalent of not defining NDEBUG is), the compiler should do
something like inserting the admissibility conditions of a goal before the
goal, and the mode analysis will migrate the individual conditions to the
right places.  Unfortunately, I don't think this sort of approach will work. 
Certainly you don't want to just insert the admissibility conditions,
because then the code will just fail rather than printing an error message
and aborting. "The right thing"  is actually pretty tricky to do without
giving the compiler the opportunity to optimize away the tests (in order not
to mess up the mode analysis, the inserted code must be det, and it will
have no useful outputs).

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

> It would be
> nice to rethink the semantics of Mercury using three values and give
> admissibility more prominence and its own syntactic construct

Agreed.

-Peter Schachte               | Any man who is under 30, and is not a
mailto:pets at cs.mu.OZ.AU       | liberal, has not heart; and any man who is
http://www.cs.mu.oz.au/~pets/ | over 30, and is not a conservative, has no
PGP: finger pets at 128.250.37.3 | brains. -- Winston Churchill