On 28-Sep-1999, Paul Hudak <[EMAIL PROTECTED]> wrote:
> > In order to prove that my program meets its requirements,
> > I need to prove not only that it terminates, but also that
> > the resources that it consumes are within the available
> > resource limits. To do that, I need to use the operational
> > semantics.
>
> Well, in this sense I think that operational semantics is overrated! In
> practice you run the program on some test cases and try a couple of
> different compilers and even then you cross your fingers :-)
True ;-) But good programmers do think about the operational semantics
while writing the program, even if they don't do any formal proofs.
> I have one final question:
>
> > For this program,
> >
> > Loop <- Loop. loop :- loop.
> > Q <- Loop & False. q :- loop, fail.
> >
> > the denotation of the program is the theory
> > { Loop <=> Loop } U { Q <=> Loop /\ False },
> > which is equivalent to the theory { ~Q } which asserts that Q is
> > false, and for that program and the same query
> >
> > <- Q. ?- q.
> >
> > the operational semantics says that the implementation may either
> > loop, report an error message, or report the answer "False".
>
> Are you saying that the operational semantics is nondeterministic?
Yes.
> Why can't the semantics be tweaked such that the operational and declarative
> semantics agree?
The declarative semantics for conjunction says that anything and false is
false because that is what classical logic says. We want our declarative
semantics to be based on classical logic rather than say 3-valued logic,
because classical logic is much easier to reason about, and is also much
more familiar to most people. So tweaking the declarative semantics is
not really an option.
Requiring the operational semantics to be complete w.r.t. the
declarative semantics (i.e. requiring implementations to report the
answer "False" for that query rather than looping or reporting an error
message) would require that implementations use a "fair" search strategy.
Unfortunately that would be prohibitively inefficient. Implementations
would essentially need to implement conjunction as parallel conjunction
(well, there are other approaches, but they too have efficiency problems).
Conjunction is the basic connective used throughout logic programs,
and if it had to be implemented as parallel conjunction, then implementations
would have to fork off a huge number of parallel threads.
> Or at least be such that the operational semantics is deterministic?
I did oversimplify slightly. Goedel always leaves the operational semantics
nondeterministic in cases like these. And that is the default behaviour of
Mercury too. But having a nondeterministic operational semantics does
have the potential to cause problems for portability. So the Mercury
language reference manual requires that implementations provide
a "strict sequential" mode in which the operational semantics is
deterministic. (In the strict sequential mode, the program above
would always loop.)
The reason that the strict sequential mode is not the _only_ mode is to
allow implementations additional freedom. This additional freedom is
intended to allow them to optimize code better, to parallelize code,
and to provide modes which offer better completeness and hence greater
expressiveness (e.g. lazy evaluation, smarter constraint solvers,
or a fair search strategy).
Cheers,
Fergus.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
