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 optimization.)

So maybe I should point him to this mail thread, to join the discussion.


	Makarius


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