[m-dev.] assertions

[Mark Anthony BROWN]

Fergus Henderson writes:
> 
> Mark Anthony BROWN <dougl at cs.mu.OZ.AU> wrote:
> > Maybe we should avoid the word `assertion' altogether?
> > I am finding it confusing.
> 
> A good idea.
> 
> I agree with your suggestion that "promise" is a better term to use;
> perhaps we can use "assertion" as the generic term that includes all
> different kinds of assertions.

That sounds OK.


> > 			*	*	*
> > 
> > Regardless of what we call it, the assumption seems to have been made
> > that what we wish to assert is a valid formula.  For the purposes of
> > declarative debugging it is useful to be able to make meta-level
> > assertions, such as:
> > 
> > 	:- assertion valid(F).
> > 	:- assertion satisfiable(F).
> 
> Isn't that distinction just an issue of quantifiers?
> i.e. if `F' is `p(X)', then can't you write those two statements as
> 
> 	:- assertion all [X] p(X).	% p(X) is valid
> 	:- assertion some [X] p(X).	% p(X) is satisfiable
> 
> ?
> 

Yes, you can write those statements that way.  The advantages of my
proposal are:
	- You don't have to use closed formulas; if F contains
	  free variables, there is no issue about whether the implicit
	  quantification should be universal or existential.  This
	  has been a point of contention in the past.
	- (As I previously mentioned) assertions could be made about
	  inadmissibility within the same framework.  This would allow
	  us to treat pre-conditions in a similar way to post-conditions
	  (which can be expressed by validity).

Maybe this scheme can also accommodate higher level assertions, such as

	:- assertion associative(P).

?  I haven't thought about this aspect very much.

Cheers,
Mark.
-- 
Mark Brown, PhD student            )O+  |  "Another of Fortran's breakthroughs
(m.brown at cs.mu.oz.au)                   |  was the GOTO statement, which was...
Dept. of Computer Science and Software  |  uniquely simple and understandable"
Engineering, University of Melbourne    |              -- IEEE, 1994
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------