Email Gateway (Aug 14 2021 at 10:02): Email Gateway (Aug 14 2021 at 10:02):From: Katherine Cordwell <kcordwel@andrew.cmu.edu>
Recently I was trying to parallelize an algorithm using the Parallel.map
function, and ran into some termination issues. For example, the following
function does not terminate with this use of "Parallel.map", though it
would work fine with vanilla "map".
function test:: "real poly ⇒ real poly list ⇒ nat"
where
"test p qs =
( let len = length qs in
if len = 0 then 1
else if len = 1 then 2
else
(let q1 = take (len div 2) qs; q2 = drop (len div 2) qs;
parallel_comput = (Parallel.map (λi. (test p i)) [q1, q2]);
left = parallel_comput ! 1; right = parallel_comput ! 2;
comb = left + right in comb
)
)"
by auto
(* Seems to not be true? *)
termination test
apply (relation "measure (λ(p,qs).(length qs))")
apply auto
sorry
Any explanation/advice would be much appreciated.
Best,
Katherine Cordwell
Email Gateway (Aug 14 2021 at 11:59):From: Manuel Eberl <eberlm@in.tum.de>
This is a classic case of a missing fundef_cong rule. Basically,
something needs to tell the function package that "Parallel.map f xs"
will only evaluate f on xs. This is done by proving a corresponding
congruence rule and declaring it as "fundef_cong":
lemma parallel_map_cong [fundef_cong]:
"(⋀x. x ∈ set xs ⟹ f x = g x) ⟹ xs = ys ⟹
Parallel.map f xs = Parallel.map g ys"
unfolding Parallel.map_def by (rule map_cong) auto
This is really an omission of the "HOL-Library.Parallel" theory, in my
opinion, and should be added there.
Your termination proof is then pretty straightforward, since you now
have more information available:
termination
proof (relation "measure (λ(p,qs).(length qs))"; clarsimp; goal_cases)
case (1 qs xs)
have "length xs ≤ Suc (length qs) div 2"
using 1 by auto
moreover have "length qs > 1"
using 1 by (cases qs) auto
ultimately have "length xs < length qs"
by linarith
thus ?case by auto
qed
"fundef_cong" is briefly mentioned in section 10 of the Function package
manual ("Higher-Order Recursion"). But I certainly cannot blame you for
missing it – it really is the tiniest of remarks. :)
Cheers,
Manuel
smime.p7s
Email Gateway (Aug 20 2021 at 10:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Katherine,
in Isabelle/HOL there is one quite successful principle when optimizing
specifications for executability: optimize the specifications for
provability and succinctness, prove separate lemmas for optimization of
executability.
This is the reason why Parallel.thy is not optimized for basing
specifications on it.
As far as I understand your example, you would end up with sth. like:
definition test:: ‹real poly ⇒ real poly list ⇒ nat›
where ‹test = …›
and later prove separately:
lemma test_code [code]:
‹test p qs =
( let len = length qs in
if len = 0 then 1
else if len = 1 then 2
else
(let q1 = take (len div 2) qs; q2 = drop (len div 2) qs;
parallel_comput = (Parallel.map (λi. (test p i)) [q1, q2]);
left = parallel_comput ! 1; right = parallel_comput ! 2;
comb = left + right in comb
)
)›
With a logically precise definition of ‹test› already at hand, the prove
of the code equation is usually easier than proving a complicated
termination schema.
I'm curious for your actual example, it seems to me that it utilizes a
divide-and-conquer schema which is a candidate to be added to
Parallel.thy explicitly.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Aug 31 2021 at 13:05):From: "Jens-D. Doll" <jens.doll@live.de>
Hello Florian,
please specify the categories executability, provability. What is the
common ground of these?
Thanks, Jens
------ Originalnachricht ------
Email Gateway (Sep 12 2021 at 14:38):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jens,
please specify the categories executability, provability. What is the
common ground of these?
a good practical introduction is §3 in the tutorial of code generation.
The use of the terms »provability« and »executability« in my answer was
indeed a little bit sloppy; »provability and succintness« refers how
»easy« properties can be derived from the specification as given in the
theory, »optimization of executability« refers to optimization of the
resulting executable program.
Cheers,
Florian
OpenPGP_signature
Last updated: Apr 23 2024 at 16:19 UTC