[Oz] equality of unbound variables

[Seif Haridi]

Included is a Prolog style CopyTerm that doess not work on infinite
(cyclic) structure.

Seif Haridi

Cesare Tinelli wrote:

> 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/.
-------------- next part --------------
%%% Prolog-style CopyTerm copies only records and numbers
%%% Does not copy cyclic values
%%% Uses System.eq


declare
local
   proc {Copy X Vs0 ?Vs ?Y}
      if {IsDet X} then 
	 if {IsNumber X} then
	    Y = X
	    Vs = Vs0
	 elseif {IsRecord X} then
	    {CopyRecord X Vs0 Vs Y}
	 else
	    raise error('Copy'(X Y)) end
	 end
      else
	 {CopyVar X Vs0 Vs Y}
      end
   end
   proc {CopyRecord R Vs ?Ws ?S}
      As = {Arity R} in
      S = {MakeRecord {Label R} As}
      {CopyArgs R As Vs Ws S}
   end
   proc {CopyArgs R As Vs0 ?Vs ?S}
      case As
      of nil then Vs0 = Vs
      [] A|Ar then
	 Vs1 in
	 {Copy R.A Vs0 Vs1 S.A}
	 {CopyArgs R Ar Vs1 Vs S}
      end
   end
   proc {CopyVar X Vs Ws ?Y}
      case Vs
      of nil then Ws = [(X#Y)]
      [] (O#N)|Vr then
	 Wr in
	 if {System.eq X O} then
	    Y = N
	    Ws = Vs
	 else
	    Ws = (O#N)|Wr
	    {CopyVar X Vr Wr Y}
	 end
      end
   end
in
   proc {CopyTerm X Y}
      {Copy X nil _ Y}
   end
end

/*

declare X 
{Browse {CopyTerm f(X a  [X] X) $}}

*/