[mercury-users] exceptions and cc_multi

[Fergus Henderson]

On 29-Nov-2000, Michael Day <mikeday at corplink.com.au> wrote:
> 
> > In many cases, propagating the cc_multiness all the way back up to
> > main is probably the right solution.
> 
> So, most programs that attempt to catch exceptions will have a cc_multi
> main. In this kind of predicate:
> 
> do_something :-
> 	do something impure,
> 	try(risky_operation),
> 	undo the impure thing that was done before,
> 	rethrow the exception if there was one.
> 
> Is do_something as a whole cc_multi or det?  Or in other words, would using
> promise_only_solution here be lying to the compiler, or not? (When
> risky_operation can be an arbitrary predicate...)

It would be OK to use `promise_only_solution' here, provided that
`risky_operation' is det or semidet (not cc_multi or cc_nondet),
and that `do something impure' and `undo the impure thing' are both det.

Proof:

	1. By assumption, all the operations involved except `try' can
	   return at most one solution for any given values of their
	   inputs.

	2. The declarative semantics of `try' are defined as
		       try(Goal, Result) <=>
		               ( Goal(R), Result = succeeded(R)
		               ; not Goal(_), Result = failed
		               ; Result = exception(_)
		               ).
	   which is equivalent to
	  		try(Goal, Result) <=>
				( 
				   (if Goal(R) then
				   	Result = succeeded(R)
				   else
				   	Result = failed
				   )
				;
				   Result = exception(_)
				).

	   This implies that for any given Goal, if Goal(R) has at most
	   one solution R, then try(Goal, Result) has at most one
	   solution for which Result \= exception(_).

	3. Since the Mercury implementation must be sound,
	   step 2 implies that `try' can return at most one
	   solution for which Result \= exception(_).
	   (Operational semantics must be sound w.r.t. declarative semantics.)

	4. For the cases where `try' returns `exception(_)',
	   your `do_something' will throw an exception.
	   Combined with 1 & 3, this implies that
	   `do_something' can return at most one solution.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------