[Oz] equality of unbound variables

[Cesare Tinelli]

Dear Nil, Denys and Christian,

thank you all for your prompt answer. Below are my replies to each of your
suggestions.

Best,

Cesare

-----------------------

Nils Franzen wrote:

>
>
> I think {System.eq V1 V2 ?B} is what you are looking for...

Yes indeed. The function is in fact documented in one of the manuals, but I
had missed it.



Christian Schulte wrote:

>
> If you know in advance for which records you'll need variants, you also
> can use procedural/functional abstraction, that is wrap the record
> construction into a function, for example
>
>         fun {F}
>           X Y in a(X Y Y)
>         end
>
> returns on each application a fresh variant.
>

That is a good idea, but unfortunately the record I need to make variants of
is not known in advance (it depends on the user's input). I guess I should
have specified that in my previous mail.


Denys Duchier wrote:

> tinelli at cs.uiowa.edu (Cesare Tinelli) writes:
>
> > Consider a tuple T, some of whose arguments are unbound variables,
> > possibly with repetitions; for instance, something like T=t(X Y X Z Z).
> > I want to create a fresh ``variant'' of T in the sense of unification
> > theory, that is, a copy of T in which all of T's unbound variables are
> > (bijectively) renamed to fresh variables. For instance, in the example
> > above, I'd like to produce a tuple of the form  t(X1 Y1 X1 Z1 Z1) where
> > X1, Y1, Z1 are fresh variables.
>
> What you want to do sounds very much like a Prolog trick.

Well, what you suggest below looks a lot like an Oz trick instead :)

> It would be
> even more meaningless in Oz due to constraints and other cncurrent
> agents :-) Fortunately, it has never been needed since Oz offers
> "computation spaces" and "encapsulated search".

> declare S = {Space.new proc {$ R} X Y Z in R=t(X Y X Z Z) end}
>
> creates a computation space whose "root variable" is constrained to be
> of the form you described.
>
> {Space.inject S proc {$ R} R:::1#9 R.1=:1+R.2 end}
>
> installs a constraint that causes X Y Z to become finite domain
> variables in the range 1..9 and enforces X=1+Y.
>
> You can now duplicate (clone) the entire computation space including
> the constraints and threads that reside in it as follows:
>
> declare S2 = {Space.clone S}
>
> This cloning idea is the basis for the implementation of "encapsulated
> search".
>

I guess I still have to come to a full appreciation of computational spaces
and encapsulated search, but what you suggest lappears like a fairly
complex, and costly, solution to (what a see as) a simple problem. Nils
suggestion of using System.eq will do for me.

>
> It might be helpful to describe _what_ you are trying to achieve.  We
> might then be able to suggest how that is best realized in Oz.
>

Sure. I'm writing an automated deduction application prototype. There, I
find it very convenient to implement the logical variables of input formulas
or terms as Oz variables, because I then get unification and substitution
for free.
In a couple of situations, however, I need to work with both terms and their
variants (in the same space), hence my request.


>
> > Put it more simply, is there any way in Oz to always tell whether to
> > unbound variables are the same or not? I've been thinking of tricks
> > involving spaces and stateful data, but I think it should be simpler
> > than that.
>
> You can use System.eq to test for identity, but I am afraid that would
> be thinking along the wrong lines.
>

Given that I'm identifying variables in the object language (the input
formulas) with variables in the implementation language (Oz) I do need a
metapredicate such as System.eq.
Of course, I could represent object variables differently, but then I would
have to reimplement certain functionalities that are already present in Oz
itself, and I'd rather not do that.


Thanks again.


=======================================================================
 Cesare Tinelli, Assistant Professor
 Department of Computer Science       email: tinelli at cs.uiowa.edu
 University of Iowa                   URL:   www.cs.uiowa.edu/~tinelli
 14 McLean Hall                       Phone: +1-319-335-0735
 Iowa City, Iowa 52242 USA            Fax:   +1-319-335-3624
=======================================================================






-
Please send submissions to users at mozart-oz.org
and administriva mail to users-request at mozart-oz.org.
The Mozart Oz web site is at http://www.mozart-oz.org/.