Email Gateway (Aug 19 2022 at 10:34): Email Gateway (Aug 19 2022 at 10:34):From: Christian Sternagel <c.sternagel@gmail.com>
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
http://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml
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?
cheers
chris
Email Gateway (Aug 19 2022 at 10:34):From: Lukas Bulwahn <bulwahn@in.tum.de>
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 2010.
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.
Lukas
Email Gateway (Aug 19 2022 at 10:34):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Lukas,
I vaguely remember that we already talked about this and well, I am
interested ;)
(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.)
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).
cheers
chris
Email Gateway (Aug 19 2022 at 10:34):From: Peter Lammich <lammich@in.tum.de>
http://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml
The union-find structures are in the examples folder in
Examples/Union_Find.thy.
However, someone seems to have messed up ROOT.ML when porting to
Isabelle2013, such that this file is not compiled any more!
I'll check whether Union_Find still compiles under 2013, and send a
patch here if it does not.
Best, and thanks for pointing to the problem,
Peter
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?cheers
chris
Email Gateway (Aug 19 2022 at 10:34):From: Lukas Bulwahn <bulwahn@in.tum.de>
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.
Lukas
cheers
chris
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
2010.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.Lukas
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 foundhttp://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml
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?cheers
chris
Email Gateway (Aug 19 2022 at 10:35):From: Peter Lammich <lammich@in.tum.de>
If you want to invest some manual work in the algorithm refinement, you
can see examples how to do that in the Separation_Logic_Imperative_HOL
entry. For example, the Union_Find data structures are first formalized
and proved correct on functional lists, and then refined to
Imperative/HOL.
Currently, I'm working on a more automatic way to refine (monadic, using
the refinement monad) programs to Imperative/HOL, but there is nothing
to show yet.
Email Gateway (Aug 19 2022 at 10:35):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
This seems to be my fault. It's now back in and online again.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 10:35):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 19 2024 at 04:17 UTC