[Oz] equality of unbound variables

[Cesare Tinelli]

Denys Duchier wrote:
> 
> 
> Hi Cesare,
> 
> I am now back from vacation.  Here is my belated answer to your last
> message.
>
Actually, I was not expecting an answer sooner than this week. Even the
wizards of Oz need a vacation once in a while!

 
> tinelli at cs.uiowa.edu (Cesare Tinelli) writes:
> 
> > My only concern is that, as I understand it, the approach you highlight
> > above still requires for a term to be known in advance (at compile time,
> > that is) to be encapsulated. I don't quite understand how to use the
> > encapsulation technique with terms that are only known at run time, for
> > instance because they are passed as input.
> > Well, if the term is passed as a string, it is fairly straightforward to
> > wrap it into a function definition (with the proper local variable
> > definitions), feed it to Compiler.virtualStringToValue say, and get its
> > encapsulated version.
> 
> For input, as you suggest, this is not an issue.  Personally, I often
> use Gump to define an application specific language/notation when that
> is more convenient.
>
Sounds like a good idea. But, as you say, it's probably not worth the
effort in my case (see later).

>  In your case, I don't know if that would be a
> worthwhile gain: input is supposed to be a predicate rather than a
> bare term.  Instead of:
> 
>         forall X . f(X X)
> 
> the user supplies
> 
>         fun {$} X in f(X X) end
> 
> i.e. this is the same as:
> 
>         proc {$ T}
>           T={MakeTuple f 2}
>           T.1 = T.2
>         end
>
Yep.
 
> a special purpose notation may allow an implicit quantification
> (convenient), but then does not support a notion of scope
> (inconvenient).
>
Actually, the application in question is a system for deciding term
equivalence modulo a (given) equational theories (for instance, decide
the equivalence modulo the associative-comutative theory of + of the
terms x+(y+z), (x+z)+y in the variables x,y,z).
In this situation, quantifiers are really not needed. As a matter of
fact, free variables are not needed either, as they can usually be
treated as free constants. This is certainly true in my case. In other
words, I can represent input terms as ground Oz tuples (and so not to
worry about encapsulation at all).
As I mentioned in a previous message, I was thinking instead of
representing term variables as actual Oz variables so that I could get
certain thing such as substitutions for free.

I have since convinced myself that using tuples with (non-encapsulated)
unbounded variables is, as you hinted at, the wrong way to go. The
benefits I was hoping for turned out to be minimal compared with the
great pains I'd have to go through to write my code so that Oz does not
suspend all the time on the unbound variables.
In conclusion, I have given up on that idea and I'm now implementing
input terms as ground Oz tuples. Input term variables are now just Oz
atoms (actually, pairs of the form x#I, where I is an integer index).
Needless to say that everything's working just fine now.

 
> > What I don't see is how to encapsulate an Oz record at run time.
> 
> You would never have a non-encapsulated term, except within an
> encapsulated computation which results in an encapsulated term.  In
> fact, you suggest this yourself:
> 
> > But again, maybe I'm thinking in the wrong terms. Maybe there
> > is a way to design any Oz application from the outset so that "run-time
> > encapsulation" will never be needed.
>
Agree.

 
> If you have a practical example where you have difficulty seeing how
> to preserve encapsulation, please let me know and I'll be happy to
> suggest how to modify your design.
> 
At this point I don't anymore. But thanks for the offer. I'll keep it in
mind for future applications.


Best,


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