[mercury-users] Indexing & operational semantics

[Peter Schachte]

> I'd rather not add sequential conjunction to the language on the
> grounds that it's not terribly declarative;

But it *is* declarative, or at least what I mean by sequential
conjunction is.  All it does is let you choose between failure and
error/nontermination, which commutative conjunction can't let you do.

For example, it would be nice in Mercury to have predicate
ensure_sorted/1 which succeeds if its argument is sorted, otherwise it
raises an exception.  Of course such a predicate would be det and
would have no outputs, which would allow the compiler to optimize it
away.  But if you write

	ensure_sorted(X) && p(X, ...)

then when p is called, X will be guaranteed to be sorted.  So this
conjunction allows you force an exception rather than a failure.

You can also use it the other way.  If division by 0 raises an
exception, and you want to compute a quotient, but fail if the
denominator is 0, then you can write

	X \= 0 && Y = Z/X

Which ensures you'll get a failure rather than an exception.

More formally, we can define the success and failure sets of a && b as
follows:

	s(a&&b) = s(a) /\ s(b)
	f(a&&b) = f(a) \/ (f(b) /\ s(a))

(where /\ is intersection and \/ is union).  So you see the success
set of a&&b is the same as for a,b, but the failure set requires that
a have terminated in success or failure.

I suggest no pragmatic meaning for a&&b:  as soon as it can be
determined that a will terminate without error, b can be permitted to
execute.  If this can be determined at compile-time, then they can be
reordered at compile-time.

> in a sense, we already
> do have a sequential `and' in if-then-else:
> 
> 	if A then B else fail
> <=>	(A, B) ; (not A, fail)
> <=>	(A, B)
> 
> but if-then-else has to have condition-first operational semantics
> for the obvious reasons (although there is a danger, I suppose, that
> the compiler will optimise line 1 to line 3, leaving us in the same
> position.)

The reason for if-then-else to necessarily be sequential isn't obvious
to me, except that you really do need to have some way to get
sequential conjunction.  Some modes that (a,b) ; (\+a,b) can support
cannot be handled by (a->b;c).  With a real sequential conjunction,
the need for if-then-else to be sequential decreases, although since
it's a bit clumsy to simulate it with sequential conjunction, it
should probably stay.  It'd be nice to have a logical if-then-else,
though.

> For my purposes, the reordering of `A then B' to `B then A' causes
> trouble when B can raise an exception or has some side effect.  The
> language recognises the problem of code with side-effects through
> (im)purity annotation and the compiler knows that it cannot reorder
> such code.  It seems to me that the same thing needs to be done for
> code that can raise exceptions.

Nontermination is another problem: if B can loop when A fails, you
probably don't want B executed before A.

> One thing I've often thought would be handy would be an option to
> turn various compiler flags on and off at the predicate or even
> clause level, for example:
> 
> :- pragma compile_with(foo/2, [strict_sequential_semantics]).

Sequential conjunction is even finer grain, a lot more concise, and
works at the semantic rather than pragmatic level.

-- 
Peter Schachte                     Mr. Spock succumbs to a powerful mating
mailto:schachte at cs.mu.OZ.AU        urge and nearly kills Captain Kirk. -- TV
http://www.cs.mu.oz.au/~schachte/  Guide, describing the Star Trek episode
PGP: finger schachte at 128.250.37.3  _Amok_Time_ 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------