[mercury-users] Trace goals

[Ralph Becket]

Nicholas Nethercote, Thursday, 28 September 2006:
> Hi,
> 
> I just learnt about trace goals.  They seem like a really useful feature. 
> But I was also surprised how little the manual discussed their effect on 
> semantics.

> For example, can a trace goal appear in nondet code?

Yes.  A trace goal is logically equivalent to just `true'.
The observable effects of trace goals should make no difference to the
*interpretation* of the behaviour of the program.
Trace goals should therefore not affect the behaviour of any part of the
program not in a trace goal.

> Are there 
> any strange effects they might have?  Or does saying "they're like impure 
> code marked with 'promise_pure'" mean that they "just work" due to the 
> purity system?

It means what I said above: because they cannot bind any variables, the
only way they can affect the rest of computation is by affecting the
IO state or through impure code.  The implicit "promise_pure" is
violated if a trace goal changes the interpretation of the behaviour of
the program.

For example, whether a program outputs progress messages via trace goals
or not should not affect the interpretation of its output.  So, yes, in
that sense trace goals do slightly affect the semantics of the program.

-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------