Re: [isabelle] union-find based unification
On Fri, 22 Mar 2013, Lukas Bulwahn wrote:
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.
That is a very interesting observation.
Just yesterday, I've attended a talk by a Coq person who made substantial
investments to include monadic imperative programming to the Coq code
extraction mechanism. He had exactly the same example, so there is
probably just that one :-) I was also wondering how much you get in
return for adding such impurity Coq. (The approach was also somehow
biased towards sequential execution, which is a bit anachronistic for code
So maybe I should point him to this mail thread, to join the discussion.
This archive was generated by a fusion of
Pipermail (Mailman edition) and