[mercury-users] Uniqueness modes etc

[Fergus Henderson]

On 30-Dec-2003, Dr Mark H Phillips <mark at austrics.com.au> wrote:
> On Mon, 2003-12-29 at 16:30, Fergus Henderson wrote:
> > > But would it really be a problem?  This is what I am not sure about.
> > 
> > Yes, it would really be a problem.
> > Several problems, actually:
> > 	- the meaning of "unique" insts would be violated
> > 	- referential transparency would be lost
> > 	- soundness would be lost
> 
> Thanks for outlining the problems.  I am fairly new to logic based
> programming languages and the surrounding concepts, but I think I 
> partly understand what you are saying.  
> 
> Are you saying that:
>   - there is a concept of "instances"; "different" instances of a
>     predicate are distinguished through the use of different 
>     variables; allowing Q would mean semantically distinct instances 
>     would have identical variables, violating this concept
>   - two references to the same procedure and variables might have
>     different outcomes
>   - if you tried to translate this Mercury code into a corresponding
>     logic expression representing the semantics of the code, then
>     everything valid in logic would not necessarily be valid in
>     corresponding Mercury code

Roughly speaking, yes, that is what I am saying.

> Is it true to say that the first and third problem you identify
> are a result of the second?

Not really; the second and third are a result of the first.

> > > It seems very similar to what DCG does.  If I am understanding DCG
> > > correctly, what it does is to hide a thread of state variables from the
> > > user.  If the compiler were to accept:
> > > 
> > >   Q = (pred(N::in, Fn::out) is det :- r(X_0, X_0, N, Fn))
> > > 
> > > it would be interpreted as: "each time Q is evaluated, feed in
> > > uniqueness variable X_0 which dies, then create a new uniqueness
> > > variable which we will also call X_0 (okay because the old X_0 is 
> > > dead), ready for feeding in next time Q is evaluated".
> > 
> > This is an operational semantics.  The problem is that this code would
> > have no declarative semantics, i.e. no meaning in predicate logic.
> > There is not even any (local) translation which you could apply
> > to give this code a declarative semantics.
> > 
> > The normal meaning of
> > 
> > 	Q = (pred(N::in, Fn::out) is det :- r(X_0, X_0, N, Fn))
> > 
> > in logic would be
> > 
> > 	(all [N, Fn] Q(N, Fn) <=> r(X_0, X_0, N, Fn))
> > 
> > but the operational semantics that you suggest is not sound
> > w.r.t. this declarative semantics.
> 
> I think what you are saying, is that in the logic expression above,
> there may be N and Fn with r being true for some X_0 and false for
> other X_0, but I'm not really sure.

> Is logic programming based around a search for true predicates?  Is
> there anything you would recommend I read on logic programming?

If you are looking for introductory material on logic programming,
I would recommend the first six chapters of Sterling and Shapiro's
book "The Art of Prolog".

> > We allow DCGs for several reasons:
> > 
> > 	- history: Prolog supports them
> > 
> > 	- DCGs can be considered as mere syntactic sugar for
> > 	  state variable threading.  That is, there is a
> > 	  local syntactic transformation which translates
> > 	  DCG clauses into ordinary clauses, which can then
> > 	  be given a declarative semantics in the usual fashion.
> > 
> > 	- it is also noteworthy you can define a declarative semantics
> > 	  for DCGs directly, if non-DCG code which calls DCGs uses phrase/3.
> 
> Question... if you were to start afresh designing a new Logic
> Programming Language from the ground up, not worrying about Prolog
> roots, would you provide DCGs, or would you do something slightly
> different? 

It would depend a lot on the other design decision for the language.
If the language was dynamically moded, and had appropriate other
features, it might be possible to implement DCGs as a library,
rather than a language feature; in that case, I would provide them.
If that was not the case, then the argument for supporting DCGs is
much weaker, and an alternative notation such as Mercury's state variable
notation would probably suffice.

> I don't know what phrase/3 is, but it sounds interesting.

phrase/3 is like call/3 except that it is used when the first
argument is a DCG goal.  If DCGs are implemented by translating
DCG clauses to ordinary clauses, then phrase/3 is just the same
as call/3.  But using phrase/3 rather than call/3 allows you to
abstract away from how DCGs are implemented, and allows the
possibility that they may be implemented by interpretation
rather than translation.

See <http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-users/mercury-users.9804/0022.html>.

> I am still curious about other possible solutions however.  One
> thought which occured to me... would it be possible to do
> something like:
> 
>   Q(N::in, Fn::out, Q::di, Q::uo)
> 
> Ie, a procedure Q which (along with the arguments N and Fn) takes
> itself as a di parameter and returns a new procedure with the same
> arguments as a uo parameter.

No, that is not allowed; it is a mode error (actually a uniqueness error),
for the same sort of reasons as your original example.

> In essence Q would be a self-modifying
> procedure, but strictly the di and uo modes would mean that Q 
> would represent a series of evaluate-only-once procedures.

In Mercury, variables are immutable; once bound, each variable refers
to a single value for the duration of its scope, not to a series of
different values.

If you want a series of values, you can use mutvars and/or Mercury's
DCG or state variable notations.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- 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
--------------------------------------------------------------------------