Re: [isabelle] union-find based unification

Hi Christian,

On 03/22/2013 08:21 AM, Christian Sternagel wrote:
Dear Lukas,

I vaguely remember that we already talked about this and well, I am interested ;)

I will send you the sources. If you have time to polish it, we can submit it to the AFP.
(If possible, I would like to improve the generated code for IsaFoR, however, after some recent improvements by René, this might no longer be necessary, let's see.)

I believe that the functional implementation of unification based on a efficient functional Map implementation is only a minor constant factor slower than the imperative implementation.
Then you would not even have to consider the Imperative HOL setting.

In principle I'm also interested in using Imperative HOL for algorithm refinement prior to code generation (at the moment it's not clear to me whether this is possible at all, i.e., for some pure function "f", prove that an Imperative HOL function "g" is a faithful implementation... if I understand correctly, "g" will always have its result type wrapped in "Heap" and thus we cannot prove a code equation between "f" and "g"... but maybe I'm wrong).

I have an argument how to define escaping this monad and set up code generation in a sound way by extending the code generation specialities for Imperative HOL even more. However, I would rather want to see that the monad remains in the whole program.

I was always hoping that the newly developed Lifting package could automate the tedious task of lifting all purely functional parts into the monad, but I never tried that.




On 03/22/2013 02:48 PM, Lukas Bulwahn wrote:
Hi Christian,

I have an efficient first-order unification algorithm in Imperative HOL
in my shelf (from back in 2009).
I was mainly interested in using Imperative HOL and what the problems in
larger developments are with the Imperative HOL framework.
Also, we used that as case study for the partial function prototype in

However, I never found time to polish the proofs and make that work
publicly available.
If you are interested, we can discuss if the unpolished development is
of any use for you.


On 03/22/2013 06:03 AM, Christian Sternagel wrote:
Dear all,

is anybody aware of an Isabelle/HOL (or even better Imperative_HOL)
formalization of a union-find data structure for which also code can
be generated? I found

which mentions union-find trees in the introduction, but by skimming
over the theory names nothing immediately jumped at me ;)

The reason I ask is for an efficient (code generatable) formalization,
using union-find,  of a first-order unification algorithm. Anybody
aware that this was already done?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.