[mercury-users] Uniqueness modes etc

[Dr Mark H Phillips]

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 (or have I got this the wrong way
    around?)

Is it true to say that the first and third problem you identify
are a result of the second?  Ie, the loss of referential transparency
damages the notion of unique instance and prevents soundness?

I should mention that I am a mathematician but I have only cursory
knowledge of mathematical logic.  And as for my knowledge of
declarative programming, I am teaching myself as I go but have no
formal training in it.

> > 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?
(Preferably downloadable from the web.)

> 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?  Ie, how significant is the historical reason you give
above?

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

> > However, this approach has its limitations (I think).  It is
> > okay if my procedure only applies the first 10 permutations
> > generated, but what if I want it to apply the first M 
> > permutations where M is an input variable?  If I understand
> > the DCG mechanism correctly, this won't work.  (Perhaps
> > I am wrong about this??)
> 
> I don't see the problem.  You can achieve this sort of thing using
> recursion and if-then-else:
> 
> 	 apply_repeatedly(M, Q) -->
> 	 	(if { M = 0 } then
> 			{ true }
> 		else
> 			Q,
> 			apply_repeatedly(M - 1, Q)
> 		).

Okay, I think I was wrong.  It sounds like the mutvar-store 
solution, together with DCG, has a lot going for it.

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

I am guessing self-reference in this fashion might be barred, but I
thought I'd ask.

Thanks again for your comments,

Mark.


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