[Oz] equality of unbound variables

[Cesare Tinelli]

Hi everybody,

I've been struggling to come up with a simple solution to the
(supposedly) simple problem below. Any suggestions will be appreciated.

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.

Initially I thought of using {Record.clone T}, or similar methods,  to
produce a tuple T1 of the form t(V1 V2 V3 V4 V5), and then identify T1.i
with T1.j  for all i and j such that T.i and T.j coincide.
Unfortunately, that will not work because the avaible equality tests in
Oz (X==Y, cond X=Y ...) will generally suspend on unbound variables.

Is there some other way to do this? Or maybe an Oz primitive that I'm
missing?

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.

Thanks a lot,


Cesare


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