Re: (OT) Pushing inductive systems to their limit

[blokhead]

Sounds interesting. I have had unification on my mind a lot lately as well. Unification just makes life really nice, as you can be declarative instead of imperative. Modern functional languages like OCaml and (especially) Haskell use tons of unification. The most notable application is for the various forms of case statements you'll find in these languages (either explicit case statements or implicit conditional behavior, like function overloading & multimethods), so I think of unification mainly as a method for conditional behavior based on the structure of the data involved.

I don't know a lot about heavy-duty logic programming, so I'm wondering what (if any) kinds of logic programming paradigms aren't easily do-able with nothing but a good unification-based case statement (perhaps in the guise of multimethod dispatch)?

In other words, I'm seriously interested in an entirely separate module which allows robust unification of perl data structures.

Again, the application to case statements makes this sound like it's in a similar vein to P6's "~~" smart match operator.

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?

A junction/intersection is the only interpretation that makes any sense to me.

If you think of unification using a geometric interpretation, the unbound variables in the unification problem are the basis of a vector space, the constraints are linear/affine (in)equalities in that space, and the solution of the unification is the intersection of all the affine constraints. Think of unifying (x,x,y) with (x,y,y). The 2-d vector space of assignments to {x,y} collapses to a 1-d vector space.

Of course the constraints you are considering aren't affine, and the spaces aren't exactly vector spaces, but the intuition is the same. Under this interpretation, it's clear that you would want to take the intersection of the ranges of two "conditionally bound" objects.