> It's very important that the operational semantics be sound
> with respect to the declarative semantics. It's much less
> important that it be complete w.r.t. the declarative semantics.
>
> Completeness (in this sense) is often highly overrated, IMHO.
I agree. Actually, it's not only overrated, its hard to achieve in
practice.
> 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 :-)
But I must stress that reasoning about nontermination as a value (_|_)
is really useful, in functional languages anyway. _|_ is also very
useful when reasoning about partial and infinite lists.
> > What
> > does the declarative semantics say for the denotation of a program,
> > written in one of these languages, that does not terminate?
>
> That depends. ...
Thanks for the interesting explanation. I hadn't thought much about
what a denotational semantics means for logic programs. 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? Why
can't the semantics be tweaked such that the operational and declarative
semantics agree? Or at least be such that the operational semantics is
deterministic?
-Paul
