Maybe you're looking for "maximal sharing" and hash-consing because these can bring structural equality tests into O(1); used in term rewriting for theorem provers. Maximal sharing data structures are a branch of persistent data structures, due to the required immutability.
-
-
-
I'm familiar with maximal sharing and it's definitely a relevant technique, but I want something more. Consider a hash table with unknown values or a vector with holes in it. Can these permit unify operations? Still have efficient lookup? Concat? push/pop? etc.
-
Mmmm.. interesting. Every studied Steven Ekers' work on pattern matching modulo associativity and commutativity and idempotency? An ACI cons tree _is_ a set. Good reads! Maybe relevant; how to efficiently (and safely) backtrack, via Pierre Etienne Moreau's backtracking library.
-
Interesting, I may take a peek at that.
End of conversation
New conversation -
-
-
Probably some name clashing going on but I know unification from logic programming, is that what you mean?
-
I mean that I have two values that represent incomplete information and I want to get out a new value that represents the union of the information in both; aborting on contradiction.
End of conversation
New conversation -
-
-
I think you want state-based CRDTs: https://hal.inria.fr/inria-00555588/document …
-
Hm, CRDTs hadn't occurred to me as relevant here, but I guess they could be. I'll do some re-reading & think on it. Thanks.
End of conversation
New conversation -
-
-
Haskell has a good library for this. It leverages traversability. It's not impossible to port this with by-hand runtime metaprogramming methods for general structures so long as you can change the type guarantees. Golang 2 will probably be able to do it. http://hackage.haskell.org/package/unification-fd-0.10.0.1/docs/Control-Unification.html …
-
By "data structures", I mean something more interesting than records. I mean abstract data types with procedures having useful semantics and acceptable performance. ie maps, vectors, etc. That library lets you make types unifiable, but says nothing about procedures on them.
-
So you want all of the maps out of your type to also be unified in some sort of way? If two types both support a map named q then q(unify(x, y)) = unify(q(x), q(y))?
-
I've thought a bunch about this since he replied. It seems to me like what it'd end up being is a way to inject bindings into a tree, and to directly model how unassigned variables interact with it at the insert/remove level of the data structure.
-
Oh sure, I definitely imagine this being done in a binding context. It’s first-order unification I believe.
End of conversation
New conversation -
-
-
There is of course the union-find algorithm, that you can generalize to a point. Also important is, when a contradiction is found, exhibit a shortest / most localized subset of inferences (as opposed to declarations) that leads to contradiction.
- 1 more reply
New conversation -
-
-
Monoidal containers? http://hackage.haskell.org/package/monoidal-container … For maps, the values (when both maps have the same key) are combined with the mappend operation.
-
Oops, wrong link. Here's a correct link:http://hackage.haskell.org/package/monoidal-containers …
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.