in reply to (OT) Pushing inductive systems to their limit
The unification as part of the language idea reminded me of matching in Lisp and Pop-11 (see chapter 7 of the Pop-11 Primer] and chapter 19 of On Lisp). Not exactly what you're talking about but might be worth a look.
Consider how unification works. First, if a particular item has a value we say it is "bound" to that value. We can then unify two items if they fall under one of the following three conditions
Like the Var class in Perl and Prolog and Continuations... oh my! :-)
The main problem that I see is what happens when one tries to unify two conditionally bound objects? Should a junction be the result? Should the unification fail because we have nothing real to bind to? Should they only be allowed to unify iff they are identical? Is there any merit to this idea at all?
I don't see why it would be different from unification of "normal" unbound variables. The logic is the same, it's just the equality test that's different.