On 28-Sep-1999, Paul Hudak <[EMAIL PROTECTED]> wrote:
> > I don't think it is correct to say that the notion of _|_ invariably
> > creeps into the denotational semantics.
> > But perhaps I am misusing the term "denotational semantics".
> >
> > In languages such as Goedel and Mercury, the declarative
> > semantics does not deal with nontermination or runtime errors.
> > Instead, those issues are handled by a separate operational semantics.
> >
> > So, wouldn't the declarative semantics of Goedel and Mercury count
> > as denotational semantics, if suitably expressed?
>
> I suppose so, although a common goal of semanticists is that the
> denotational semantics and operational semantics are the same.
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.
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.
> What
> does the declarative semantics say for the denotation of a program,
> written in one of these languages, that does not terminate?
That depends.
There's basically two cases, programs which have no answer,
and programs which have an answer but for which the implementation
happens to not deliver any answer (due to an infinite loop,
lack of resources, or some other problem).
Here's an example of the first case.
For this program
% Goedel % Mercury
Loop <- Loop. loop :- loop.
Q <- Loop. q :- loop.
the denotation of the program is the theory { Loop <=> Loop } U { Q <=> Loop },
which is equivalent to the empty theory. (Actually there are some axioms
in the theory for equality and so forth, but we can ignore those.)
For that program and this query
<- Q. ?- q.
the operational semantics says that the implementation is required to
either loop or report an error message.
Here's an example of the second case.
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".
> (A denotational semantics aims to give a "denotation" -- a value -- to
> every program. So if you say that the declarative semantics is
> undefined in the case of a nonterminating program, then in some sense
> the semantics is incomplete. To make it complete, perhaps all you have
> to do is equate "undefined" with _|_ !)
For the two logic programming languages I discussed above,
every program has a denotation, but not every query has an answer.
--
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.
