Re: [isabelle] union-find based unification
On 03/22/2013 08:21 AM, Christian Sternagel wrote:
I will send you the sources. If you have time to polish it, we can
submit it to the AFP.
I vaguely remember that we already talked about this and well, I am
(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
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:
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
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:
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