[mercury-users] vanilla in Mercury

[Ralph Becket]

Randall Helzerman wrote on  7 Sep:
> I'm trying to port an application from prolog to Mercury.  It makes
> extensive use of a very simple metainterpreter (vanilla):
> 
> demo([]).
> demo([G|Gs]) :-
>         axiom(G,Gs1),
>         append(Gs1,Gs,Gs2),
>         demo(Gs2).
> 
> or simple modifications thereof (abduction, goal delaying,
> negation-as-failure--things like that).
> 
> Can such a simple meta-interpreter be coded in Mercury?

The problem here is that (for very good reasons) Mercury doesn't
support full-on logical variables in the same way that Prolog does.
The main show-stopper is that you can't alias two unbound variables,
which is the sort of thing that tends to happen a lot in this kind of
theorem proving application.

If you can guarantee that (1) G will always be ground and that (2) Gs1
will be as a consequence of calling axiom(G, Gs1) then you can
implement the above fairly directly (modulo having to define a special
type for literals).

Otherwise you need a library implementing logical variables, which is
what interpreter.m relies upon.  However, given such a library
(implemented using, say, refs or, preferably, tr_stores), you can
implement demo/1 without too much extra hassle.  The real work happens
in axiom/2 where you have to worry about special calls for unification
and so forth.

This is exactly what I'm working on at the moment (I'm doing planning
research); we can discuss my approach out of band if you like.  My
take on the problem is that, having done a lot of this kind of theorem
proving stuff in Prolog, working in a ground representation (i.e.
having a special representation for logical variables etc.) is the
Right Way To Go.  Basically, you end up writing a compiler for turning
your theory into Mercury.

Cheers,

Ralph

-- 
Ralph Becket  |  rwab1 at cam.sri.com  |  http://www.cam.sri.com/people/becket.html
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------