declarative & procedural semantics

[Fergus Henderson]

The following was forwarded to the goedel-users mailing list. 
I'm CC'ing this to the mercury-users list too.  Apologies in advance
to all those avid declarative programming fans who are subscribed
to both lists and who will hence get this twice ;-)

Vyacheslav Petukhin (slava at math.isu.runnet.ru) wrote:

>  > For the better mutual understanding of the further discussion I 
>  > offer to agree about terminology. I suppose that the term 
>  > "Declarative Programming Language" usually implies a fixed 
>  > procedural semantics, i.e.
>  >  Declarative Programming Language =
>  >        Syntax + Declarative Semantics + Procedural Semantics.
>  > And if we speak about implementation of a such language, we mean 
>  > that the procedural semantics can not be changed.

I agree with this description.

>  > This usually 
>  > means that we must get same output for various implementations.

This does not follow.  You only get the same output if

	(a) the procedural semantics is deterministic

and

	(b) there are absolutely no areas of unspecified behaviour

There are a number of declarative languages for which (a) is true, e.g.
Haskell, Escher, pure Prolog.  However, I'm pretty sure that there are
no real-world programming languages for which (b) is true.  As soon as
you add a standard library, and start dealing with issues like I/O,
etc., you start having to give up some of these guarantees.

There are also a number of declarative languages for which (a) is not
true, e.g. Goedel, concurrent Clean, concurrent Haskell.  Giving up a
deterministic procedural semantics is sometimes necessary, e.g. if you
want concurrency.

Anthony Bowers <bowers at compsci.bristol.ac.uk> wrote:

>  I claim the following to be a theorem:
>  --------------------------------------
>  If you have a fixed search order, and pruning, you can always write 
>  programs so that the declarative semantics and procedural semantics 
>  do not coincide.
>  --------------------------------------
>
>  Notes :-
> 
>  (a) The declarative semantics is obtained by simply leaving out any 
>      pruning operators.
> 
>  (b) Pruning includes the ability to accept the first answer as the 
>      only answer at the top level. It also includes the use of 
>      quantifiers to obtain the same effect.
> 
>  (c) A language with a fixed search rule can be declarative if it has
>      no pruning at all (all answers are returned at the top level,
>      no use of !).
> 
>  The theorem implies that all theoretical LP research does not apply 
>  to languages with those properties. That is very sad! There's no 
>  partial evaluation, semantics based analysis, program transformation 
>  etc. that can be done on real Prolog programs.

I think you overstate things a bit here.  You can still do partial
evaluation.  You can still do a certain amount of program transformation.
A fixed search rule does prevent some of them, but you can still do
quite a bit.  See e.g. Mixtus. 

Furthermore, a lot of the problems with Prolog are related to features
of Prolog other than the fixed search rule.  For example, the
possibility of `read(X), call(X)' makes dead code elimination
impossible in Prolog.  If you have a nice clean declarative language
and you give it a fixed search rule, you can still apply a lot of that
theoretical LP research, and you can still do a lot more in the way of
program transformation than you can do with Prolog.

>  The choice we have is:
> 
>  1. Accept non-deterministic search rules
>  2. Accept languages without pruning
>  3. Move to computational models not based on search at all (e.g. 
>     Escher)
>  4. Abandon true declarative programming, and stick with Prolog.
> 
>  Take your pick!

There's definitely a trade-off here.  But you don't have to take your
pick at programming language design time.  Instead, your programming
language can provide support for more than one option from that list,
allowing programmers to choose whichever trade-off is best for them.
This is the approach taken we've taken in Mercury.

In Mercury, you can choose options 2 or 3 by simply not using certain
features of the language.  If you only use functions and predicates
whose determinism is `det', then you get option 3.  If you never use
committed choice nondeterminism (i.e. none of your predicates has
determinism `cc_multi' or `cc_nondet'), then you get option 2.
If you do use these features, then the default is option 1.
However, you can select option 4 (well, a fixed computation rule --
it's still not Prolog!) with a compile-time flag.  This is a feature of
the Mercury language, not just the current implementation: the
Mercury language reference manual requires that all implementations
provide a mode of invocation in which they will use the specified
"strict sequential" computation rule.

Also you've overstated option "4" quite a bit here.
A fixed computation rule doesn't necessarily mean you've abandoned
declarative programming (and it certainly doesn't mean you have to
stick to Prolog!).  It may just make testing, porting, and termination
proofs a bit easier.

-- 
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.