[mercury-users] declarative kernels

[Fergus Henderson]

On 08-Mar-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> > From: Fergus Henderson [mailto:fjh at cs.mu.OZ.AU]
> > 
> > On 07-Mar-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> > > My picture of an io__state is that it records a
> > > *view* of the interface between a Mercury program
> > > at some point and the outside world.  That is, it
> > > records which files are currently opened by the
> > > program, whereabouts the read/write cursor is for
> > > each open file and so forth.  An io__state does 
> > > *not* reflect the state of the outside world.
> > 
> > How then would you distinguish between the following
> > two programs?
> > 
> > 	main --> print("yes\n").
> > 
> > 	main --> print("no!\n").
> > 
> > The position of the read/write cursor will be the same
> > in both cases, the only difference is the state of the
> > outside world (the contents of the screen, for example).
> 
> I see where the misunderstanding lies.  The program
> interacts with its environment by carrying out IO operations;
> it's io__state is updated as a function of its previous value,
> the just executed IO op, and the `reply' from the environment.
> Since the compiler can't predict how the io__state will be
> changed after a given IO op, it can't transform a "yes"
> program into a "no!" program (that is, print("yes") and
> print("no!") are *different* IO ops).
> 
> The flaw in this picture is that it requires a `hidden'
> notional state of the world, whereas taking an io__state to
> actually be the state of the world means that a Mercury
> program really is a relation between various world states,
> with no need for auxiliary machinery.

Right.  When we say that Mercury is "purely declarative", one of the
things that we typically mean by it is that we can reason about most
properties of programs (e.g. the set of possible answers that they might
give, but not operational properties such as whether they will terminate
or how long they will take) using just the declarative semantics,
i.e. treating `main' as just a relation to which all the usual laws of
predicate calculus apply.

If you say that the io__state does not contain the state of the
external world, and instead resort to having a `hidden' state
of the world, then you lose that property.

-- 
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.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------