[mercury-users] Indexing & operational semantics

[Fergus Henderson]

On 31-Jan-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> I'm pretty sure the answer to this question is `yes', but
> I just want to check.
> 
> I'm writing a term -> my_thing translator and I want to
> raise an error if it sees a syntax error or attempt to
> overload a primitive functor name.  Some of the clauses
> in the translator therefore look like this:
> 
> translate(functor(atom("/\"), Args, Ctxt), Out) :-
> 	require(list__length(Args) = 2, "/\ must have two args"),
> 	Out = f(Args).
> 
> Now it occurred to me that this could equally be written
> as
> 
> translate(functor(Name, Args, Ctxt), Out) :-
> 	Name = atom("/\"),
> 	require(list__length(Args) = 2, "/\ must have two args"),
> 	Out = f(Args).
> 
> which is something the compiler might very well do.  In this
> case, there's no dependency between the first and second lines
> of the clause body, so there's a chance that they will be
> reordered.

Yes, the "strict commutative" semantics described in the
language reference manual allows such reordering.

> This would be a disaster, since I only want require/2
> to be called provided Name = atom("/\").

In that case, you should either
	(1) use the "strict sequential" semantics,
	    which every Mercury implementation is required
	    to support (with the current Mercury
	    implementation, it is enabled by the
	    `--strict-sequential' option).
or 
	(2) avoid writing such constructs,
	    instead using code like the code that you give
	    below.

> Since this is the
> behaviour that I assume everybody expects, I infer that head
> unifications work like this:
> 
> translate(functor(Name, Args, Ctxt), Out) :-
> 	( if Name = atom("/\") then
> 		require(list__length(Args) = 2, "/\ must have two args"),
> 		Out = f(Args)
> 	  else
> 		fail
> 	).
> 
> with appropriate munging of output variables from the head 
> unification.

No, head unifications do not work like that.
If you want that effect, you need to write it like that.

> I just couldn't find anything about this in the
> reference manual.

On re-reading the relevant section, I agree that it
is not very clear about this point.

The "Semantics" chapter of the language reference manual
says that the axioms include the "completion of the clauses
for all predicates in the program".  This is the Clark completion,
which is defined (e.g. in standard texts on semantics of logic programs)
as follows.  For a set of clauses

	H1 :- B1.
	...
	HN :- BN.

whose heads H1 ... HN all have the same top-level functor F
with arity M, the completion is defined as

	all [X1, ..., XM]
		(F(X1, ..., XM) <=>
			(  F(X1, ..., XM) = H1 /\ B1
			\/ F(X1, ..., XM) = H2 /\ B2
			...
			\/ F(X1, ..., XM) = HN /\ BN
			)
		).

The operational semantics are then defined in terms
of executing the program in a particular order
or in one of a given set of allowable orderings.
When it says that the "strict commutative" semantics
allows conjunctions to be reordered, the intent is
that these conjunctions include the ones introduced
by taking the completion.

The current wording does not make this clear -- I'll
see what I can do to improve it.

However, one paragraph from the Mercury language reference
manual does seem particularly appropriate to quote here:

 |  This compromise allows Mercury to be used in several different ways.
 |  Programmers who care more about ease of programming and portability
 |  than about efficiency can use the strict sequential semantics, and can
 |  then be guaranteed that if their program works on one correct
 |  implementation, it will work on all correct implementations.  Compiler
 |  implementors who want to write optimizing implementations that do lots
 |  of clever code reorderings and other high-level transformations or that
 |  want to offer parallelizing implementations which take maximum
 |  advantage of parallelism can define different semantic models.
 |  Programmers who care about efficiency more than portability can write
 |  code for these implementation-defined semantic models.  Programmers who
 |  care about efficiency _and_ portability can achieve this by writing
 |  code for the commutative semantics.  Of course, this is not quite as
 |  easy as using the strict sequential semantics...

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- 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
--------------------------------------------------------------------------