Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Iteration until saturation

Email Gateway (Aug 18 2022 at 10:06):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi list,

I want to formalize a saturation algorithm.
That is, I start with some initial set v_0:: 's set and have a function
f:: 's set => 's set that maps sets to additional elements that should
be added.

Imperatively, I have the following algorithm:
input: v0
precondition: v0 \subseteq U & P v0
v:=v_0
while there is some x with x \in f v and not x \in v do v:=v \cup {x}; od
output: v

Function f is monotonous.

Termination is because I have a finite set U such that v_0 \subseteq U
and v\subseteq U ==> f v \subseteq U.

To prove something about the result, I have an invariant P, such that P
v_0 and [|P v; x\in f v - v |] ==> P (v \cup {x}).

What approach should I use to formalize this algorithm in isabelle, i.e.
define some Isabelle function algo: 's set => 's set that describes the
algorithm above, and
how to prove
v0 \subseteq U & P v0 ==> P algo v0
and
v0 \subseteq U & P v0 ==> f(algo v0) \subseteq algo v0

My main problem with using inductive definition, i.e. somthing like
inductive "algo v0"
intros
"x\in v0 ==> x \in algo v0"
"x\in f (algo v0) ==> x \in (algo v0)"
monos f_mono

is, that I cannot use the invariant P to reason about the correctness of
the result. Using algo.induct, I can only reason about single elements
of (algo v0), but not
about the set as whole (as this reasoning would not be correct in
general for infinite sets).

Thanks in advance for any hints or pointers to examples of formalization
of such algorithms.

-- Peter

Email Gateway (Aug 18 2022 at 10:07):

From: Alexander Krauss <krauss@in.tum.de>
Peter,

I want to formalize a saturation algorithm.
That is, I start with some initial set v_0:: 's set and have a function
f:: 's set => 's set that maps sets to additional elements that should
be added.

Imperatively, I have the following algorithm:
input: v0
precondition: v0 \subseteq U & P v0
v:=v_0
while there is some x with x \in f v and not x \in v do v:=v \cup
{x}; od
output: v

Function f is monotonous.

Termination is because I have a finite set U such that v_0 \subseteq U
and v\subseteq U ==> f v \subseteq U.

It seems the best way to to this is using recdef (I assume you are using
Isabelle 2005, otherwise the new "function" package for partial
functions would be just what you need)

The problem here is that the function might not terminate if called
outside the finite set U you mention...? In this case, you might need to
have an extra check for this:

recdef algo "???"
"algo v = (if v \subseteq U then
then if f v \subseteq v then v else algo (v \union f v)
else arbitrary)"

for the termination relation, you should be able to construct something
using the predefined wellfounded relation "finite_psubset".

I replaced the "pointwise" addition by a union, which should be the same
if f is monotone...

To prove something about the result, I have an invariant P, such that P
v_0 and [|P v; x\in f v - v |] ==> P (v \cup {x}).

From this you should also be able to prove
"[| v \subseteq U; P v |] ==> P (v \union f v)"
(using your finiteness assumptions and induction) which together with
algo.induct gives you your result.

Hope this helps...
Alex

Last updated: May 03 2024 at 04:19 UTC