Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Parallel_Example.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close>

theory Parallel_Example
imports Complex_Main "HOL-Library.Parallel" "HOL-Library.Debug"
begin

subsection \<open>Compute-intensive examples.\<close>

subsubsection \<open>Fragments of the harmonic series\<close>

definition harmonic :: "nat \ rat" where
  "harmonic n = sum_list (map (\n. 1 / of_nat n) [1..

subsubsection \<open>The sieve of Erathostenes\<close>

text \<open>
  The attentive reader may relate this ad-hoc implementation to the
  arithmetic notion of prime numbers as a little exercise.
\<close>

primrec mark :: "nat \ nat \ bool list \ bool list" where
  "mark _ _ [] = []"
| "mark m n (p # ps) = (case n of 0 \ False # mark m m ps
    | Suc n \<Rightarrow> p # mark m n ps)"

lemma length_mark [simp]:
  "length (mark m n ps) = length ps"
  by (induct ps arbitrary: n) (simp_all split: nat.split)

function sieve :: "nat \ bool list \ bool list" where
  "sieve m ps = (case dropWhile Not ps
   of [] \<Rightarrow> ps
    | p#ps' \ let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
by pat_completeness auto

termination \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
  apply (relation "measure (length \ snd)")
  apply rule
  apply (auto simp add: length_dropWhile_le)
proof -
  fix ps qs q
  assume "dropWhile Not ps = q # qs"
  then have "length (q # qs) = length (dropWhile Not ps)" by simp
  then have "length qs < length (dropWhile Not ps)" by simp
  moreover have "length (dropWhile Not ps) \ length ps"
    by (simp add: length_dropWhile_le)
  ultimately show "length qs < length ps" by auto
qed

primrec natify :: "nat \ bool list \ nat list" where
  "natify _ [] = []"
| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"

primrec list_primes where
  "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"

subsubsection \<open>Naive factorisation\<close>

function factorise_from :: "nat \ nat \ nat list" where
  "factorise_from k n = (if 1 < k \ k \ n
    then
      let (q, r) = Divides.divmod_nat n k
      in if r = 0 then k # factorise_from k q
        else factorise_from (Suc k) n
    else [])"
by pat_completeness auto

termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
  apply (relation "measure (\(k, n). 2 * n - k)")
    apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
  apply (case_tac "k \ ka * 2")
   apply (auto intro: diff_less_mono)
  done

definition factorise :: "nat \ nat list" where
  "factorise n = factorise_from 2 n"

subsection \<open>Concurrent computation via futures\<close>

definition computation_harmonic :: "unit \ rat" where
  "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"

definition computation_primes :: "unit \ nat list" where
  "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"

definition computation_future :: "unit \ nat list \ rat" where
  "computation_future = Debug.timing (STR ''overall computation'')
   (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
     in (computation_primes (), Parallel.join c))"

value "computation_future ()"

definition computation_factorise :: "nat \ nat list" where
  "computation_factorise = Debug.timing (STR ''factorise'') factorise"

definition computation_parallel :: "unit \ nat list list" where
  "computation_parallel _ = Debug.timing (STR ''overall computation'')
     (Parallel.map computation_factorise) [20000..<20100]"

value "computation_parallel ()"

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.